Set.Countable.biUnion
theorem Set.Countable.biUnion :
∀ {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a ∈ s → Set β},
s.Countable → (∀ (a : α) (ha : a ∈ s), (t a ha).Countable) → (⋃ a, ⋃ (h : a ∈ s), t a h).Countable
The theorem `Set.Countable.biUnion` states that for any two types `α` and `β`, and any set `s` of type `α`, if `s` is countable, and for any element `a` of `s`, the set `t a ha` (where `t` is a function that takes an element of `s` and a proof that it belongs to `s` to a set of type `β`, and `ha` is a proof that `a` belongs to `s`) is countable, then the union of all such sets `t a ha` for each `a` in `s` is also countable. In mathematical terms, this is stating that a countable union of countable sets is countable.
More concisely: If `α` and `β` are types, `s` is a countable set of type `α`, and for each `a` in `s`, the set `t a ha` (where `t : α → Set β` and `ha : a ∈ s`) is countable, then the union of all `t a ha` is countable (i.e., countable union of countable sets is countable).
|
Set.Finite.countable
theorem Set.Finite.countable : ∀ {α : Type u} {s : Set α}, s.Finite → s.Countable
This theorem states that for any type `α` and any set `s` of type `α`, if the set `s` is finite, then it is also countable. In other words, if there exists a natural number `n` and an equivalence between the set `s` and the finite ordinal `Fin n`, there must also exist an injective map from `s` to the set of natural numbers `ℕ`. This theorem is a fundamental property in set theory and number theory.
More concisely: If a type `α`'s set `s` is finite, then it has an injective map to the natural numbers `ℕ`.
|
Set.countable_iUnion
theorem Set.countable_iUnion :
∀ {α : Type u} {ι : Sort x} {t : ι → Set α} [inst : Countable ι],
(∀ (i : ι), (t i).Countable) → (⋃ i, t i).Countable
The theorem `Set.countable_iUnion` states that for any type `α` and any sort `ι`, if we have a function `t` from the set of all `ι` to the set of all `α`, and if `ι` is countable, and if for each `ι`, the set `t i` is countable, then the union of all `t i` is also countable. Here, a set is defined as countable if there exists an injective map from the set to the natural numbers.
More concisely: If `α` is a type, `ι` is a countable sort, and for each `ι`, the set `ti` is countable, then the union of the `ti`'s is countable. (In the language of set theory: The image of a countable set under a function whose domain and each fiber is countable is countable.)
|
Set.Countable.to_subtype
theorem Set.Countable.to_subtype : ∀ {α : Type u} {s : Set α}, s.Countable → Countable ↑s
This theorem restates the definition of a countable set as an instance of countability. Given a type `α` and a set `s` of this type, it states that if `s` is countable (in the sense of the `Set.Countable` predicate), then the subtype corresponding to `s` is also countable in the sense of the `Countable` type class. This theorem provides a bridge between the definition of countability for sets and the definition of countability for subtypes.
More concisely: If `s` is a countable set of type `α`, then the subtype `{x : α | x ∈ s}` is also a countable subtype.
|
Set.to_countable
theorem Set.to_countable : ∀ {α : Type u} (s : Set α) [inst : Countable ↑s], s.Countable
The theorem `Set.to_countable` states that for any type `α` and any set `s` of this type, if the subtype corresponding to this set has an instance of being `Countable` (that is, there exists an injective map from the subtype to the natural numbers), then the set `s` itself is `Countable`. In other words, if we can count the elements of the subtype associated with a set, then we can count the elements of the set itself.
More concisely: If a subtype of a type has a countable instance, then the type itself is countable.
|
Set.countable_setOf_finite_subset
theorem Set.countable_setOf_finite_subset :
∀ {α : Type u} {s : Set α}, s.Countable → {t | t.Finite ∧ t ⊆ s}.Countable
This theorem states that for any type `α` and any set `s` of that type, if `s` is countable, then the set of all subsets `t` of `s` which are both finite and included in `s` is also countable. In mathematical terms, if we have a countable set, then the collection of all of its finite subsets is also countable.
More concisely: If `α` is a type and `s : set α` is countable, then the set of finite subsets of `s` is also countable.
|
Set.Countable.prod
theorem Set.Countable.prod :
∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β}, s.Countable → t.Countable → (s ×ˢ t).Countable
The theorem `Set.Countable.prod` states that for all types `α` and `β`, and for all sets `s` of type `α` and `t` of type `β`, if `s` and `t` are countable, then the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is also countable. In other words, if we can establish a one-to-one correspondence between each of the sets `s` and `t` and the set of natural numbers, then we can also establish a similar correspondence for the set of all ordered pairs `(a, b)` where `a` is from `s` and `b` is from `t`.
More concisely: If `α` and `β` are countable types, and `s:` `Type α` and `t:` `Type β` are countable sets, then their Cartesian product `s ×β t` is also countable.
|
Set.Countable.image
theorem Set.Countable.image :
∀ {α : Type u} {β : Type v} {s : Set α}, s.Countable → ∀ (f : α → β), (f '' s).Countable
The theorem `Set.Countable.image` states that for any type `α` and `β`, and any set `s` of type `α`, if `s` is countable, then for any function `f` from `α` to `β`, the image of `s` under `f` is also countable. This means that applying a function to all elements of a countable set results in a new set that is also countable.
More concisely: If `α` is a countable type and `s : Set α` is countable, then the image `{f x | x ∈ s}` of `s` under a function `f : α → β` is also countable.
|
Set.Countable.exists_eq_range
theorem Set.Countable.exists_eq_range : ∀ {α : Type u} {s : Set α}, s.Countable → s.Nonempty → ∃ f, s = Set.range f
The theorem `Set.Countable.exists_eq_range` states that given any nonempty countable set `s` of type `α`, there exists a function `f` from the set of natural numbers `ℕ` to `α` such that the set `s` is equal to the range of `f`. In other words, for any nonempty countable set, we can find a function that maps each natural number to a unique element in the set, thereby covering all elements of the set.
More concisely: Given a nonempty countable set, there exists a function from natural numbers to set elements such that the set is the range of that function.
|
Set.countable_univ
theorem Set.countable_univ : ∀ {α : Type u} [inst : Countable α], Set.univ.Countable
This theorem states that for any type `α`, if `α` is countable (meaning there exists an injective map from `α` to the natural numbers `ℕ`), then the universal set of `α` is also countable. The universal set of `α` is the set containing all elements of `α`. So, in other words, if we can count the elements of a type `α`, then we can also count all elements in the set of all things of type `α`.
More concisely: If `α` is a countable type, then its universe is also countable.
|
Set.countable_empty
theorem Set.countable_empty : ∀ {α : Type u}, ∅.Countable
The theorem `Set.countable_empty` states that for any type `α`, the empty set of `α` is countable. In other words, there exists an injective map from the empty set to the set of natural numbers. This is true because the empty set does not contain any elements, so it's trivial to map it injectively (without duplicates) to the set of natural numbers.
More concisely: The empty set of any type is countable, i.e., there exists an injective function from the empty set to the natural numbers.
|
Set.countable_iff_exists_injOn
theorem Set.countable_iff_exists_injOn : ∀ {α : Type u} {s : Set α}, s.Countable ↔ ∃ f, Set.InjOn f s
A set `s` of type `α` is countable if and only if there exists an injective function from `α` to the natural numbers `ℕ` which is injective on `s`. In other words, we can enumerate the elements of `s` using natural numbers without any repeats. This is represented by the existence of a function `f` that maps any two different elements in the set `s` to different natural numbers, ensuring that no two distinct elements of `s` share the same natural number in their mapping.
More concisely: A set is countable if and contradiction-free there exists an injective function from the set to the natural numbers.
|
Set.countable_coe_iff
theorem Set.countable_coe_iff : ∀ {α : Type u} {s : Set α}, Countable ↑s ↔ s.Countable
The theorem `Set.countable_coe_iff` states that for any type `α` and any set `s` of type `α`, the set `s` is countable (i.e., there exists an injective function from `s` to the natural numbers) if and only if the corresponding subtype of `s` is countable. In other words, countability of a set and its corresponding subtype are equivalent.
More concisely: For any type `α` and set `s` of type `α`, `s` is countable if and only if its subtype is countable.
|
Set.countable_singleton
theorem Set.countable_singleton : ∀ {α : Type u} (a : α), {a}.Countable
The theorem `Set.countable_singleton` states that for any type `α` and any element `a` of type `α`, the set containing only `a` is countable. In other words, there exists an injective function from the set `{a}` to the set of natural numbers `ℕ`. This implies that single-element sets, or singletons, are always countable regardless of what that single element is.
More concisely: For any type `α` and any element `a` of type `α`, the singleton set `{a}` is countable.
|
Countable.to_set
theorem Countable.to_set : ∀ {α : Type u} {s : Set α}, Countable ↑s → s.Countable
This theorem, `Countable.to_set`, provides an alternative way to express that a set is countable, using a `Countable` instance. Specifically, for any type `α` and set `s` of type `α`, if the set `s`, when converted to a subtype, is countable (`Countable ↑s`), then the set `s` itself is countable (`s.Countable`). In other words, it restates the property `Set.Countable` in terms of a `Countable` instance.
More concisely: If a subtype of a countable type is countable, then the subtype itself is countable. (The `Countable.to_set` theorem in Lean 4 states that `(Countable (subtype.val s)) → s.Countable` for any set `s` of type `α`.)
|
Set.countable_range
theorem Set.countable_range : ∀ {β : Type v} {ι : Sort x} [inst : Countable ι] (f : ι → β), (Set.range f).Countable
The theorem `Set.countable_range` states that for any type `β` and for any sort `ι`, given a countable instance of `ι` and a function `f` from `ι` to `β`, the range of the function `f` is countable. In other words, if we have a countable set, and we apply a function to each element in this set, the set of all possible outputs (the range of the function) is also countable.
More concisely: Given a countable index set `ι` and a function `f` from `ι` to a type `β`, the range of `f` is countable.
|
Finset.countable_toSet
theorem Finset.countable_toSet : ∀ {α : Type u} (s : Finset α), (↑s).Countable
This theorem states that for any type `α` and any finite set `s` of type `α`, the set `s` is countable. In other words, there exists an injective (one-to-one) function from set `s` to the natural numbers. The countability of a set implies that its elements can be listed in a sequence, often an infinite sequence. Here, the theorem states that any finite set can be enumerated in such a way.
More concisely: Every finite set has an injective function to the natural numbers.
|
Mathlib.Data.Set.Countable._auxLemma.2
theorem Mathlib.Data.Set.Countable._auxLemma.2 : ∀ {α : Type u}, ∅.Countable = True
This theorem states that for any type `α`, the empty set of type `α` is countable. In other words, there exists an injective mapping from the empty set to the set of natural numbers. This is true by definition, as there are no elements in the empty set that need to be mapped to the set of natural numbers.
More concisely: The empty set is countable, that is, there exists an injective function from the empty set to the natural numbers.
|
Set.Countable.insert
theorem Set.Countable.insert : ∀ {α : Type u} {s : Set α} (a : α), s.Countable → (insert a s).Countable
The theorem `Set.Countable.insert` states that for any type `α`, any set `s` of that type, and any element `a` of the type `α`, if the set `s` is countable, then the set that results from inserting the element `a` into the set `s` is also countable. Therefore, adding an element to a countable set does not change its countability.
More concisely: If `α` is a type and `s : Set α` is countable, then `s.insert a` is also countable, where `a : α`.
|
Set.countable_iff_exists_surjective
theorem Set.countable_iff_exists_surjective :
∀ {α : Type u} {s : Set α}, s.Nonempty → (s.Countable ↔ ∃ f, Function.Surjective f)
The theorem states that a non-empty set is countable if and only if there exists a surjective function from the set of natural numbers to the subset induced by the set. Here, a set is considered countable if its elements can be put into a one-to-one correspondence with a subset of the natural numbers. A function is surjective if every element in the target set is mapped to by at least one element in the domain set. In this context, the target set is a subset of some type `α`, and the domain set is the set of natural numbers.
More concisely: A set is countable if and only if there exists a surjective function from the natural numbers to the set.
|
Set.Countable.union
theorem Set.Countable.union : ∀ {α : Type u} {s t : Set α}, s.Countable → t.Countable → (s ∪ t).Countable
The theorem `Set.Countable.union` states that for any type `α` and for any two sets `s` and `t` of type `α`, if both `s` and `t` are countable sets then their union `s ∪ t` is also a countable set. This essentially means that the union of two countable sets is itself a countable set.
More concisely: If `s` and `t` are countable sets, then their union `s ∪ t` is also a countable set.
|
Set.Countable.exists_surjective
theorem Set.Countable.exists_surjective :
∀ {α : Type u} {s : Set α}, s.Nonempty → s.Countable → ∃ f, Function.Surjective f
The theorem `Set.Countable.exists_surjective` states that for any type `α` and a non-empty set `s` of type `α`, if `s` is countable then there exists a function `f` which is surjective. In other words, every element of the subtype induced by `s` corresponds to at least one element in the set of natural numbers. This is also known as the forward direction of `Set.countable_iff_exists_surjective`, meaning that if a set is countable, then there exists a surjective function from the natural numbers to that set.
More concisely: If `α` is a type and `s` is a non-empty countable subset of `α`, then there exists a surjective function from the natural numbers to `s`.
|
Set.countable_setOf_nonempty_of_disjoint
theorem Set.countable_setOf_nonempty_of_disjoint :
∀ {α : Type u} {β : Type v} {f : β → Set α},
Pairwise (Disjoint on f) → ∀ {s : Set α}, (∀ (t : β), f t ⊆ s) → s.Countable → {t | (f t).Nonempty}.Countable
The theorem `Set.countable_setOf_nonempty_of_disjoint` states that given a family of sets `f : β → Set α` and a set `s : Set α`, if every set in that family is pairwise disjoint and each set in the family is a subset of `s`, and if `s` itself is countable (i.e., has the same cardinality or size as some subset of the natural numbers), then the subset of `β` consisting of indices `t` for which the corresponding set `f t` is nonempty is also countable. In other words, there can only be countably many nonempty sets in a family of disjoint sets that are all subsets of a countable set.
More concisely: If `s : Set α` is countable and every set in the family `{f t | t ∈ β, f t ⊆ s}` of subsets of `s` is disjoint from every other set in the family, then the index set `{t ∈ β | f t ≠ ∅}` is countable.
|
Set.MapsTo.countable_of_injOn
theorem Set.MapsTo.countable_of_injOn :
∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β},
Set.MapsTo f s t → Set.InjOn f s → t.Countable → s.Countable
This theorem states that for any two sets `s` of type `α` and `t` of type `β`, and a function `f` that maps `α` to `β`, if `f` maps every element of `s` into `t` (`Set.MapsTo f s t`), and `f` is injective (one-to-one) on `s` (`Set.InjOn f s`), and if `t` is countable (`Set.Countable t`), then `s` must also be countable (`Set.Countable s`).
In other words, if we have a function that is injective on a set and maps it into a countable set, then the original set is also countable. This is a logical consequence of the definition of countability – a set is countable if there exists an injective function from the set to the natural numbers. If we have an injective function to another countable set, we can compose this with the injection from that countable set to the natural numbers to get an injection from our original set to the natural numbers.
More concisely: If a function that maps a set `s` injectively into a countable set `t` exists, then `s` is countable.
|
Set.Countable.sUnion
theorem Set.Countable.sUnion :
∀ {α : Type u} {s : Set (Set α)}, s.Countable → (∀ a ∈ s, a.Countable) → s.sUnion.Countable
This theorem, referred to as an "Alias" of the reverse direction of `Set.Countable.sUnion_iff`, states that for any type `α` and any set `s` whose elements are sets of `α`, if `s` is countable and every element of `s` is also countable, then the union of all the sets in `s` is countable. In mathematical terms, this is expressing the idea that a countable union of countable sets is itself countable.
More concisely: If `s` is a countable set of countable sets of type `α`, then the union of `s` is a countable set.
|
Set.Countable.mono
theorem Set.Countable.mono : ∀ {α : Type u} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → s₂.Countable → s₁.Countable
The theorem `Set.Countable.mono` asserts that for any two sets `s₁` and `s₂` of a certain type `α`, if `s₁` is a subset of `s₂` and if `s₂` is countable, then `s₁` is also countable. In other words, countability is preserved under taking subsets: if you have a countable set and you select some elements from it to form a new set, the resulting set will also be countable.
More concisely: If `s₁` is a subset of countable set `s₂` of type `α`, then `s₁` is also countable.
|