Function.Surjective.countable
theorem Function.Surjective.countable :
∀ {α : Sort u} {β : Sort v} [inst : Countable α] {f : α → β}, Function.Surjective f → Countable β
The theorem `Function.Surjective.countable` states that for any types `α` and `β`, if `α` is countable and there exists a function `f` from `α` to `β` that is surjective (i.e., for every element `b` in `β`, there exists an element `a` in `α` such that `f(a) = b`), then `β` is also countable. Here, a countable type is one that has the same cardinality as some subset of the natural numbers.
More concisely: If `α` is a countable type and `f: α → β` is a surjective function, then `β` is also countable.
|
Uncountable.of_equiv
theorem Uncountable.of_equiv : ∀ {β : Sort v} (α : Sort u_1) [inst : Uncountable α], α ≃ β → Uncountable β
This theorem is stating that if there is an equivalence (bijective mapping) between two types, `α` and `β`, and `α` is uncountable, then `β` must also be uncountable. In other words, uncountability is preserved under equivalence relations. This is similar to saying that if you have an uncountable set in the mathematical sense (like the set of real numbers) and you can establish a one-to-one correspondence between this set and another set, the other set is also uncountable.
More concisely: If `α` is an uncountable type and there exists an equivalence relation between `α` and `β`, then `β` is also an uncountable type.
|
Countable.exists_injective_nat'
theorem Countable.exists_injective_nat' : ∀ {α : Sort u} [self : Countable α], ∃ f, Function.Injective f
A type `α` is countable if there exists an injective function from `α` to the set of natural numbers `ℕ`. The theorem `Countable.exists_injective_nat'` states that for any type `α` that is countable (as denoted by `[self : Countable α]`), there exists a function `f` such that `f` is injective. Injectivity of `f` means that if `f` maps two elements of `α` to the same natural number, those two elements must be identical.
More concisely: For any countable type `α`, there exists an injective function from `α` to the natural numbers.
|
Countable.of_equiv
theorem Countable.of_equiv : ∀ {β : Sort v} (α : Sort u_1) [inst : Countable α], α ≃ β → Countable β
This theorem, `Countable.of_equiv`, states that for any two types `α` and `β`, if `α` is countable and there exists a bijective function (an equivalence) between `α` and `β`, then `β` is also countable. In other words, the countability of a type is preserved under bijective mappings. Here, countability refers to the property that there exists a surjective function from the natural numbers to the given type.
More concisely: If `α` is a countable type and there exists a bijective function between `α` and `β`, then `β` is also countable.
|
Uncountable.not_countable
theorem Uncountable.not_countable : ∀ {α : Sort u_1} [self : Uncountable α], ¬Countable α
This theorem states that for any type `α`, if `α` is uncountable (that is, there is no one-to-one correspondence between the elements of `α` and the set of natural numbers), then it is not countable. In other words, no surjective function exists from the natural numbers to `α`. This is a basic property of set cardinality in mathematics.
More concisely: If a type `α` is uncountable, then there is no surjective function from the natural numbers to `α`.
|
Function.Injective.countable
theorem Function.Injective.countable :
∀ {α : Sort u} {β : Sort v} [inst : Countable β] {f : α → β}, Function.Injective f → Countable α
The theorem `Function.Injective.countable` states that for any two types `α` and `β`, if `β` is countable (i.e., there exists a surjective function from the natural numbers to `β`) and `f` is a function from `α` to `β` that is injective (i.e., no two different elements in `α` map to the same element in `β`), then `α` is also countable. In other words, if we have an injective function from `α` to a countable set `β`, then `α` must also be countable.
More concisely: If `β` is countable and `f : α → β` is an injective function, then `α` is countable.
|
Function.Injective.uncountable
theorem Function.Injective.uncountable :
∀ {α : Sort u} {β : Sort v} [inst : Uncountable α] {f : α → β}, Function.Injective f → Uncountable β
The theorem `Function.Injective.uncountable` states that for any sorts `α` and `β`, given an instance where `α` is uncountable and a function `f` from `α` to `β` that is injective, it follows that `β` is uncountable. In other words, if we have an uncountable set and an injective function from this set to another set, then the other set is also uncountable.
More concisely: If `α` is an uncountable set and `f : α → β` is an injective function, then `β` is uncountable.
|
not_countable
theorem not_countable : ∀ {α : Sort u} [inst : Uncountable α], ¬Countable α
This theorem states that for any type `α`, if `α` is uncountable, then it cannot be countable. In more mathematical terms, if a type `α` exists such that it has an uncountable number of elements (denoted by the Uncountable `α`), then it is not possible for `α` to also have a countable number of elements (denoted by the negation `¬Countable α`).
More concisely: If a type `α` is uncountable, then it is not countable.
|
exists_surjective_nat
theorem exists_surjective_nat : ∀ (α : Sort u) [inst : Nonempty α] [inst : Countable α], ∃ f, Function.Surjective f
The theorem `exists_surjective_nat` states that for any sort or type `α`, given that `α` is nonempty and countable, there exists a function `f` that is surjective. In other words, no matter what element you choose in the co-domain of `f`, there is at least one element in the domain of `f` that maps to it. Countability here refers to the property that there's a one-to-one correspondence between the elements of `α` and the natural numbers.
More concisely: If `α` is a nonempty and countable type or sort, then there exists a surjective function `f : ℕ → α`.
|
Equiv.countable_iff
theorem Equiv.countable_iff : ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Countable α ↔ Countable β)
This theorem states that for any two types `α` and `β`, if `α` is equivalent to `β` (denoted as `α ≃ β`), then `α` is countable if and only if `β` is countable. In other words, the countability of `α` and `β` is preserved under their equivalence. The countability of a type is a property that indicates whether the elements of the type can be put in one-to-one correspondence with the set of natural numbers.
More concisely: If two types `α` and `β` are equivalent (`α ≃ β`), then they have the same countability property.
|
countable_iff_exists_surjective
theorem countable_iff_exists_surjective :
∀ {α : Sort u} [inst : Nonempty α], Countable α ↔ ∃ f, Function.Surjective f
This theorem, `countable_iff_exists_surjective`, states that for any type `α` (which must be nonempty), `α` is countable if and only if there exists a surjective function `f`. A surjective function `f` from type `α` to another type, is a function such that for every element in the second type, there is at least one element in the first type `α` that maps to it under `f`. In mathematical terms, this is saying that a set is countable if and only if there exists a function that is surjective (onto) from the set to the set of natural numbers.
More concisely: A nonempty type `α` is countable if and only if there exists a surjective function from `α` to the natural numbers.
|