Denumerable.ofEquiv_ofNat
theorem Denumerable.ofEquiv_ofNat :
∀ (α : Type u_3) {β : Type u_4} [inst : Denumerable α] (e : β ≃ α) (n : ℕ),
Denumerable.ofNat β n = e.symm (Denumerable.ofNat α n)
The theorem `Denumerable.ofEquiv_ofNat` states that for any type `α` and a type `β` equivalent to `α` (denoted as `β ≃ α`), and for any natural number `n`, the `n`-th element of `β` as indexed by the denumerable decoding is equal to the inverse of the equivalent mapping applied to the `n`-th element of `α`. In other words, applying the bijective function `e` to map elements from `α` to `β` doesn't affect the `n`-th element of the denumerable decoding.
More concisely: For any denumerable types `α` and `β` equivalent to `α`, and any bijective function `e : α ≃ β`, the `n`-th element of `β` as indexed by the denumerable decoding equals the inverse of `e` applied to the `n`-th element of `α`.
|
Denumerable.sigma_ofNat_val
theorem Denumerable.sigma_ofNat_val :
∀ {α : Type u_1} [inst : Denumerable α] {γ : α → Type u_3} [inst_1 : (a : α) → Denumerable (γ a)] (n : ℕ),
Denumerable.ofNat (Sigma γ) n =
⟨Denumerable.ofNat α n.unpair.1, Denumerable.ofNat (γ (Denumerable.ofNat α n.unpair.1)) n.unpair.2⟩
The theorem `Denumerable.sigma_ofNat_val` states that for any denumerable type `α`, a function `γ` from `α` to another type, and a natural number `n`, the `n`-th element of the sigma type `Sigma γ` (which represents dependent pairs of an element of `α` and an element of the type determined by `γ` applied to the element of `α`) is a pair whose first component is the `n`-th denumerable element of `α`, and whose second component is the `n`-th denumerable element of the type determined by `γ` applied to the `n`-th denumerable element of `α`. This is done by using `Nat.unpair` function to split the natural number `n` into two numbers, one for indexing the first component and the other for indexing the second component.
More concisely: For any denumerable type `α` and function `γ` from `α` to another type, the `n`-th element of the sigma type `Σγ` is the pair with the `n`-th element of `α` as the first component and the `n`-th element of the image of `γ` on the `n`-th element of `α` as the second component.
|
Denumerable.decode_inv
theorem Denumerable.decode_inv :
∀ {α : Type u_3} [self : Denumerable α] (n : ℕ), ∃ a ∈ Encodable.decode n, Encodable.encode a = n
The theorem `Denumerable.decode_inv` states that for any natural number `n` and any type `α` that is denumerable (that is, it can be listed in a sequence with no repetitions), there exists an element `a` in the decoding of `n` such that the encoding of `a` is equal to `n`. In other words, the functions `decode` and `encode` are inverses of each other for denumerable types. This means that if you encode an element of a denumerable type and then decode the resulting number, you get back the original element. Similarly, if you decode a natural number and then encode the resulting element, you get back the original number. This relationship is fundamental to the concept of a denumerable set in mathematics, which refers to a set that can be put into a one-to-one correspondence with the set of natural numbers.
More concisely: For any denumerable type `α` and natural number `n`, there exists an element `a` of `α` such that `encode(a) = n` if and only if `decode(n) = a`.
|
Denumerable.encode_ofNat
theorem Denumerable.encode_ofNat :
∀ {α : Type u_1} [inst : Denumerable α] (n : ℕ), Encodable.encode (Denumerable.ofNat α n) = n
This theorem, `Denumerable.encode_ofNat`, states that for any type `α` that is denumerable (i.e., can be put into a one-to-one correspondence with the natural numbers), and a given natural number `n`, when we use the function `Denumerable.ofNat` to get the `n`-th element of `α` and then encode it back to a natural number using `Encodable.encode`, we get the original natural number `n` back. In other words, encoding the `n`-th element of a denumerable type `α` yields `n` itself. This is essentially asserting the correctness of the encoding and decoding process for denumerable types.
More concisely: For any denumerable type α and natural number n, `Denumerable.encode_ofNat α n = n`.
|
Nat.Subtype.exists_succ
theorem Nat.Subtype.exists_succ : ∀ {s : Set ℕ} [inst : Infinite ↑s] (x : ↑s), ∃ n, ↑x + n + 1 ∈ s
This theorem states that for every set `s` of natural numbers `ℕ`, given that `s` is infinite (`Infinite ↑s`), for any element `x` in `s`, there exists a natural number `n` such that the sum of `x`, `n`, and 1 is also an element in the set `s`. In other words, we can always find a natural number `n` so that moving `n` plus one steps from any number in an infinite set of natural numbers will still keep us within the set.
More concisely: For every infinite set `s` of natural numbers, for all `x` in `s`, there exists `n` in `ℕ` such that `x + n + 1` is also in `s`.
|
Nat.Subtype.lt_succ_self
theorem Nat.Subtype.lt_succ_self :
∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] (x : ↑s), x < Nat.Subtype.succ x := by
sorry
This theorem states that for any set `s` of natural numbers which is infinite, and for any element `x` in the set `s`, `x` is strictly less than the successor of `x` in the set `s` according to the usual ordering of natural numbers. Here, the successor of `x` is computed using the function `Nat.Subtype.succ`. This result formalizes a fundamental property of natural numbers within a subset, that each number is less than its successor.
More concisely: For any infinite set `s` of natural numbers and any `x` in `s`, `x` is strictly less than `Nat.Subtype.succ x` in the order of natural numbers.
|
Denumerable.ofNat_encode
theorem Denumerable.ofNat_encode :
∀ {α : Type u_1} [inst : Denumerable α] (a : α), Denumerable.ofNat α (Encodable.encode a) = a
This theorem states that for any type `α` that is denumerable, applying the function `Denumerable.ofNat α` to the result of encoding an element `a` of type `α` using `Encodable.encode` will return the original element `a`. In other words, the encoding operation, followed by the decoding operation, is the identity operation for any element of any denumerable type.
More concisely: For any denumerable type `α` and encodable element `a` of type `α`, `Encodable.encode a = Denumerable.ofNat (α : Type) (Denumerable.ofNat _ a)`.
|
nonempty_denumerable
theorem nonempty_denumerable : ∀ (α : Type u_3) [inst : Countable α] [inst : Infinite α], Nonempty (Denumerable α) := by
sorry
This theorem, `nonempty_denumerable`, states that for any type `α`, if `α` is countable and infinite, then there exists a denumerable encoding for `α`. In other words, we can list all elements of `α` in a sequence, such that any element in `α` is associated with a unique natural number. This is often used in set theory and number theory to discuss concepts such as countable infinity.
More concisely: If a countable and infinite type `α` exists, then it has a denumerable encoding.
|
Nat.Subtype.ofNat_surjective
theorem Nat.Subtype.ofNat_surjective :
∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s],
Function.Surjective (Nat.Subtype.ofNat s)
This theorem, `Nat.Subtype.ofNat_surjective`, states that for any set `s` of natural numbers which is infinite (`Infinite ↑s`) and has a decidable membership predicate (`DecidablePred fun x => x ∈ s`), the function `Nat.Subtype.ofNat` is surjective. In mathematical terms, this means that for every element in the co-domain (the subtype of natural numbers in `s`), there exists an element in the domain (the set of natural numbers) such that the function maps this domain element to the given co-domain element. In other words, every element in the subtype `↑s` can be attained by applying the function `Nat.Subtype.ofNat` on some natural number.
More concisely: If `s` is an infinite, decidably enumerable set of natural numbers, then the function `Nat.Subtype.ofNat : Nat →* ↑s` is surjective.
|
Denumerable.decode_eq_ofNat
theorem Denumerable.decode_eq_ofNat :
∀ (α : Type u_3) [inst : Denumerable α] (n : ℕ), Encodable.decode n = some (Denumerable.ofNat α n)
The theorem `Denumerable.decode_eq_ofNat` states that for any type `α` that has a `Denumerable` instance, and for any natural number `n`, the decoding of `n` into an optional value of type `α` is exactly equal to the `n`-th element of `α` indexed by the decoding. Essentially, this means that the function `Denumerable.ofNat` returns the `n`-th element of `α` that correctly matches the decoded value of `n` using the `Encodable.decode` function.
More concisely: For any type `α` with a `Denumerable` instance and natural number `n`, `Denumerable.decode (Encodable.decode x (Encodable.encode (Some (α!n))) = α!n`, where `x : option Nat` is the decoded value of `n`.
|
Denumerable.ofNat_of_decode
theorem Denumerable.ofNat_of_decode :
∀ {α : Type u_1} [inst : Denumerable α] {n : ℕ} {b : α}, Encodable.decode n = some b → Denumerable.ofNat α n = b
This theorem, `Denumerable.ofNat_of_decode`, states that for every type `α` that has a `Denumerable` instance and for every natural number `n` and element `b` of type `α`, if the decoding of `n` yields `b` (i.e., `Encodable.decode n = some b`), then the `n`-th element of `α`, as indexed by the decoding, is indeed `b` (i.e., `Denumerable.ofNat α n = b`). This connects the behavior of the `Encodable.decode` function with the `Denumerable.ofNat` function and asserts that they are consistent in their indexing and decoding of elements in denumerable types.
More concisely: For every denumerable type `α` and natural number `n` such that `Encodable.decode n = some b`, it holds that `Denumerable.ofNat α n = b`.
|