Set.Finite.diff
theorem Set.Finite.diff : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (s \ t).Finite
The theorem `Set.Finite.diff` states that for any type 'α' and for any set 's' of type 'α', if 's' is a finite set, then for every other set 't' of type 'α', the difference of 's' and 't' (denoted as 's \ t'), which is the set of elements in 's' not in 't', is also a finite set. In other words, the operation of set difference preserves finiteness: subtracting elements from a finite set always results in a finite set.
More concisely: If 's' is a finite set, then the set difference 's \ t' between 's' and any set 't' is also a finite set.
|
Set.Finite.bddAbove
theorem Set.Finite.bddAbove :
∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] [inst_2 : Nonempty α] {s : Set α},
s.Finite → BddAbove s
This theorem states that for any type `α` with a preorder (a binary relation that is reflexive and transitive) and a direction (for any two elements in the set, there is another element that is greater than or equal to both), and for any nonempty set `s` of this type, if the set `s` is finite, then `s` is bounded above. In other words, there exists an element in `α` that is greater than or equal to every element in `s`.
More concisely: If `α` is a type with a preorder and direction, then any nonempty finite subset `s` of `α` has an upper bound.
|
Set.card_le_card
theorem Set.card_le_card :
∀ {α : Type u} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊆ t → Fintype.card ↑s ≤ Fintype.card ↑t
The theorem `Set.card_le_card` states that for any two sets `s` and `t` of an arbitrary type `α`, if set `s` is a subset of set `t` and both sets are finite (`Fintype`), then the cardinality (number of elements) of set `s` is less than or equal to the cardinality of set `t`. In other words, a subset cannot have more elements than its superset when both sets are finite.
More concisely: For any finite sets `s` and `t` of type `α` with `s ⊆ t`, we have `#s ≤ #t`. (Here, `#s` denotes the cardinality of set `s`.)
|
Set.finite_empty
theorem Set.finite_empty : ∀ {α : Type u}, ∅.Finite
This theorem states that for any type `α`, the empty set of type `α` is finite. In other words, no matter what type of elements we are considering, a set with no elements (an empty set) is always considered to be finite.
More concisely: The empty set of any type is a finite set.
|
Set.exists_finite_iff_finset
theorem Set.exists_finite_iff_finset : ∀ {α : Type u} {p : Set α → Prop}, (∃ s, s.Finite ∧ p s) ↔ ∃ s, p ↑s
The theorem `Set.exists_finite_iff_finset` states that for any type `α` and any property `p` applied to a set of type `α`, there exists a finite set `s` such that `s` is finite and `p s` holds if and only if there exists a finite set `s` such that `p ↑s` holds. Here, `↑s` refers to the coercion of `s` from a finite set to a set, and `Set.Finite s` means that the set `s` is finite, i.e., it can be put into a one-to-one correspondence with a set of natural numbers less than some natural number `n`.
More concisely: For any type `α` and property `p`, a set of type `α` is finite if and only if there exists a finite set of elements of type `α` satisfying property `p`.
|
Set.finite_le_nat
theorem Set.finite_le_nat : ∀ (n : ℕ), {i | i ≤ n}.Finite
This theorem states that for any natural number `n`, the set of all natural numbers `i` that are less than or equal to `n` is finite. This is essentially saying that any natural number range starting from 0 and ending in `n` (inclusive) is a finite set. The concept of finiteness here is defined in terms of an equivalence to the set `Fin n`, which is the set of all natural numbers less than `n`.
More concisely: For any natural number `n`, the set {i | i <= n} is finite.
|
Set.Finite.exists_lt_map_eq_of_forall_mem
theorem Set.Finite.exists_lt_map_eq_of_forall_mem :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Infinite α] {t : Set β} {f : α → β},
(∀ (a : α), f a ∈ t) → t.Finite → ∃ a b, a < b ∧ f a = f b
This theorem states that for any types `α` and `β`, given a linear order on `α` and assuming `α` is infinite, if we have a set `t` of type `β` and a function `f` from `α` to `β` such that every element of `α` maps into the set `t`, if the set `t` is finite, then there exists two elements `a` and `b` in `α` where `a` is less than `b` and they map to the same element in `β` under the function `f`. This essentially says that if you have an infinite domain and a finite range, some elements in the domain must map to the same element in the range - a discrete version of the Pigeonhole Principle.
More concisely: Given an infinite linear order `α` and a function `f` from `α` to a finite set `t` of type `β` such that the image of every element in `α` is in `t`, there exist distinct elements `a` and `b` in `α` with `a` less than `b` such that `f(a) = f(b)`.
|
Set.iInter_iUnion_of_monotone
theorem Set.iInter_iUnion_of_monotone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι']
[inst_1 : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst_2 : Nonempty ι'] {s : ι → ι' → Set α},
(∀ (i : ι), Monotone (s i)) → ⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
The theorem `Set.iInter_iUnion_of_monotone` states that if we have a collection of sets indexed by two types `ι` and `ι'`, where `ι` is finite and `ι'` is directed, such that for every element of the first type, the corresponding function from `ι'` to `Set α` is monotone, then the operation of intersecting over `ι'` distributes over the operation of uniting over `ι`. In other words, if we first take the union over `ι` and then intersect over `ι'`, or if we first intersect over `ι'` and then take the union over `ι`, the result is the same. Here, a function is said to be monotone if whenever `a ≤ b`, we have `f a ≤ f b`.
More concisely: Given a collection of sets indexed by finite type `ι` and directed type `ι'` such that the corresponding functions from `ι'` to `Set α` are monotone, the intersection over `ι'` commutes with the union over `ι`.
|
Set.Finite.coeSort_toFinset
theorem Set.Finite.coeSort_toFinset : ∀ {α : Type u} {s : Set α} (hs : s.Finite), { x // x ∈ hs.toFinset } = ↑s := by
sorry
The theorem `Set.Finite.coeSort_toFinset` states that for any finite set `s` of an arbitrary type `α`, there exists an equivalence between the elements `x` that belong to the finset representation of `s` and the elements of the original set `s`. Here, `x` is equipped with a proof that it is in the finset of `s`. However, it should be noted that this is an equality of types, but not a definitional one. Therefore, it should be used with discretion.
More concisely: For any finite set `s` of type `α`, there exists an equivalence between the elements of `s` and their corresponding elements in the finset representation of `s`.
|
Set.Infinite.nonempty
theorem Set.Infinite.nonempty : ∀ {α : Type u} {s : Set α}, s.Infinite → s.Nonempty
The theorem `Set.Infinite.nonempty` states that for any type `α` and any set `s` of type `α`, if `s` is infinite, then `s` is nonempty. In other words, if a set is not finite, it must contain at least one element.
More concisely: If a set is infinite, then it is nonempty.
|
Set.Finite.induction_on
theorem Set.Finite.induction_on :
∀ {α : Type u} {C : Set α → Prop} {s : Set α},
s.Finite → C ∅ → (∀ {a : α} {s : Set α}, a ∉ s → s.Finite → C s → C (insert a s)) → C s
The theorem `Set.Finite.induction_on` is a principle of mathematical induction for finite sets. Given a type `α` and a property `C` that we wish to prove for all finite sets of type `α`, it says the following. If `s` is a finite set, `C` holds for the empty set, and whenever `C` holds for any finite set `s`, it also holds for the set obtained by inserting an element `a` not present in `s` into `s`, then `C` holds for `s`. This is a typical structure of induction: prove something for a base case (here, the empty set), then prove that if it holds for a certain case, it also holds for the next case (here, inserting a new element into the set).
More concisely: The theorem `Set.Finite.induction_on` asserts that if `C` is a property that holds for the empty set of type `α` and is closed under adding an element not in the set, then `C` holds for all finite sets of type `α`.
|
Set.Finite.not_infinite
theorem Set.Finite.not_infinite : ∀ {α : Type u} {s : Set α}, s.Finite → ¬s.Infinite
This theorem states that for any type `α` and any set `s` of type `α`, if the set `s` is finite, then it cannot be infinite. In other words, it's a confirmation of the logical opposite of the statement "an infinite set is not finite". It's essentially restating the mathematical truism that a set cannot be both finite and infinite at the same time.
More concisely: A finite set cannot be infinite.
|
Set.Finite.pi
theorem Set.Finite.pi :
∀ {ι : Type u_1} [inst : Finite ι] {κ : ι → Type u_2} {t : (i : ι) → Set (κ i)},
(∀ (i : ι), (t i).Finite) → (Set.univ.pi t).Finite
This theorem states that the product of finite sets is also finite. More specifically, given an index set `ι` which is finite, a family of sets `t` indexed by `ι`, where each set `t i` is also finite for all `i` in `ι`, the set of all dependent functions (or products) `f : Πa, π a` such that `f a` belongs to `t a` for all `a` in `ι` is also finite. Here, the product is defined with respect to the universal set, which contains all elements of the index set `ι`. In mathematical terms, this theorem can be written as: if ι is a finite set and for every i in ι, t(i) is also a finite set, then ∏ t(i) over all i in ι is also finite.
More concisely: If `ι` is a finite index set and every `t(i)` is a finite set, then the product `∏ t(i)` over all `i` in `ι` is also finite.
|
Set.finite_univ
theorem Set.finite_univ : ∀ {α : Type u} [inst : Finite α], Set.univ.Finite
The theorem `Set.finite_univ` states that for any type `α`, if `α` is finite, then the universal set of `α` is also finite. Here, the universal set of a type `α` refers to the set containing all elements of `α`, and a set is considered finite if there exists a natural number `n` such that there is an equivalence between the set and `Fin n`, the set of natural numbers less than `n`. This theorem essentially bridges the concept of finiteness between the realms of type theory and set theory.
More concisely: If `α` is a finite type, then the universal set of `α` is equivalent to `Fin (|α|)`, where `|α|` denotes the cardinality of `α`.
|
Set.finite_image_iff
theorem Set.finite_image_iff :
∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → ((f '' s).Finite ↔ s.Finite)
The theorem `Set.finite_image_iff` states that for all types `α` and `β`, for all sets `s` of type `α`, and for all functions `f` from `α` to `β`, if `f` is injective on `s`, then the image of `s` under `f` is finite if and only if `s` is finite. In other words, an injective function preserves the finiteness of a set through its image.
More concisely: An injective function maps a finite set to a finite image.
|
Set.eq_of_subset_of_card_le
theorem Set.eq_of_subset_of_card_le :
∀ {α : Type u} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
s ⊆ t → Fintype.card ↑t ≤ Fintype.card ↑s → s = t
The theorem `Set.eq_of_subset_of_card_le` states that for any two sets `s` and `t` of some type `α`, if `s` is a subset of `t` and the cardinality (or the number of elements) of `t` is less than or equal to the cardinality of `s`, then `s` must be equal to `t`. In other words, if `s` is a subset of `t` and there are no more elements in `t` than in `s`, then `s` and `t` must contain exactly the same elements. This theorem is defined under the condition that the power sets of `s` and `t` (denoted by `↑s` and `↑t` respectively) are finite types, meaning they have a finite number of elements.
More concisely: If `s` is a subset of `t` and the cardinality of `t` is less than or equal to that of `s`, then `s` and `t` have the same elements. (Assuming `s` and `t` have finite power sets.)
|
Set.finite_lt_nat
theorem Set.finite_lt_nat : ∀ (n : ℕ), {i | i < n}.Finite
This theorem states that for any natural number 'n', the set of all natural numbers 'i' that are less than 'n' is finite. In mathematical terms, it says that there exists a natural number 'm' and an equivalence between the set `{i | i < n}` and the set `Fin m`, where 'Fin m' is the set of all natural numbers less than 'm'. This result holds for every natural number 'n'.
More concisely: For every natural number 'n', the set of natural numbers less than 'n' is finite and equivalent to the set of natural numbers less than some natural number 'm'.
|
Set.Infinite.image
theorem Set.Infinite.image :
∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → s.Infinite → (f '' s).Infinite
This theorem states that if a function `f` is injective (i.e., distinct inputs produce distinct outputs) when restricted to a set `s`, and if the set `s` is infinite, then the image of `s` under `f` is also infinite. In other words, mapping an infinite set through an injective function results in another infinite set.
More concisely: If `f` is an injective function on the infinite set `s`, then the image `f(s)` is also infinite.
|
Set.finite_or_infinite
theorem Set.finite_or_infinite : ∀ {α : Type u} (s : Set α), s.Finite ∨ s.Infinite
The theorem `Set.finite_or_infinite` states that for any set `s` of an arbitrary type `α`, the set `s` is either finite or infinite. In other words, given any set `s`, there exists a logical disjunction - `s` is a finite set (there exists a natural number `n` and an equivalence between the set `s` and `Fin n`), or `s` is an infinite set (it is not finite). This theorem provides a comprehensive partition of all sets into two mutually exclusive categories: finite and infinite sets.
More concisely: Every set can be classified as either finite or infinite.
|
Set.Infinite.mono
theorem Set.Infinite.mono : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Infinite → t.Infinite
This theorem, referred to as `Set.Infinite.mono`, states that for any type `α` and any two sets `s` and `t` of this type, if `s` is a subset of `t` and `s` is an infinite set, then `t` is also an infinite set. It asserts the preservation of the property of infiniteness under the operation of set inclusion, meaning that if an infinite set is contained within another set, the latter set must also be infinite.
More concisely: If `s` is a subset of `t` and `s` is an infinite set, then `t` is also infinite.
|
Set.infinite_coe_iff
theorem Set.infinite_coe_iff : ∀ {α : Type u} {s : Set α}, Infinite ↑s ↔ s.Infinite
The theorem `Set.infinite_coe_iff` states that for any type `α` and any set `s` of type `α`, the set `s` is infinite if and only if its co-domain is infinite. In other words, a set `s` in Lean is considered infinite if its mapping to another type (via the ↑ coe function) is also infinite, and vice versa. This is a characterization of the infiniteness of a set in terms of its co-domain.
More concisely: A set is infinite if and only if its image under the coercion function is an infinite type.
|
Set.Finite.toFinset_mono
theorem Set.Finite.toFinset_mono :
∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, s ⊆ t → hs.toFinset ⊆ ht.toFinset
The theorem `Set.Finite.toFinset_mono` states that for any two sets `s` and `t` of some type `α`, if `s` is a subset of `t` and both `s` and `t` are finite sets, then the finite set representation (`Finset`) of `s` is a subset of the finite set representation of `t`. In other words, the process of converting a finite set to the `Finset` data type preserves subset relationships.
More concisely: If `s` is a finite subset of `t`, then the `Finset` representations `Finset.univ s` and `Finset.univ t` satisfy `Finset.subset (Finset.univ s) (Finset.univ t)`.
|
Set.Finite.offDiag
theorem Set.Finite.offDiag : ∀ {α : Type u} {s : Set α}, s.Finite → s.offDiag.Finite
The theorem `Set.Finite.offDiag` states that for any type `α` and any set `s` of that type, if `s` is finite then the off-diagonal of `s` is also finite. The off-diagonal of a set `s` is defined as the set of all pairs `(a, b)` such that `a` and `b` are elements of `s` and `a` is not equal to `b`. This theorem essentially indicates that the set of all distinct pairs from a finite set is also finite.
More concisely: If `α` is a type and `s` is a finite set of `α`, then the set of distinct pairs in `s` is finite.
|
Set.Finite.finite_subsets
theorem Set.Finite.finite_subsets : ∀ {α : Type u} {a : Set α}, a.Finite → {b | b ⊆ a}.Finite
This theorem states that for any finite set `a` of a certain type `α`, the collection of all subsets of `a` is also finite. In other words, if we have a finite set, then there are finitely many subsets of that set. This is formally written as, given a set `a` of type `α`, if `a` is finite (`a.Finite`), then the set of all subsets `b` of `a` (`{b | b ⊆ a}`) is also finite.
More concisely: If `α` is a type and `a` is a finite set of type `α`, then the collection of all subsets of `a` is also finite.
|
Set.Finite.fin_embedding
theorem Set.Finite.fin_embedding : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ n f, Set.range ⇑f = s
The theorem `Set.Finite.fin_embedding` states that for any type `α` and any set `s` of type `α`, if the set `s` is finite, then there exists a natural number `n` and a function `f` such that the range of `f` is exactly the set `s`. In other words, every finite set `s` of elements of some type `α` can be put into one-to-one correspondence (or "embedded") with a finite subset of the natural numbers, specified by the function `f`. This function `f` is essentially encoding the index of each element in the set `s`, allowing us to map each element of `s` to a unique natural number in the range 0 to `n-1`, where `n` is the size of the set `s`.
More concisely: Every finite set can be embedded as a subset of the natural numbers.
|
Multiset.finite_toSet
theorem Multiset.finite_toSet : ∀ {α : Type u} (s : Multiset α), {x | x ∈ s}.Finite
The theorem `Multiset.finite_toSet` states that, for any multiset `s` of type `α`, the set of elements `{x | x ∈ s}` that are in `s` is finite. In other words, it asserts that if we take a multiset and construct a set by considering all of its elements, the resulting set will always be finite. This is essentially a property linking multisets to finite sets.
More concisely: The theorem `Multiset.finite_toSet` asserts that the set of elements in a multiset is finite.
|
Mathlib.Data.Set.Finite._auxLemma.4
theorem Mathlib.Data.Set.Finite._auxLemma.4 :
∀ {α : Type u} {s : Set α} (hs : s.Finite), hs.toFinset.Nonempty = s.Nonempty
This theorem states that for any type `α` and any set `s` of type `α`, if `s` is finite (denoted by `hs : Set.Finite s`), then the non-emptiness of the `Finset` associated with `s` (obtained by calling `Set.Finite.toFinset hs`) is equivalent to the non-emptiness of `s` itself (`Set.Nonempty s`). In other words, a set `s` in our context is non-empty if and only if its corresponding `Finset` is non-empty.
More concisely: For any set `s` of type `α`, its `Finset` is non-empty if and only if `s` itself is non-empty, assuming `s` is finite.
|
Finset.finite_toSet
theorem Finset.finite_toSet : ∀ {α : Type u} (s : Finset α), (↑s).Finite
This theorem states that for any finset `s` of type `α`, when `s` is coerced to a set, it is a finite set. In other words, any finset can be considered a finite set. This is a wrapper around the `Set.toFinite` function, meaning it is providing a more specific or convenient interface for the existing function `Set.toFinite`.
More concisely: For any finset `s` of type `α`, the coerced set `{x | x ∈ s}` is a finite set.
|
Set.Finite.prod
theorem Set.Finite.prod : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β}, s.Finite → t.Finite → (s ×ˢ t).Finite
The theorem `Set.Finite.prod` states that for any two types `α` and `β`, and any two sets `s` and `t` where `s` is a set of type `α` and `t` is a set of type `β`, if both `s` and `t` are finite sets, then the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is also a finite set. In other words, if we have finite sets from two different types, their Cartesian product will also form a finite set.
More concisely: If `α` and `β` are types and `s : Set α` and `t : Set β` are finite sets, then `s ×ˢ t` is a finite set.
|
Set.Finite.infinite_compl
theorem Set.Finite.infinite_compl : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → sᶜ.Infinite
The theorem `Set.Finite.infinite_compl` states that for any type `α` that is infinite, and for any set `s` of type `α` that is finite, the complement of `s` (denoted by `sᶜ`) is infinite. In other words, removing a finite set from an infinite set results in another infinite set.
More concisely: For any infinite type `α` and finite set `s` of type `α`, the complement of `s` is infinite.
|
Set.not_infinite
theorem Set.not_infinite : ∀ {α : Type u} {s : Set α}, ¬s.Infinite ↔ s.Finite
This theorem states that for any given set `s` of some type `α`, the set `s` is not infinite if and only if it is finite. In other words, in the context of sets, the property of not being infinite is equivalent to the property of being finite. This is a direct consequence of the definitions of finiteness and infiniteness for sets in Lean 4, where a set is finite if and only if it is not infinite.
More concisely: A set is finite if and only if it is not infinite.
|
Set.finite_range
theorem Set.finite_range : ∀ {α : Type u} {ι : Sort w} (f : ι → α) [inst : Finite ι], (Set.range f).Finite
The theorem `Set.finite_range` states that for all types `α` and `ι`, given a function `f` from `ι` to `α` and assuming that `ι` is finite (`inst : Finite ι`), the range of `f` is also finite. In other words, if the domain of a function is finite, then the set of all output values (the range) of the function is also finite.
More concisely: If `ι` is a finite type, then the range of a function `f : ι → α` is a finite set.
|
Set.Finite.induction_to_univ
theorem Set.Finite.induction_to_univ :
∀ {α : Type u} [inst : Finite α] {C : Set α → Prop} (S0 : Set α),
C S0 → (∀ (S : Set α), S ≠ Set.univ → C S → ∃ a ∉ S, C (insert a S)) → C Set.univ
The theorem `Set.Finite.induction_to_univ` states that for any finite type `α`, if a property `C` holds for a set `S0` and, for any set `S` that is not the universal set, if `C` holds for `S` then there exists an element `a` not in `S` such that `C` holds for the set obtained by inserting `a` into `S`, then `C` holds for the universal set. This can be seen as a form of induction up to the universal set, where the base case is `C` holding for `S0` and the inductive step involves adding an element not already in the set.
More concisely: If `α` is finite and `C` holds for an empty set `S0` and for any set `S` not equal to the universal set, if `C` holds for `S` then there exists an `a` not in `S` such that `C` holds for `S ∪ {a}`, then `C` holds for the universal set.
|
Set.Finite.coe_toFinset
theorem Set.Finite.coe_toFinset : ∀ {α : Type u} {s : Set α} (hs : s.Finite), ↑hs.toFinset = s
This theorem states that for any type `α` and any set `s` of elements of type `α`, if `s` is a finite set, then the conversion of the `Finset` representing `s` back into a set is equal to `s` itself. Here, `Finset` is a type of finite sets in Lean 4. The `Set.Finite.toFinset` function is used to get the `Finset` that represents the finite set `s`, while `↑` is used to convert this `Finset` back into a set. The theorem ensures the consistency of conversion between sets and `Finset`s for finite sets.
More concisely: For any finite set `s` of type `α`, the conversion of `s` to a `Finset` and back to a set is equal to the original set `s`.
|
Set.Finite.exists_maximal_wrt
theorem Set.Finite.exists_maximal_wrt :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] (f : α → β) (s : Set α),
s.Finite → s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
This theorem states that for any set `s` of some type `α`, where `s` is both finite and nonempty, and for any function `f` from `α` to another type `β` that has a partial order, there exists an element `a` in `s` such that `f(a)` is maximal with respect to `f` over all elements in `s`. In other words, for all other elements `a'` in `s`, if `f(a')` is not less than `f(a)`, then `f(a')` must be equal to `f(a)`. This is essentially a statement about the existence of maximal elements under a function `f` in a finite and nonempty set.
More concisely: Given a finite and nonempty set `s` of type `α` and a function `f` from `α` to a partially ordered type `β`, there exists an element `a` in `s` such that for all `a'` in `s`, `f(a) ≤ f(a')` implies `f(a) = f(a')`.
|
Set.Finite.inter_of_left
theorem Set.Finite.inter_of_left : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (s ∩ t).Finite
This theorem states that for any type `α`, and any set `s` of type `α`, if `s` is finite, then for any other set `t` of type `α`, the intersection of `s` and `t` is also finite. In other words, the intersection of a finite set with any other set results in a finite set.
More concisely: If `α` is a type and `s` and `t` are finite sets of type `α`, then the intersection `s INTER t` is also a finite set.
|
Mathlib.Data.Set.Finite._auxLemma.28
theorem Mathlib.Data.Set.Finite._auxLemma.28 : ∀ {α : Type u} (a : α), {a}.Finite = True
The theorem `Mathlib.Data.Set.Finite._auxLemma.28` states that for all types `α` and any element `a` of type `α`, the set containing only the element `a` is finite. This is trivially true as the set contains exactly one element, hence there exists a natural number `n` (in this case, `n` is 1) and an equivalence between the set `{a}` and the finite set `Fin n`, satisfying the definition of a finite set.
More concisely: The set consisting of a single element is finite.
|
Set.Finite.preimage
theorem Set.Finite.preimage :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, Set.InjOn f (f ⁻¹' s) → s.Finite → (f ⁻¹' s).Finite
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is injective on the preimage of a set `s` under `f`, and if the set `s` is finite, then the preimage of `s` under `f` is also finite.
In other words, if we have a function that does not map different elements to the same value within the preimage of a set, and if that set has a finite number of elements, then the preimage of the set (i.e., all the elements in the domain that map to elements in the set) must also have a finite number of elements.
More concisely: If `f : α → β` is a function, `s ⊆ β` is finite, and the restriction of `f` to the preimage of `s` is injective, then the preimage of `s` under `f` is also finite.
|
Set.finite_univ_iff
theorem Set.finite_univ_iff : ∀ {α : Type u}, Set.univ.Finite ↔ Finite α
This theorem states that, for any type `α`, the universal set `Set.univ` of `α` is finite if and only if the type `α` itself is finite. In other words, there exists a natural number `n` and an equivalence between `Set.univ` and `Fin n` if and only if such an `n` and equivalence exist for `α`. This tells us that the finiteness property is preserved between a type and its associated universal set.
More concisely: The universal set of a type is finite if and only if the type itself is finite.
|
Finite.of_forall_not_lt_lt
theorem Finite.of_forall_not_lt_lt :
∀ {α : Type u} [inst : LinearOrder α], (∀ ⦃x y z : α⦄, x < y → y < z → False) → Finite α
This theorem states that for any type `α` which has a linear order, if there does not exist any triple of elements `x`, `y`, `z` such that `x < y < z`, then the type `α` is finite. In simpler terms, if you cannot find three distinct elements in this type that are ordered in ascending order, then there are a finite number of elements in this type.
More concisely: If a type `α` with a linear order has no three-element chain `x < y < z`, then `α` is finite.
|
Finset.bddAbove
theorem Finset.bddAbove : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : Nonempty α] (s : Finset α), BddAbove ↑s
The theorem `Finset.bddAbove` states that for any given finite set (`Finset`) `s` of a certain type `α`, where `α` is a semilattice with a supremum operation and is nonempty, there exists an upper bound for `s`. In other words, every finite set in a nonempty semilattice is bounded above.
More concisely: Every nonempty finite set in a semilattice with a supremum operation has an upper bound.
|
Finite.Set.subset
theorem Finite.Set.subset : ∀ {α : Type u} (s : Set α) {t : Set α} [inst : Finite ↑s], t ⊆ s → Finite ↑t
This theorem states that for any set `s` of type `α`, and another set `t` of the same type, if `s` is finite and `t` is a subset of `s`, then `t` is also finite. In other words, the theorem establishes that any subset of a finite set is also finite. This is a fundamental property in set theory.
More concisely: If `s` is a finite set and `t` is a subset of `s`, then `t` is also finite.
|
Set.Finite.exists_minimal_wrt'
theorem Set.Finite.exists_minimal_wrt' :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] (f : α → β) (s : Set α),
(f '' s).Finite → s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'
This theorem is a variant of `Finite.exists_minimal_wrt`, which allows for a weaker hypothesis that the image of a set `s` under a function `f` is finite, rather than the set `s` itself being finite. Given a set `s` of elements of type `α` and a function `f` from `α` to a partially ordered type `β`, if the image of `s` under `f` is finite and `s` is nonempty, then there exists an element `a` in `s` such that for all other elements `a'` in `s`, if `f(a')` is less than or equal to `f(a)`, then `f(a')` equals `f(a)`. In other words, the theorem asserts the existence of an element in `s` with a minimal value under `f`, in the sense that no other element of `s` maps to a strictly smaller value under `f`.
More concisely: Given a nonempty set `s` of elements from a type `α` and a function `f` from `α` to a partially ordered type `β` with finite image, there exists an element `a` in `s` such that for all `a'` in `s`, if `f(a') ≤ f(a)`, then `f(a') = f(a)`.
|
Set.Finite.bddAbove_biUnion
theorem Set.Finite.bddAbove_biUnion :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] [inst_2 : Nonempty α]
{I : Set β} {S : β → Set α}, I.Finite → (BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i))
The theorem `Set.Finite.bddAbove_biUnion` states that for all types `α` and `β` where `α` is a preorder and is directed, and where `α` is non-empty, for a set `I` of type `β` and a function `S` mapping `β` to a set of `α`, if `I` is finite, then the union of all sets `S i` where `i` is an element of `I` is bounded above if and only if all the sets `S i` for every `i` in `I` are bounded above. This means that a finite union of sets, where each set is bounded above, is still bounded above.
More concisely: For a preorder type `α` that is directed, non-empty, and has a finite set `I` of elements, the union of images `S i` under a function `S : β → Set α` is bounded above if and only if each image `S i` is bounded above for `i` in `I`.
|
Set.toFinite
theorem Set.toFinite : ∀ {α : Type u} (s : Set α) [inst : Finite ↑s], s.Finite
The theorem `Set.toFinite` provides a method to create a finite set. Specifically, if `s` is a set of elements of some type `α`, and `s` has an instance of `Finite`, then `s` is a finite set according to the definition `Set.Finite`. In other words, if we can establish an equivalence between `s` and a finite subtype (say, there exists a natural number `n` and an equivalence `s ≃ Fin n`), then `s` is considered a finite set.
More concisely: Given a set `s` of type `α` with a finite instance, `s` is equivalent to a finite subtype `Fin n` for some natural number `n`, making `s` a finite set.
|
Set.Finite.nonempty_fintype
theorem Set.Finite.nonempty_fintype : ∀ {α : Type u} {s : Set α}, s.Finite → Nonempty (Fintype ↑s)
This theorem, known as the **Alias of the forward direction of `Set.finite_def`**, states that for any type `α` and any set `s` of type `α`, if the set `s` is finite, then there exists a `Fintype` (a finite type) whose elements are drawn from the set `s`. In other words, every finite set `s` has a corresponding `Fintype` structure. This theorem emphasizes that the concept of finite sets and finite types are closely related in Lean 4.
More concisely: For any finite set `s` of type `α` in Lean 4, there exists a `Fintype` structure `F : Fintype α` such that `s = range (coe : F.to_fun)`.
|
Finite.of_finite_univ
theorem Finite.of_finite_univ : ∀ {α : Type u}, Set.univ.Finite → Finite α
This theorem, denoted as `Finite.of_finite_univ`, asserts that for any type `α`, if the universal set of `α` (i.e., the set containing all elements of `α`) is finite, then the type `α` itself is finite. In other words, it directly connects the finiteness of the universal set on a type with the finiteness of the type itself. This is an alias of the forward direction of the theorem `Set.finite_univ_iff`.
More concisely: If the universal set of a type `α` is finite, then `α` is a finite type.
|
Set.Subsingleton.finite
theorem Set.Subsingleton.finite : ∀ {α : Type u} {s : Set α}, s.Subsingleton → s.Finite
The theorem `Set.Subsingleton.finite` states that for any type `α` and any set `s` of type `α`, if `s` is a subsingleton (i.e., it contains at most one element), then `s` is finite. In other words, all subsingleton sets are finite. This theorem guarantees that any set with the property of having at most one element is finite.
More concisely: A subsingleton set is finite.
|
Set.Finite.iSup_biInf_of_monotone
theorem Set.Finite.iSup_biInf_of_monotone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [inst_1 : Nonempty ι']
[inst_2 : IsDirected ι' fun x x_1 => x ≤ x_1] [inst_3 : Order.Frame α] {s : Set ι},
s.Finite → ∀ {f : ι → ι' → α}, (∀ i ∈ s, Monotone (f i)) → ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
This theorem, `Set.Finite.iSup_biInf_of_monotone`, states that for any two types `ι` and `ι'`, where `ι'` is a preordered set and is also nonempty and directed with respect to the order relation, and for any type `α` which forms a frame, and any finite set `s` of elements of type `ι`, the following holds: if we have a function `f` from `ι` to `ι'` to `α` such that for every element `i` in the set `s`, the function `f i` is monotone, then the supremum of the infimum (over elements in the set `s`) of `f i j` over all `j` is equal to the infimum (over elements in the set `s`) of the supremum of `f i j` over all `j`.
In mathematical notation, this is saying that $\sup_j \inf_{i \in s} f(i, j) = \inf_{i \in s} \sup_j f(i, j)$ provided that each function $f(i, \cdot)$ is monotone for each $i \in s$ and the set $s$ is finite. This is a generalisation of the min-max theorem in order theory.
More concisely: For a finite, nonempty and directed preordered set `ι`, type `α` forming a frame, and monotone functions `f : ι → ι' → α`, the supremum of the infimum of `f i j` over `i ∈ s` and `j` is equal to the infimum of the supremum of `f i j` over `i ∈ s` for any finite set `s ⊆ ι`.
|
Set.Finite.bddBelow_biUnion
theorem Set.Finite.bddBelow_biUnion :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] [inst_2 : Nonempty α]
{I : Set β} {S : β → Set α}, I.Finite → (BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i))
The given theorem states that for any types `α` and `β`, given a preorder relationship on `α` and a directed relationship where for any two elements the first is greater or equal to the second, and assuming `α` is nonempty, for any set `I` of type `β` and a function `S` mapping elements of `β` to sets of `α`, if `I` is finite, then the union of all sets `S i` for `i` in `I` is bounded below if and only if each individual set `S i` is bounded below. In other words, a finite union of sets, all of which are bounded below is itself bounded below.
More concisely: For any preorders on types `α` and `β`, if `α` is nonempty and for every `i` in a finite set `I` of type `β`, `S i` subset of `α` is bounded below, then their union is also bounded below.
|
Mathlib.Data.Set.Finite._auxLemma.3
theorem Mathlib.Data.Set.Finite._auxLemma.3 :
∀ {α : Type u} {s : Set α} {a : α} (hs : s.Finite), (a ∈ hs.toFinset) = (a ∈ s)
This theorem states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, the membership of `a` in the finite set `s` is equivalent to the membership of `a` in the finset obtained from the set `s`. In other words, an element `a` belongs to the finset representation of a finite set `s` if and only if `a` belongs to the set `s`.
More concisely: For any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, `a` is in the finite set `s` if and only if `a` is in the finset obtained from `s`.
|
Set.Finite.ofFinset
theorem Set.Finite.ofFinset : ∀ {α : Type u} {p : Set α} (s : Finset α), (∀ (x : α), x ∈ s ↔ x ∈ p) → p.Finite := by
sorry
This theorem is about constructing a `Finite` instance for a set from a `Finset`. Given a type `α`, a set `p` of type `Set α`, and a `Finset α` `s`, if each element `x` of type `α` belongs to `s` if and only if it belongs to `p`, then the set `p` is finite. In other words, this theorem states that if a set and a finite set (`Finset`) have exactly the same elements, then the set is also finite.
More concisely: If a set `p` has the same elements as a finite set `s` of type `Finset`, then `p` is also a finite set.
|
Set.Finite.subset
theorem Set.Finite.subset : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ {t : Set α}, t ⊆ s → t.Finite
This theorem states that for any type `α` and any set `s` of type `α` that is finite, if we have another set `t` of the same type `α` such that every element of `t` is also an element of `s` (i.e., `t` is a subset of `s`), then `t` is also finite. This is a generalization of the principle that a subset of a finite set is always finite.
More concisely: If `s` is a finite set of type `α`, then any subset `t` of `s` also has finite size.
|
Set.Finite.biUnion'
theorem Set.Finite.biUnion' :
∀ {α : Type u} {ι : Type u_1} {s : Set ι},
s.Finite →
∀ {t : (i : ι) → i ∈ s → Set α},
(∀ (i : ι) (hi : i ∈ s), (t i hi).Finite) → (⋃ i, ⋃ (h : i ∈ s), t i h).Finite
This theorem, `Set.Finite.biUnion'`, is a dependent version of the theorem `Finite.biUnion`. It states that for any type `α`, index type `ι`, and a finite set `s` of type `ι`, if for each element `i` of `s`, the dependent set `t i` indexed by `i` and predicated on `i` being an element of `s`, is finite, then the union of all such `t i` is also finite. This theorem is expressed over elements of `s` and their corresponding dependent sets, and it generalizes the concept of union of two finite sets being finite to an indexed family of sets.
More concisely: If `ι` is a finite type and for each `i` in `ι`, the dependent set `t i` indexed by `i` is finite, then the union of all `t i` is also finite.
|
Set.infinite_univ
theorem Set.infinite_univ : ∀ {α : Type u} [h : Infinite α], Set.univ.Infinite
This theorem states that for any type `α` that is infinite, the universal set of `α`, denoted by `Set.univ`, is also infinite. Here, `Infinite α` is a hypothesis which asserts the infiniteness of the type `α`, and `Set.Infinite` is a property of a set that it is not finite. Therefore, the theorem essentially states that the infiniteness of a type implies the infiniteness of the universal set over that type.
More concisely: If `α` is an infinite type, then `Set.univ (α : Type)` is an infinite set.
|
Set.Finite.image
theorem Set.Finite.image : ∀ {α : Type u} {β : Type v} {s : Set α} (f : α → β), s.Finite → (f '' s).Finite
The theorem `Set.Finite.image` asserts that for all types `α` and `β`, and for any set `s` of type `α`, if a function `f` is applied from `α` to `β` and if the original set `s` is finite, then the image of the set `s` under the function `f`, i.e., the set of all `f(x)` for `x` in `s`, is also finite. In other words, the image of a finite set under any function is also finite.
More concisely: If `f` is a function and `s` is a finite set, then the image of `s` under `f`, i.e., `{f(x) | x ∈ s}`, is also a finite set.
|
Set.finite_singleton
theorem Set.finite_singleton : ∀ {α : Type u} (a : α), {a}.Finite
This theorem states that for any given type `α` and any element `a` of type `α`, the singleton set containing only `a` is finite. In other words, the set `{a}` for any `a` in the universe of discourse `α` is always finite. This is intuitive as a singleton set only contains one element, and therefore its size can be explicitly counted as one, making it finite.
More concisely: For any type `α` and element `a` of type `α`, the singleton set `{a}` is a finite set with cardinality 1.
|
Set.iInter_iUnion_of_antitone
theorem Set.iInter_iUnion_of_antitone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι']
[inst_1 : IsDirected ι' fun x x_1 => x ≤ x_1] [inst_2 : Nonempty ι'] {s : ι → ι' → Set α},
(∀ (i : ι), Antitone (s i)) → ⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
The theorem `Set.iInter_iUnion_of_antitone` states that for any types `ι`, `ι'`, and `α`, given a finite indexing set `ι`, and a preordered `ι'` which is directed and nonempty, if we have a family of antitone functions `s` from `ι` to `ι'` to the set of `α`, then the intersection over `ι'` of the union over `ι` of `s i j` is equal to the union over `ι` of the intersection over `ι'` of `s i j`. In simpler terms, this theorem asserts that for these specific conditions, the operation of decreasing intersection distributes over finite union.
More concisely: For any types `ι`, `ι'`, and `α`, given a finite indexing set `ι`, and a preordered `ι'` which is directed and nonempty, if `s` is a family of antitone functions from `ι` to `ι'` to the set of `α`, then the intersection over `ι'` of the union over `ι` of `s i j` equals the union over `ι` of the intersections over `ι'` of `s i j`.
|
Set.finite_coe_iff
theorem Set.finite_coe_iff : ∀ {α : Type u} {s : Set α}, Finite ↑s ↔ s.Finite
This theorem states that for any set `s` of type `α`, the set `s` is finite if and only if the subtype corresponding to `s` is also finite. In other words, it establishes the equivalence between the finiteness of a set and the finiteness of its corresponding subtype. This can be represented mathematically as `Finite ↑s ↔ Set.Finite s`, where `Finite ↑s` refers to the finiteness of the subtype corresponding to set `s` and `Set.Finite s` refers to the finiteness of set `s`.
More concisely: A set `s` is finite if and only if its subtype is finite. (In Lean: `Finite ↑s ↔ Set.Finite s`)
|
Mathlib.Data.Set.Finite._auxLemma.15
theorem Mathlib.Data.Set.Finite._auxLemma.15 : ∀ {α : Type u} {s : Set α} {h : s.Finite}, (h.toFinset = ∅) = (s = ∅)
This theorem states that for any given type `α` and any set `s` of that type, if the set `s` is finite (denoted by `h : Set.Finite s`), then the finiteness of the set `s` being converted to a finite set (using the `Set.Finite.toFinset` function) equals the empty set if and only if the set `s` itself equals the empty set. In other words, the conversion of a finite set to a finite set results in an empty set if and only if the original set was empty.
More concisely: For any type `α` and finite set `s` of that type, `Set.Finite.toFinset s = {} <> s` if and only if `s = {}`.
|
Set.Finite.induction_to
theorem Set.Finite.induction_to :
∀ {α : Type u} {C : Set α → Prop} {S : Set α},
S.Finite → ∀ S0 ⊆ S, C S0 → (∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) → C S
This theorem states the principle of induction over a finite set `S` of an arbitrary type `α`. Specifically, if a property `C` holds for a subset `S0` of `S`, and for any proper subset `s` of `S` on which `C` holds, there exists an element `a` in the difference of `S` and `s` such that `C` also holds on the set resulting from inserting `a` into `s`, then the property `C` must hold for the whole set `S`. This principle is analogous to the induction principle for natural numbers, but applied to finite sets.
More concisely: If a property holds for a finite set and holds for any proper subset with an element added such that the property also holds for the new subset, then the property holds for the entire set.
|
Set.Finite.bddBelow
theorem Set.Finite.bddBelow :
∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] [inst_2 : Nonempty α] {s : Set α},
s.Finite → BddBelow s
The theorem states that any finite set is bounded below. More specifically, for all types `α` that have a preorder and are directed, and for all nonempty sets of this type `s`, if `s` is finite then it is also bounded below. Here being "bounded below" means that there exists an element that is less than or equal to every element in the set. Being "directed" means that for every pair of elements in `α`, there is another element that is greater or equal to both.
More concisely: For any finite, directed set `s` of type `α` with a preorder, there exists a lower bound.
|
Set.Finite.toFinset_strictMono
theorem Set.Finite.toFinset_strictMono :
∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, s ⊂ t → hs.toFinset ⊂ ht.toFinset
This theorem, named `Set.Finite.toFinset_strictMono`, states that for any two sets `s` and `t` of any type `α`, if both `s` and `t` are finite, then if `s` is a strict subset of `t` (i.e., `s` is a subset of `t` but `s` is not equal to `t`), the conversion of `s` to a finite set is also a strict subset of the conversion of `t` to a finite set. This theorem is actually an alias of the reverse direction of another theorem `Set.Finite.toFinset_ssubset_toFinset`.
More concisely: For any finite sets `s` and `t` of type `α`, if `s` is a strict subset of `t`, then the conversion of `s` to a finite set is a strict subset of the conversion of `t` to a finite set.
|
Set.Finite.of_preimage
theorem Set.Finite.of_preimage :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, (f ⁻¹' s).Finite → Function.Surjective f → s.Finite
The theorem `Set.Finite.of_preimage` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `β`, if the preimage of `s` under `f` is a finite set and `f` is a surjective function, then `s` is a finite set.
In other words, it says that if you have a map that covers all elements of the codomain and the set of elements from the domain that map to a specific set in the codomain is finite, then that specific set is also finite. This theorem establishes a relationship between the finiteness of sets and the properties of the functions that map to them.
More concisely: If a function from a type to a type is surjective and its preimage of a finite set is finite, then that set is finite.
|
Set.Finite.mem_toFinset
theorem Set.Finite.mem_toFinset : ∀ {α : Type u} {s : Set α} {a : α} (hs : s.Finite), a ∈ hs.toFinset ↔ a ∈ s := by
sorry
The theorem `Set.Finite.mem_toFinset` states that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, if `s` is a finite set, then `a` belongs to the `Finset` representation of `s` if and only if `a` belongs to `s`. Here, `Finset` refers to a finite set in Lean, and `Set.Finite.toFinset` is a function that converts a finite set into its `Finset` representation. This theorem essentially establishes the membership equivalence between a set and its `Finset` representation when the set is finite.
More concisely: For any type `α` and finite set `s` of type `α`, an element `a` belongs to `s` if and only if `a` is in the `Finset` representation `Set.Finite.toFinset s`.
|
Set.Finite.biUnion
theorem Set.Finite.biUnion :
∀ {α : Type u} {ι : Type u_1} {s : Set ι},
s.Finite → ∀ {t : ι → Set α}, (∀ i ∈ s, (t i).Finite) → (⋃ i ∈ s, t i).Finite
The theorem `Set.Finite.biUnion` states that for any type `α` and index type `ι`, given a set `s` of index type `ι`, if `s` is finite and for any index `i` in `s`, the set `t i` (where `t` is a function from `ι` to sets of `α`) is also finite, then the union of the sets `t i` over all `i` in `s` is finite as well. In mathematical terms, if we have a finite set of indices and each index corresponds to a finite set, then the union of all these finite sets is also a finite set.
More concisely: If `ι` is a finite type and for each `i` in `ι`, `t i` is a finite set, then the union of `{ti : i ∈ ι}` is finite.
|
Set.seq_of_forall_finite_exists
theorem Set.seq_of_forall_finite_exists :
∀ {γ : Type u_1} {P : γ → Set γ → Prop},
(∀ (t : Set γ), t.Finite → ∃ c, P c t) → ∃ u, ∀ (n : ℕ), P (u n) (u '' Set.Iio n)
This theorem states that for any type `γ` and any relation `P` between elements of `γ` and sets of `γ`, if every finite set `t` of type `γ` has some element `c` of `γ` that is related to it through `P`, then there exists a recursively defined sequence `u` in `γ` such that for every natural number `n`, the `n`th element of sequence `u`, denoted `u n`, is related through `P` to the image of the set `{0, 1, ..., n-1}` under the sequence `u`. This set `{0, 1, ..., n-1}` is represented as `Set.Iio n`, which refers to the left-infinite right-open interval `{x | x < n}`. This theorem is used later to demonstrate that sequentially compact sets are totally bounded.
More concisely: If every finite set has an element related to it via a relation P, then there exists a recursively defined sequence u in a type γ such that for each natural number n, the n-th element of u is related to the set {0, 1, ..., n-1} through P.
|
Set.Finite.exists_finset_coe
theorem Set.Finite.exists_finset_coe : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ s', ↑s' = s
This theorem states that for every set `s` of any type `α`, if `s` is a finite set (`Set.Finite s`), then there exists a finset `s'` such that the conversion of `s'` to a set is equal to `s`. In other words, any finite set can be represented as a finset in Lean.
More concisely: Given any finite set `s` of type `α` in Lean, there exists a finset `s'` such that `s'` is equal to `s` as sets.
|
Mathlib.Data.Set.Finite._auxLemma.29
theorem Mathlib.Data.Set.Finite._auxLemma.29 :
∀ {α : Type u} (a : α) {s : Set α}, s.Finite → (insert a s).Finite = True
This theorem states that for any type `α`, any element `a` of type `α`, and any set `s` of type `α`, if the set `s` is finite, then the set resulting from inserting the element `a` into `s` is also finite. Thus, adding an element to a finite set maintains the finiteness of the set.
More concisely: If `α` is a type, `a : α`, and `s : set α` is finite, then `a ∈ s` implies `s.insert a` is finite.
|
Mathlib.Data.Set.Finite._auxLemma.27
theorem Mathlib.Data.Set.Finite._auxLemma.27 : ∀ {α : Type u}, ∅.Finite = True
This theorem states that for any type `α`, the empty set of that type is always finite. In other words, regardless of what type you're dealing with, if you have an empty set of that type, it is considered as finite. It is one of the fundamental properties of finite sets in mathematics.
More concisely: The empty set of any type is a finite set.
|
Finset.bddBelow
theorem Finset.bddBelow : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : Nonempty α] (s : Finset α), BddBelow ↑s
This theorem states that for any finite set `s` in an arbitrary type `α`, which is equipped with a semilattice structure and is nonempty, the set `s` is bounded below. In other words, there exists a lower bound for the set `s`. The semilattice structure on the type `α` provides the necessary order relation to discuss concepts such as lower bounds.
More concisely: For any finite, nonempty semilattice `s` in type `α`, there exists a bottom element.
|
Set.iUnion_iInter_of_antitone
theorem Set.iUnion_iInter_of_antitone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι']
[inst_1 : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst_2 : Nonempty ι'] {s : ι → ι' → Set α},
(∀ (i : ι), Antitone (s i)) → ⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
The theorem `Set.iUnion_iInter_of_antitone` states that for any type `ι` that is finite, a type `ι'` that is ordered in a preorder relationship and directed when the order is swapped, and a nonempty type `α`, if `s` is a function from `ι` and `ι'` to a set of `α` such that for each `i` in `ι`, `s i` is an antitone function (a function `f` is antitone if `a ≤ b` implies `f b ≤ f a`), then the union over `j` of the intersection over `i` of `s i j` is equal to the intersection over `i` of the union over `j` of `s i j`. In other words, this theorem states that a decreasing union distributes over a finite intersection.
More concisely: For any finite type `ι`, ordered preorder `ι'`, nonempty type `α`, and antitone function `s` from `ι` to `ι'` to sets of `α`, the union over `j` of the intersection over `i` of `s i j` equals the intersection over `i` of the union over `j` of `s i j`.
|
Set.Finite.to_subtype
theorem Set.Finite.to_subtype : ∀ {α : Type u} {s : Set α}, s.Finite → Finite ↑s
This theorem states that for any set `s` of a certain type `α`, if `s` is finite (as defined by `Set.Finite`), then the subtype corresponding to `s` (denoted by `↑s`) is also finite. This projection of `Set.Finite` to its `Finite` instance is designed for use with dot notation. The theorem also refers to two other concepts, `Set.Finite.Fintype` and `Set.Finite.nonempty_fintype`, for further exploration.
More concisely: If `s` is a finite set of type `α` in Lean, then the subtype `↑s` is also a finite set.
|
Set.Finite.of_finite_image
theorem Set.Finite.of_finite_image :
∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, (f '' s).Finite → Set.InjOn f s → s.Finite
This theorem states that for any types `α` and `β`, any set `s` of type `α`, and any function `f` from `α` to `β`, if the image of `s` under `f` (denoted by `f '' s`) is finite and if `f` is injective on `s` (i.e., no two distinct elements of `s` have the same image under `f`), then the original set `s` is also finite.
More concisely: If `s` is a finite, invariant under `f` subset of type `α` such that the image of `s` under an injective function `f`: `α → β` is also finite, then `s` is finite.
|
Set.Finite.induction_on'
theorem Set.Finite.induction_on' :
∀ {α : Type u} {C : Set α → Prop} {S : Set α},
S.Finite → C ∅ → (∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → a ∉ s → C s → C (insert a s)) → C S
This theorem, analogous to `Finset.induction_on'`, is about finite sets in a given type `α`. The theorem states that for any property `C` about sets of `α` and any finite set `S`, if the property `C` holds for the empty set and for any subset `s` of `S` to which an element `a` of `S` that is not already in `s` is added (given that `C` already holds for `s`), then the property `C` holds for the set `S`. In other words, it defines an induction principle for finite sets.
More concisely: If `C(∅)` holds and for all finite sets `S` and `a ∈ S\S`, `C(s)` implies `C(s ∪ {a})`, then `C(S)` holds for all finite sets `S` of type `α`.
|
Set.union_finset_finite_of_range_finite
theorem Set.union_finset_finite_of_range_finite :
∀ {α : Type u} {β : Type v} (f : α → Finset β), (Set.range f).Finite → (⋃ a, ↑(f a)).Finite
This theorem states that for any types `α` and `β`, given a function `f` from `α` to `Finset β`, if the range of function `f` is finite, then the union of all the `Finset β`s (obtained by applying `f` to every element in `α` and converting the resulting finsets to sets) is also finite. In mathematical terms, if we have a function `f: α → Finset β` such that `f`'s range is finite, then the union of the sets `f(a)` for all `a` in `α` is finite.
More concisely: If `f: α → Finset β` is a function with finite range, then the union of the sets `{β : β | ∃ a: α, b ∈ f a}`, where `b` ranges over `β`, is finite.
|
Set.finite_subset_iUnion
theorem Set.finite_subset_iUnion :
∀ {α : Type u} {s : Set α},
s.Finite → ∀ {ι : Type u_1} {t : ι → Set α}, s ⊆ ⋃ i, t i → ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
The theorem `Set.finite_subset_iUnion` states that for any type `α`, given a finite set `s` of type `α`, for any index set `ι` and any indexed family `t` of sets of `α`, if `s` is a subset of the union of the sets `t i` for all `i`, then there exists a finite subset `I` of `ι` such that `s` is a subset of the union of the sets `t i` for `i` in `I`. In other words, if a finite set is included in the union of an indexed family of sets, then the finite set is actually included in the union of a finite subfamily of sets.
More concisely: Given a finite set `s` and an indexed family `t` of sets, if `s` is a subset of the union of the `t i` for all `i`, then there exists a finite subset `I` of the index set such that `s` is a subset of the union of the `t i` for `i` in `I`.
|
Set.Finite.union
theorem Set.Finite.union : ∀ {α : Type u} {s t : Set α}, s.Finite → t.Finite → (s ∪ t).Finite
The theorem `Set.Finite.union` states that for any type `α`, and any two sets `s` and `t` of that type, if both `s` and `t` are finite sets, then their union (denoted by `s ∪ t`) is also a finite set.
More concisely: If `s` and `t` are finite sets of type `α`, then their union `s ∪ t` is also a finite set.
|
Set.Finite.image2
theorem Set.Finite.image2 :
∀ {α : Type u} {β : Type v} {γ : Type x} {s : Set α} {t : Set β} (f : α → β → γ),
s.Finite → t.Finite → (Set.image2 f s t).Finite
This theorem states that for any types `α`, `β`, and `γ`, any sets `s` of `α` and `t` of `β`, and any binary function `f` from `α` and `β` to `γ`, if both `s` and `t` are finite, then the set formed by the image of the function `f` applied on all combinations of elements from sets `s` and `t` (mathematically considered as the image of the function `f` from `α × β` to `γ`) is also finite.
More concisely: If `α`, `β`, and `γ` are types, `s` and `t` are finite sets of `α` and `β` respectively, and `f` is a binary function from `α × β` to `γ`, then the image of `f` on the cartesian product `s × t` is a finite set.
|
Set.Finite.iUnion
theorem Set.Finite.iUnion :
∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set ι},
t.Finite → (∀ i ∈ t, (s i).Finite) → (∀ i ∉ t, s i = ∅) → (⋃ i, s i).Finite
The theorem says that given an indexed collection of sets `s i` where `i` comes from a finite set `t` and `s i` is finite for all `i` in `t`, and `s i` is empty for each `i` not in `t`, then the union of all the sets `s i`, denoted by `⋃ i, s i`, is also a finite set. In other words, if we have a finite set of finite sets, the union of all those sets is also finite; if an index is not present in `t`, then the corresponding set is empty and does not contribute to the union.
More concisely: Given a finite index set `t` and a family `{s i | i ∈ t}` of finite sets, the union `⋃ i, s i` is also finite.
|
Set.iUnion_iInter_of_monotone
theorem Set.iUnion_iInter_of_monotone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι']
[inst_1 : IsDirected ι' fun x x_1 => x ≤ x_1] [inst_2 : Nonempty ι'] {s : ι → ι' → Set α},
(∀ (i : ι), Monotone (s i)) → ⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
This theorem states that for any types `ι`, `ι'`, and `α`, where `ι` is finite and `ι'` is preordered with directed and nonempty elements, and a function `s` that maps `ι` and `ι'` to a set of `α`, if each function `s i` is monotone, then the increasing union over the intersection of `s i j` for all `j` and `i` respectively, is equal to the intersection over the increasing union of `s i j` for all `i` and `j` respectively. In mathematical terms, it can be described as if ∪ and ∩ denote union and intersection respectively, then `∪ j (∩ i s i j) = ∩ i (∪ j s i j)`. This is essentially stating a distribution property of increasing union over finite intersection.
More concisely: For any finite preorders `ι` and `ι'`, and a monotone function `s : ι × ι' → Set α`, the increasing union over intersections of `s i j` equals the intersection over increasing unions of `s i j`. In symbols: `∋ i, ∋ j, ∩ j (s i j) ⊆ i (⋃ j s i j) ⟹ ∋ i, ∋ j, i (⋃ j s i j) ⊆ ⋃ j (i (s i j))`.
|
Set.Infinite.of_image
theorem Set.Infinite.of_image : ∀ {α : Type u} {β : Type v} (f : α → β) {s : Set α}, (f '' s).Infinite → s.Infinite
The theorem `Set.Infinite.of_image` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if the image set of `s` under `f` (denoted by `f '' s`) is infinite, then the original set `s` itself must also be infinite. In other words, if you have a function that maps elements from set `s` to another set and the resulting set is infinite, then the original set `s` must have been infinite too.
More concisely: If `f` is a function from an infinite set `s` to a type `β`, then `s` is infinite.
|
Set.Finite.insert
theorem Set.Finite.insert : ∀ {α : Type u} (a : α) {s : Set α}, s.Finite → (insert a s).Finite
This theorem states that for any type `α`, any element `a` of that type, and any set `s` of elements of that type, if the set `s` is finite, then the set resulting from inserting the element `a` into `s` is also finite. In other words, inserting an element into a finite set results in another finite set.
More concisely: If `α` is a type, `a : α`, and `s : set α` is finite, then `insert a s` is also finite.
|
Set.Finite.pi'
theorem Set.Finite.pi' :
∀ {ι : Type u_1} [inst : Finite ι] {κ : ι → Type u_2} {t : (i : ι) → Set (κ i)},
(∀ (i : ι), (t i).Finite) → {f | ∀ (i : ι), f i ∈ t i}.Finite
This theorem states that the Cartesian product of a collection of finite sets is itself finite. More precisely, it says that for any type `ι` which is finite, and a dependent type `κ` indexed over `ι`, if for each `i : ι`, the set `t(i)` of elements of type `κ(i)` is finite, then the set of all functions `f` from `ι` to the union of `κ(i)` such that for each `i : ι`, `f(i)` is an element of `t(i)`, is also finite.
More concisely: The Cartesian product of a finite index type and a family of finite sets is itself finite.
|
Directed.exists_mem_subset_of_finset_subset_biUnion
theorem Directed.exists_mem_subset_of_finset_subset_biUnion :
∀ {α : Type u_1} {ι : Type u_2} [inst : Nonempty ι] {f : ι → Set α},
Directed (fun x x_1 => x ⊆ x_1) f → ∀ {s : Finset α}, ↑s ⊆ ⋃ i, f i → ∃ i, ↑s ⊆ f i
The theorem `Directed.exists_mem_subset_of_finset_subset_biUnion` states that for any type `α` and `ι` where `ι` is nonempty, given a directed family of sets `f : ι → Set α` directed with respect to the subset (`⊆`) relation, if a set `s` of finite elements of `α` is a subset of the union of all sets in the family, then there exists a member set `i` in the family such that `s` is a subset of `i`. This theorem essentially provides a guarantee that a subset of the union of a directed family of sets is actually a subset of some specific member in that family.
More concisely: Given a nonempty indexed family of sets `f : ι → Set α` directed with respect to subset relation, if a finite set `s` is a subset of the union of all sets in the family, then there exists `i ∈ ι` such that `s` is a subset of `f i`.
|
Set.toFinite_toFinset
theorem Set.toFinite_toFinset : ∀ {α : Type u} (s : Set α) [inst : Fintype ↑s], ⋯.toFinset = s.toFinset
The theorem `Set.toFinite_toFinset` states that for any given set `s` of some type `α`, if this set is finite (indicated by the `Fintype` instance of the set), then the conversion of this set to a `Finset` (finite set) using the `Set.Finite.toFinset` function is equivalent to the direct conversion of the set to a `Finset` using the `Set.toFinset` function. This establishes the equality between the two methods of converting a finite set to a `Finset` in Lean 4.
More concisely: For any finite set `s` of type `α` in Lean 4, `Set.Finite.toFinset s` equals `Set.toFinset s`.
|
Set.Finite.exists_maximal_wrt'
theorem Set.Finite.exists_maximal_wrt' :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] (f : α → β) (s : Set α),
(f '' s).Finite → s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
The theorem `Set.Finite.exists_maximal_wrt'` states that for any two types `α` and `β`, where `β` is partially ordered, and given a function `f` from `α` to `β` and a set `s` of type `α`, if the image of `s` under `f` is finite and `s` is nonempty, then there exists an element `a` in `s` such that for all other elements `a'` in `s`, if `f(a)` is less than or equal to `f(a')`, then `f(a)` is equal to `f(a')`. In simpler terms, this theorem asserts the existence of a maximal element in the image of a set under a given function, provided the image set is finite and the original set is nonempty.
More concisely: Given a function from a nonempty set to a finite, partially ordered set, there exists an element with maximal image under the function.
|
Set.Infinite.to_subtype
theorem Set.Infinite.to_subtype : ∀ {α : Type u} {s : Set α}, s.Infinite → Infinite ↑s
This theorem, referred to as `Set.Infinite.to_subtype`, asserts that for any type `α` and any set `s` of type `α`, if the set `s` is infinite (according to the definition provided in the Lean 4 code), then its corresponding subtype (denoted by `↑s`) is also infinite. Here, `Infinite ↑s` refers to the standard mathematical notion of an infinite set. Essentially, the theorem argues that if a set is not finite in the context of the defined mathematical structure, then its subtype will also be not finite.
More concisely: If `s` is an infinite set, then the subtype `↑s` is also infinite.
|
Set.iSup_iInf_of_monotone
theorem Set.iSup_iInf_of_monotone :
∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst_1 : Nonempty ι']
[inst_2 : IsDirected ι' fun x x_1 => x ≤ x_1] [inst_3 : Order.Frame α] {f : ι → ι' → α},
(∀ (i : ι), Monotone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
The theorem `Set.iSup_iInf_of_monotone` states that for any types `ι`, `ι'`, and `α`, where `ι` is finite, `ι'` is nonempty and directed under the order `≤`, and `α` is a frame; given a function `f` from `ι` and `ι'` to `α` such that for every element `i` of `ι`, the function `f i` is monotone, then the supremum (over `j`) of the infimum (over `i`) of `f i j` equals the infimum (over `i`) of the supremum (over `j`) of `f i j`. This means the order of taking supremum and infimum does not change the result in this context.
More concisely: For any finite `ι`, nonempty and directed `ι'`, and frame `α`, if `f : ι → ι' → α` is such that `f i` is monotone for all `i`, then `sup (i, inf (j, f i j)) = inf (i, sup (j, f i j))`.
|
Set.infinite_image_iff
theorem Set.infinite_image_iff :
∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → ((f '' s).Infinite ↔ s.Infinite)
This theorem states that for any types `α` and `β`, a set `s` of type `α`, and a function `f` that maps from `α` to `β`, if `f` is injective on the set `s`, then the image of the set `s` under `f` is infinite if and only if the set `s` itself is infinite. In other words, an injective function preserves the infiniteness of a set.
More concisely: For any injective function `f` between sets `α` and `β`, if `α` is infinite, then so is the image `f(α)`.
|
Set.finite_of_forall_not_lt_lt
theorem Set.finite_of_forall_not_lt_lt :
∀ {α : Type u} [inst : LinearOrder α] {s : Set α}, (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) → s.Finite
The theorem `Set.finite_of_forall_not_lt_lt` states that for any type `α` with a linear order, if a set `s` of this type does not contain any triple of elements `(x, y, z)` such that `x < y < z`, then the set `s` must be finite. In other words, if the set `s` does not have any strictly increasing sequences of length three, then `s` has a finite number of elements.
More concisely: If a linearly ordered type `α` has no strictly increasing sequences of length three, then any subset of `α` is finite.
|