Finset.coe_compl
theorem Finset.coe_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), ↑sᶜ = (↑s)ᶜ
The theorem `Finset.coe_compl` states that for any given type `α`, which has a finite number of elements (`Fintype α`) and decidable equality (`DecidableEq α`), and for any finite set of `α` (`s : Finset α`), the complement of the set `s` translated to a type^{} (`↑sᶜ`) is equal to the complement of the translated set `s` (`(↑s)ᶜ`). In other words, the operation of taking the complement commutes with the operation of translating a set from `Finset α` to `Set α`.
More concisely: For any finite type `α` with decidable equality, the complement of a finite set `s` in type `α` is equal to the complement of its image under coercion from `Finset α` to `Set α`.
|
Set.toFinset_inj
theorem Set.toFinset_inj :
∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s.toFinset = t.toFinset ↔ s = t := by
sorry
This theorem, `Set.toFinset_inj`, states that for any two sets `s` and `t` of some type `α`, with both sets having `Fintype` instances, the function `Set.toFinset` returns the same `Finset` for `s` and `t` if and only if `s` and `t` are the same set. This theorem essentially asserts the injectivity of the `Set.toFinset` function — it maps distinct sets to distinct finite sets.
More concisely: For sets `s` and `t` of type `α` with `Fintype` instances, `Set.toFinset s = Set.toFinset t` if and only if `s = t`.
|
Fintype.complete
theorem Fintype.complete : ∀ {α : Type u_4} [self : Fintype α] (x : α), x ∈ Fintype.elems
This is a theorem about the completeness of `Fintype.elems`, which is a `Finset` containing all elements of a `Fintype`. The theorem states that for any type `α` that has a `Fintype` structure and any element `x` of type `α`, `x` is an element of the `Finset` returned by `Fintype.elems`. In other words, `Fintype.elems` is a complete set containing all elements of its associated `Fintype`, hence the name `Fintype.complete`.
More concisely: For any `Fintype` `α`, the `Fintype.elems` of `α` is a `Finset` containing all elements of `α`.
|
Finset.univ_unique
theorem Finset.univ_unique : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Unique α], Finset.univ = {default} := by
sorry
The theorem `Finset.univ_unique` states that for any type `α` which is a finite type (`Fintype α`) and also has a unique element (`Unique α`), the universal finite set of type `α` (denoted by `Finset.univ`) is a set containing only the default element of `α`. In other words, if there's exactly one element in the type, then the universal finite set of that type consists solely of that unique element.
More concisely: If `α` is a finite type with a unique element, then `Finset.univ` is the singleton set containing that unique element.
|
Finset.subset_univ
theorem Finset.subset_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s ⊆ Finset.univ
This theorem states that for any finite type `α` and any finite set `s` of type `α`, `s` is a subset of the universal finite set of type `α`. In other words, any finite set is always a subset of the universe set for that type.
More concisely: For any finite type `α` and finite set `s` of type `α`, `s` is a subset of the universal set of type `α`.
|
Set.coe_toFinset
theorem Set.coe_toFinset : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], ↑s.toFinset = s
The theorem `Set.coe_toFinset` states that for any type `α` and any set `s` of type `α` with a `Fintype` instance, the set obtained by coercing the finset derived from `s` using `Set.toFinset` is equal to the original set `s`. In other words, we can convert a set to a finset (in the context of a finite type) and back to a set without losing any elements.
More concisely: For any type `α` with a `Fintype` instance and any set `s` of type `α`, the coercion of `s` to a finset and back is the identity function on `s`.
|
Set.toFinset_compl
theorem Set.toFinset_compl :
∀ {α : Type u_1} (s : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype α]
[inst_3 : Fintype ↑sᶜ], sᶜ.toFinset = s.toFinsetᶜ
The theorem `Set.toFinset_compl` states that for any type `α` and any set `s` of type `α`, given that `α` has decidable equality, the set `s` and the type `α` both have finite types, and the complement of `s` also has a finite type, the `Finset` corresponding to the complement of `s` is equal to the complement of the `Finset` corresponding to `s`. In simpler terms, converting the complement of a set to a finite set is the same as taking the complement of the finite set derived from the original set.
More concisely: For any decidably equal and finite type `α` with a finite set `s`, the finite set of elements not in `s` is equal to the complement of the finite set `Finset.univ s`.
|
Mathlib.Data.Fintype.Basic._auxLemma.2
theorem Mathlib.Data.Fintype.Basic._auxLemma.2 :
∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ = s₂) = ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
This theorem, `Mathlib.Data.Fintype.Basic._auxLemma.2`, states that for any given type `α` and for any two finite sets `s₁` and `s₂` of this type, `s₁` is equal to `s₂` if and only if for all elements `a` of type `α`, `a` is in `s₁` if and only if `a` is in `s₂`. In other words, two finite sets are equal precisely when they contain exactly the same elements.
More concisely: Two finite sets of type `α` are equal if and only if they contain the same elements.
|
Multiset.bijective_iff_map_univ_eq_univ
theorem Multiset.bijective_iff_map_univ_eq_univ :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
Function.Bijective f ↔ Multiset.map f Finset.univ.val = Finset.univ.val
The theorem `Multiset.bijective_iff_map_univ_eq_univ` states that for any types `α` and `β`, and for any function `f` from `α` to `β`, the function `f` is bijective (i.e., both injective and surjective) if and only if the multiset obtained by mapping the function `f` over the elements of the universal set of `α` (denoted `Finset.univ.val`) is equal to the universal set of `β`. Here, the universal set of a type refers to the set of all possible elements of that type. This theorem is valid under the assumption that both `α` and `β` are finite types.
More concisely: A function between finite types `α` and `β` is bijective if and only if the multiset obtained by mapping all elements of `α` under `f` equals the universal set of `β`.
|
Set.toFinset_univ
theorem Set.toFinset_univ :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Fintype ↑Set.univ], Set.univ.toFinset = Finset.univ
This theorem asserts that for any type `α` that has a `Fintype` instance, the transformation of the universal set of `α` into a `Finset` using `Set.toFinset` equals the universal `Finset` of `α`. In other words, if we take all elements of `α` (represented by `Set.univ`), cast them into a `Finset`, we get the same as if we directly constructed the universal `Finset` of `α` (represented by `Finset.univ`). It implies that there is a one-to-one correspondence between all elements of a finite type `α` and the elements in the universal `Finset` of `α`.
More concisely: For any type `α` with a `Fintype` instance, `Set.toFinset (Set.univ : α)` equals `Finset.univ : Finset α`.
|
Finset.eq_univ_iff_forall
theorem Finset.eq_univ_iff_forall :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, s = Finset.univ ↔ ∀ (x : α), x ∈ s
The theorem `Finset.eq_univ_iff_forall` states that for any type `α` which has a `Fintype` instance (i.e., `α` is a finite type), a `Finset` `s` of type `α` is equal to the universal `Finset` (finset of all elements of type `α`) if and only if every element of type `α` is contained in `s`. This theorem essentially captures the concept of a full or universal set in the context of finite sets.
More concisely: For a finite type `α`, a `Finset` `s` of `α` is equal to the universal `Finset` on `α` if and only if every element of `α` is in `s`.
|
exists_seq_of_forall_finset_exists'
theorem exists_seq_of_forall_finset_exists' :
∀ {α : Type u_4} (P : α → Prop) (r : α → α → Prop) [inst : IsSymm α r],
(∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) →
∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise fun m n => r (f m) (f n)
The theorem `exists_seq_of_forall_finset_exists'` states that given a type `α`, a predicate `P` on `α`, and a symmetric relation `r` on `α`, if for any finite set `s` of `α` where every element satisfies `P`, there exists another element also satisfying `P` and the relation `r` with respect to all elements in `s`, then there exists a function `f` mapping natural numbers to `α` such that every output satisfies `P` and any two distinct outputs satisfy the relation `r`. In other words, this theorem provides an induction principle for building a sequence where each new point satisfies a given predicate and a symmetric relation with respect to all the previously chosen points.
More concisely: Given a type `α`, a predicate `P` on `α`, and a symmetric relation `r` on `α`, if for any finite subset `S` of `α` where all elements satisfy `P` and are pairwise related by `r`, there exists an infinite sequence `(x_n)` in `α` such that each `x_n` satisfies `P` and `r(x_i, x_j)` holds for all distinct `i` and `j`.
|
Set.toFinset_range
theorem Set.toFinset_range :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype β] (f : β → α)
[inst_2 : Fintype ↑(Set.range f)], (Set.range f).toFinset = Finset.image f Finset.univ
This theorem states that for any types `α` and `β`, where `α` has decidable equality and `β` is finite, given a function `f` mapping from `β` to `α` and under the assumption that the range of `f` is finite, the set obtained by converting the range of `f` to a finite set equals the image of the universal finite set of type `β` under the function `f`. In other words, it says that the set of all outputs of `f` when applied to any element of `β` is the same set as applying `f` to the entire set `Finset.univ` of `β` and taking the image under `f`.
More concisely: For functions `f` from a finite type `β` to a type `α` with decidable equality, the image of `f` and the image of the universal finite set `Finset.univ` of `β` under `f` are equal.
|
Finset.image_univ_of_surjective
theorem Finset.image_univ_of_surjective :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β] {f : β → α},
Function.Surjective f → Finset.image f Finset.univ = Finset.univ
This theorem states that for any two types `α` and `β`, given that `α` and `β` are finite types (`Fintype`), `α` has decidable equality (`DecidableEq`), and `f` is a function from `β` to `α`, if `f` is surjective (i.e., for every element in `α`, there is an element in `β` such that the function `f` maps this element of `β` to that element of `α`), then the image of the universal finite set of `β` under the function `f` is equal to the universal finite set of `α`. In other words, applying `f` to every element of `β` gives us every element of `α`.
More concisely: If `α` and `β` are finite types with decidable equality, `f` is a surjective function from `β` to `α`, then the image of the universal set of `β` under `f` equals the universal set of `α`.
|
Finset.mem_univ_val
theorem Finset.mem_univ_val : ∀ {α : Type u_1} [inst : Fintype α] (x : α), x ∈ Finset.univ.val
This theorem states that for any type `α` that has a `Fintype` instance, every element `x` of type `α` belongs to the universal finite set of type `α`. In simpler terms, the theorem ensures that every element of a finite type is included in its corresponding universal finite set.
More concisely: For any type `α` with a `Fintype` instance, every `x : α` is an element of the universal finite set of `α`.
|
exists_seq_of_forall_finset_exists
theorem exists_seq_of_forall_finset_exists :
∀ {α : Type u_4} (P : α → Prop) (r : α → α → Prop),
(∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) →
∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
The theorem, 'exists_seq_of_forall_finset_exists', states that if for any finite set `s` of a certain type `α`, we can find another point that satisfies a particular relation `r` with respect to all the points in `s` and a certain predicate `P`, then we can construct a function `f` from natural numbers to `α` such that for any natural number `n`, the image of `n` under `f` satisfies the predicate `P`, and for any two natural numbers `m` and `n` where `m` is less than `n`, the image of `m` under `f` has relation `r` with the image of `n` under `f`.
More concisely: If for every finite set `S` of type `α`, there exists an element `x` in `α` such that `P(x)` holds and `r(x, y)` holds for all `y` in `S`, then there exists a function `f : ℕ → α` such that `P(f n)` holds for all natural numbers `n` and `r(f m, f n)` holds for all `m < n`.
|
Set.toFinset_diff
theorem Set.toFinset_diff :
∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
[inst_3 : Fintype ↑(s \ t)], (s \ t).toFinset = s.toFinset \ t.toFinset
The theorem `Set.toFinset_diff` states that for any type `α` and for any two sets `s` and `t` of this type, given that `α` has decidable equality, and that the sets `s`, `t`, and the difference `s \ t` are finite, the conversion to a finset of the difference set `s \ t` is equal to the difference of the finsets obtained from `s` and `t`. In other words, converting the difference of two sets to a finset gives the same result as taking the difference of the finsets obtained from the individual sets.
More concisely: For types `α` with decidable equality and finite sets `s` and `t` of `α`, the conversion of `(s \ t)` to a finset is equal to `(finset.fromFunc (λ x => if h : x ∈ s then some x else none) s) `\` (finset.fromFunc (λ x => some x) t)`.
|
Finset.map_univ_equiv
theorem Finset.map_univ_equiv :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : β ≃ α),
Finset.map f.toEmbedding Finset.univ = Finset.univ
The theorem `Finset.map_univ_equiv` states that for any two types `α` and `β` with finite instances, and an equivalence `f` from `β` to `α`, the image of the universal finset of `β` under the map induced by `f` is equal to the universal finset of `α`. This essentially means that the mapping, with the equivalence `f`, reshuffles the elements of the universal finset `β` into `α` without introducing any new elements or losing any existing ones.
More concisely: For any types `α` and `β` with finite instances and an equivalence `f` from `β` to `α`, the image of the universal finset of `β` under the map induced by `f` is equal to the universal finset of `α`.
|
Set.toFinset_setOf
theorem Set.toFinset_setOf :
∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype ↑{x | p x}],
{x | p x}.toFinset = Finset.filter p Finset.univ
The theorem `Set.toFinset_setOf` states that for any type `α` which has a `Fintype` instance, any predicate `p` over `α` for which `DecidablePred p` instance exists, and any subset of `α` defined by the set of elements that satisfy the predicate `p` for which a `Fintype` instance exists, the finset created from this subset using `Set.toFinset` is equal to the finset obtained by filtering the universal finset of `α` using the predicate `p`. In other words, it states the equivalence between the conversion of a subset defined by a predicate into a finset and the filtering of the universal set using the same predicate.
More concisely: For any type `α` with a `Fintype` instance, any decidable predicate `p` over `α`, and any subset of `α` defined by `p`, the finset obtained from `p` using `Set.toFinset` is equal to the filtering of the universal finset of `α` through `p`.
|
Finset.toFinset_coe
theorem Finset.toFinset_coe : ∀ {α : Type u_1} (s : Finset α) [inst : Fintype ↑↑s], (↑s).toFinset = s
The theorem `Finset.toFinset_coe` states that for any type `α` and any finite set `s` of type `α`, the operation of transforming the set `s` into a finset (finite set) using the `Set.toFinset` function will simply return `s` itself. This holds for all `s` such that `s` is itself a finset and there is a `Fintype` instance for the double coercion `↑↑s`. Essentially, this theorem states that the `Set.toFinset` operation on a finset is the identity function.
More concisely: For any finite set `s` of type `α` that is also a finset and has a `Fintype` instance for its double coercion, `Set.toFinset s = s`.
|
Finset.univ_filter_mem_range
theorem Finset.univ_filter_mem_range :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α → β) [inst_1 : Fintype β]
[inst_2 : DecidablePred fun y => y ∈ Set.range f] [inst_3 : DecidableEq β],
Finset.filter (fun y => y ∈ Set.range f) Finset.univ = Finset.image f Finset.univ
The theorem `Finset.univ_filter_mem_range` states that for any types `α` and `β`, given that `α` and `β` are finite, a function `f : α → β`, a decidable predicate to determine whether an element is in the range of `f`, and a decidable equality on `β`, the set of all elements of the universal finite set `Finset.univ` that satisfy the property of being in the range of `f` is equal to the set obtained by mapping the universal set `Finset.univ` using the function `f`. This corresponds to the mathematical notion of filtering the universal set for elements in the range of a function, and it is equivalent to applying the function to the entire universal set.
More concisely: For finite types `α` and `β`, the set of elements in `Finset.univ` that map to elements in the range of a function `f : α → β` with decidable domain, codomain, and equality is equal to the image of `Finset.univ` under `f`.
|
Mathlib.Data.Fintype.Basic._auxLemma.26
theorem Mathlib.Data.Fintype.Basic._auxLemma.26 :
∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], s.toFinset.Nonempty = s.Nonempty
This theorem, named `Mathlib.Data.Fintype.Basic._auxLemma.26`, establishes the equivalence between two ways of expressing the non-emptiness of a set in the context of finite types. Specifically, for any type `α` and any set `s` of this type, if `s` is a finite type, then the property of `s` being non-empty when converted to a finite set (`Set.toFinset s`) is identical to the property of `s` being non-empty in its original form (`Set.Nonempty s`). In other words, converting a non-empty set to a finite set preserves its non-emptiness.
More concisely: For any finite type `α` and non-empty set `s` of type `α`, `Set.Nonempty s` is equivalent to `Set.Finite.Nonempty (Set.toFinset s)`.
|
Fintype.ofBijective.proof_1
theorem Fintype.ofBijective.proof_1 :
∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Bijective f → Function.Injective f
The theorem `Fintype.ofBijective.proof_1` states that for any two types `α` and `β`, and for any function `f` from `α` to `β`, if the function `f` is bijective (meaning it is both injective and surjective), then it is also injective. In mathematical terms, this means that for all elements `a₁` and `a₂` in `α`, if `f(a₁) = f(a₂)` then necessarily `a₁ = a₂`. In other words, no two distinct elements in `α` map to the same element in `β` under the function `f` when `f` is bijective.
More concisely: If `f` is a bijective function from type `α` to type `β` in Lean 4, then for all `a₁, a₂ ∈ α`, `a₁ = a₂` implies `f(a₁) = f(a₂)`.
|
Fintype.rightInverse_bijInv
theorem Fintype.rightInverse_bijInv :
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β}
(f_bij : Function.Bijective f), Function.RightInverse (Fintype.bijInv f_bij) f
This theorem is stating that for any types `α` and `β` where `α` is finite and `β` has decidable equality, and for any bijective function `f` from `α` to `β`, the function `Fintype.bijInv f_bij` is a right inverse to `f`. In other words, if we apply `f` and then `Fintype.bijInv f_bij`, we get the identity function on `β`. This means that for each value `b` in `β`, applying `Fintype.bijInv f_bij` and then `f` to it gives us back the original `b`. This is a characteristic property of bijective functions and their inverses.
More concisely: For any finite type `α` and decidably equal type `β`, if `f` is a bijective function from `α` to `β`, then `Fintype.bijInv f` is its right inverse.
|
Finset.compl_filter
theorem Finset.compl_filter :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : α → Prop) [inst_2 : DecidablePred p]
[inst_3 : (x : α) → Decidable ¬p x], (Finset.filter p Finset.univ)ᶜ = Finset.filter (fun x => ¬p x) Finset.univ
This theorem, `Finset.compl_filter`, states that for any type `α` which has a finite number of elements (`Fintype α`) and a decidable equality (`DecidableEq α`), and a predicate `p` on `α` that is decidable (`DecidablePred p`), the complement (`ᶜ`) of the set of all elements in the universal set (`Finset.univ`) that satisfy `p` (i.e., `(Finset.filter p Finset.univ)ᶜ`) is equal to the set of all elements in the universal set that do not satisfy `p` (i.e., `Finset.filter (λ x => ¬p x) Finset.univ`). Here, the complement of a set refers to all elements that are not in the set, and the universality of a set refers to the set containing all possible elements of a given type.
More concisely: For any `Fintype α` with decidable equality and a decidable predicate `p` on `α`, `Finset.filter (λ x => ¬p x) Finset.univ` equals the complement of `Finset.filter p Finset.univ` in the finite power set.
|
Finset.mem_compl
theorem Finset.mem_compl :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} [inst_1 : DecidableEq α] {a : α}, a ∈ sᶜ ↔ a ∉ s
The theorem `Finset.mem_compl` states that for any type `α`, given `s`, a finite set of type `α`, and an element `a` of type `α`, `a` belongs to the complement of `s` if and only if `a` does not belong to `s`. This theorem assumes that the type `α` has decidable equality, meaning for any two elements of type `α`, whether they are equal or not can be decided definitively. Furthermore, it assumes that the type `α` is finite, which means there is a finite number of `α` objects.
More concisely: For any finite type `α` with decidable equality, an element `a` of type `α` belongs to the complement of a finite set `s` if and only if `a` is not in `s`.
|
Finset.univ_nonempty_iff
theorem Finset.univ_nonempty_iff : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.Nonempty ↔ Nonempty α
This theorem, `Finset.univ_nonempty_iff`, states that for any type `α` that has an instance of `Fintype α`, the universal finite set of that type (denoted as `Finset.univ`) is nonempty if and only if `α` is nonempty. In other words, there exists at least one element in the universal finite set of the type `α` if and only if there exists at least one element of the type `α`. This theorem provides an equivalence relationship between the nonemptiness of `Finset.univ` and the nonemptiness of `α`.
More concisely: The universal finite set of a nonempty type is nonempty.
|
Set.toFinset_congr
theorem Set.toFinset_congr :
∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s = t → s.toFinset = t.toFinset := by
sorry
The theorem `Set.toFinset_congr` states that for any two sets `s` and `t` of the same type `α`, if these two sets are equal (denoted as `s = t`), and both have `Fintype` instances, then their corresponding finite sets (or `Finset`) obtained using the `Set.toFinset` function are also equal. In other words, the `Set.toFinset` function preserves set equality.
More concisely: If two sets `s` and `t` of type `α` are equal (`s = t`) and have `Fintype` instances, then their corresponding finite sets obtained using `Set.toFinset` are also equal (`Set.toFinset s = Set.toFinset t`).
|
Set.mem_toFinset
theorem Set.mem_toFinset : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {a : α}, a ∈ s.toFinset ↔ a ∈ s
This theorem, `Set.mem_toFinset`, states that for any type `α`, any set `s` of that type, and any element `a` of type `α`, the element `a` belongs to the finite set (or `Finset`) derived from `s` if and only if the element `a` belongs to the original set `s`. In other words, the theorem establishes the equivalence of membership between a set and the corresponding finite set produced from it.
More concisely: For any type `α`, set `s` of `α`, and element `a` of `α`, `a` belongs to the finite set `Finset.fromFunc s` if and only if `a` belongs to `s`.
|
Mathlib.Data.Fintype.Basic._auxLemma.1
theorem Mathlib.Data.Fintype.Basic._auxLemma.1 :
∀ {α : Type u_1} [inst : Fintype α] (x : α), (x ∈ Finset.univ) = True
The theorem `Mathlib.Data.Fintype.Basic._auxLemma.1` states that for any type `α` that is a finite type (expressed as `[inst : Fintype α]`), any element `x` of that type is indeed a member of the universal finite set of type `Finset α` (expressed as `(x ∈ Finset.univ) = True`). In simpler terms, it confirms that every element in a finite type is a part of the universal set of that type.
More concisely: For any finite type `α`, every `α` is an element of the universal finite set `Finset α`.
|
Fin.univ_succ
theorem Fin.univ_succ :
∀ (n : ℕ), Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := ⋯ } Finset.univ) ⋯
This theorem states that for any natural number `n`, the universal finite set of type `Fin (n + 1)` (denoted as `Finset.univ`) can be constructed by first taking the universal finite set of type `Fin (n)`, then applying the function `Fin.succ` (which increments each element), and finally adding the element zero at the beginning. In other words, it embeds the set of first `n` natural numbers into the set of first `n+1` natural numbers by prepending zero. The mapping function `Fin.succ` ensures that the original elements are incremented, and hence no duplicates are present in the final set.
More concisely: For any natural number `n`, the universal finite set of type `Fin (n + 1)` is the set obtained by adding zero to the universal finite set of type `Fin n`, and incrementing each element using the `Fin.succ` function.
|
Fin.univ_succAbove
theorem Fin.univ_succAbove :
∀ (n : ℕ) (p : Fin (n + 1)), Finset.univ = Finset.cons p (Finset.map p.succAboveEmb.toEmbedding Finset.univ) ⋯ := by
sorry
This theorem states that for any natural number `n` and any `p` of type `Fin (n + 1)`, the universal finite set of type `Finset` for `Fin (n+1)` is equivalent to a new set constructed by inserting `p` into the set obtained by mapping the universal set of `Fin` `n` via the embedding function `p.succAboveEmb.toEmbedding`. Here `p.succAboveEmb.toEmbedding` denotes an embedding of `Fin n` into `Fin (n + 1)` around the specified pivot `p`. The new set is therefore the union of `{p}` and the image of the universal set under this embedding.
More concisely: For any natural number `n` and `p` in `Fin (n+1)`, the universal finite set of `Fin (n+1)` is equal to the set obtained by inserting `p` into the image of the universal set of `Fin n` under the embedding function around `p`.
|
Fintype.subtype.proof_1
theorem Fintype.subtype.proof_1 :
∀ {α : Type u_1} {p : α → Prop} (s : Finset α), (∀ (x : α), x ∈ s ↔ p x) → ∀ x ∈ s, p x
This theorem states that for any type `α`, and any property `p` defined on `α`, and for any finite set `s` of elements of type `α`, if every element `x` of `α` is in `s` if and only if it satisfies the property `p`, then for any element `x` in `s`, `x` satisfies the property `p`. In simpler terms, it asserts that if membership in the finite set `s` is equivalent to satisfying the property `p`, then all members of `s` have the property `p`.
More concisely: If a finite set `s` of elements from a type `α` contains exactly those elements satisfying a property `p`, then every element in `s` has property `p`.
|
Mathlib.Data.Fintype.Basic._auxLemma.25
theorem Mathlib.Data.Fintype.Basic._auxLemma.25 :
∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {a : α}, (a ∈ s.toFinset) = (a ∈ s)
This theorem, named `Mathlib.Data.Fintype.Basic._auxLemma.25`, states that for any type `α`, any set `s` of elements of type `α`, a finiteness instance for the set `s`, and an element `a` of type `α`, the element `a` belongs to the finite set generated from `s` (i.e., `Set.toFinset s`) if and only if the element `a` belongs to the original set `s`. This theorem connects the membership status of an element between a set and the finite set generated from it.
More concisely: For any type `α`, set `s` of elements from `α`, and a finiteness instance for `s`, an element `a` belongs to the finite set generated from `s` if and only if it belongs to `s`.
|
Set.toFinset_strict_mono
theorem Set.toFinset_strict_mono :
∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊂ t → s.toFinset ⊂ t.toFinset := by
sorry
This theorem, named `Set.toFinset_strict_mono`, is proving the **strict monotonicity** of the function `toFinset` on sets. In other words, for any two sets `s` and `t` of the same type `α`, if `s` is a strict subset of `t` (denoted by `s ⊂ t`), then the finite set derived from `s` (denoted by `s.toFinset`) is also a strict subset of the finite set derived from `t` (denoted by `t.toFinset`). Please note that this theorem assumes that the elements of `s` and `t` form finite sets, as denoted by the instances `[inst : Fintype ↑s]` and `[inst_1 : Fintype ↑t]`.
More concisely: If `s` is a strict subset of `t`, then the finite set `s.toFinset` is a strict subset of the finite set `t.toFinset`.
|
Fintype.choose_spec
theorem Fintype.choose_spec :
∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] (hp : ∃! a, p a),
p (Fintype.choose p hp)
The theorem `Fintype.choose_spec` states that for a given finite type `α`, a predicate `p` over `α`, and the proof `hp` that there exists a unique element in `α` that satisfies `p`, the element `α` produced by `Fintype.choose` using `p` and `hp` also satisfies `p`. In other words, the element chosen by `Fintype.choose` is guaranteed to satisfy the original predicate `p`.
More concisely: If `α` is a finite type, `p` is a predicate on `α`, and there exists a unique element `x` in `α` such that `p(x)` holds, then `Fintype.choose x p hp` satisfies `p`.
|
Set.toFinset_singleton
theorem Set.toFinset_singleton : ∀ {α : Type u_1} (a : α) [inst : Fintype ↑{a}], {a}.toFinset = {a}
This theorem states that for any type `α` and any instance `a` of that type, if we have a `Fintype` instance for the singleton set containing `a`, then the finset obtained by applying the `Set.toFinset` function to this singleton set is equal to the singleton set `{a}` itself. In other words, the `Set.toFinset` operation, when applied to a singleton set, will produce a finset that is identical to the original set.
More concisely: For any type `α` and any `a : α`, the singleton set `{a}` is equal to the finset obtained by applying `Set.toFinset` to it.
|
Subtype.fintype.proof_1
theorem Subtype.fintype.proof_1 :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : Fintype α] (a : α),
a ∈ Finset.filter p Finset.univ ↔ p a
This theorem states that for any type `α`, any property `p` of elements of `α` that is a decidable predicate, and any instance of `α`, if `α` is a finite type, then an element `a` of `α` is in the set of all elements of `α` that satisfy the property `p` if and only if `a` itself satisfies the property `p`. In other words, it verifies that the finite set of elements in `α` that satisfy `p` correctly filters out those elements that do not satisfy `p`.
More concisely: For any finite type `α` and decidable predicate `p` on `α`, an element `a` lies in the set of elements of `α` satisfying `p` if and only if `a` itself satisfies `p`.
|
Mathlib.Data.Fintype.Basic._auxLemma.9
theorem Mathlib.Data.Fintype.Basic._auxLemma.9 :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} [inst_1 : DecidableEq α] {a : α}, (a ∈ sᶜ) = (a ∉ s)
This theorem, `Mathlib.Data.Fintype.Basic._auxLemma.9`, states that for any type `α` which has finite elements, and for any finite set `s` of type `α`, given that `α` has decidable equality and some element `a` of type `α`, the property of `a` being an element of the complement of `s` is equivalent to `a` not being an element of `s`. In other words, an element is in the complement of a set if and only if it is not in the set itself. This is a fundamental property of set theory.
More concisely: For any type `α` with finite elements and decidable equality, the complement of a finite set `s` in `α` is equal to the set of elements not in `s`.
|
Mathlib.Data.Fintype.Basic._auxLemma.4
theorem Mathlib.Data.Fintype.Basic._auxLemma.4 :
∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), (s ⊆ Finset.univ) = True
This theorem states that for any type `α` with a finite set of instances (expressed by the typeclass `Fintype α`), any finset `s` of this type is a subset of the universal finite set of the type `α` (denoted by `Finset.univ`). Here, `Finset.univ` is the set that contains all elements of the given type `α`. In other words, every element in the finset `s` is also an element of the universal set of `α`. This is always true for all finite types and finsets of those types.
More concisely: For any finite type `α` and any finset `s` of type `α`, `s` is a subset of the universal finite set `Finset.univ` of type `α`.
|
Finset.univ_inter
theorem Finset.univ_inter :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), Finset.univ ∩ s = s
This theorem, `Finset.univ_inter`, states that for any type `α` that has a finite number of elements (denoted by `Fintype α`) and decidable equality (denoted by `DecidableEq α`), and for any finite set `s` of type `α` (denoted by `Finset α`), the intersection of the universal finite set (`Finset.univ`) and `s` is equal to `s` itself. In other words, when we take the intersection of `s` and the set of all possible elements of the same type, we simply get `s` back. This is the equivalent of saying that a set intersected with the universal set is the set itself in set theory.
More concisely: For any type `α` that is a finite Fintype with decidable equality, and any finite set `s` of type `α`, `Finset.univ α` intersect `s` equals `s`.
|
Finset.eq_univ_of_forall
theorem Finset.eq_univ_of_forall :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, (∀ (x : α), x ∈ s) → s = Finset.univ
This theorem states that for any type `α` that is of finite type (`Fintype α`), and any finite set `s` of this type (`Finset α`), if every element `x` of type `α` is an element of `s`, then `s` is equivalent to the universal finite set of type `Finset α` (`Finset.univ`). In other words, if a finite set contains every possible element of a given finite type, it is considered the universal set of that type.
More concisely: If `α` is a finite type and `s : Finset α` contains every element of `α`, then `s` is equivalent to the universal finite set `Finset.univ` of type `Finset α`.
|
Finset.coe_univ
theorem Finset.coe_univ : ∀ {α : Type u_1} [inst : Fintype α], ↑Finset.univ = Set.univ
This theorem asserts that, for any type `α` that is finite (`Fintype α`), the coercion of the universal finite set of type `Finset α` (denoted as `Finset.univ`) is equal to the universal set of type `α` (`Set.univ`). In other words, when viewed as a set, the universal finite set contains all and only the elements of the type `α`, which is the definition of the universal set of type `α`.
More concisely: For any finite type `α`, the universal finite set `Finset.univ (Fintype α)` equals the universal set `Set.univ` of type `α`.
|
Finset.mem_univ
theorem Finset.mem_univ : ∀ {α : Type u_1} [inst : Fintype α] (x : α), x ∈ Finset.univ
The theorem `Finset.mem_univ` states that for any type `α` which is a finite type (i.e., it has a `Fintype` instance), every element `x` of type `α` belongs to the universal finite set `Finset.univ` of type `Finset α`. In other words, `Finset.univ` includes all possible elements of a finite type.
More concisely: For any finite type `α`, every element `x` of type `α` belongs to the universal finite set `Finset.univ` of type `Finset α`.
|
Fin.univ_castSuccEmb
theorem Fin.univ_castSuccEmb :
∀ (n : ℕ), Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSuccEmb.toEmbedding Finset.univ) ⋯
This theorem states that for any natural number `n`, we can embed the finite set `Fin n` into the finite set `Fin (n + 1)`. This is done by appending the greatest value of `Fin n`, represented by `Fin.last n`, to the universal set `Finset.univ`. The universal set is then mapped to `Fin (n + 1)` using the function `Fin.castSuccEmb.toEmbedding`, which is an order-preserving embedding from `Fin n` to `Fin (n + 1)`. The result of this operation is equal to the original universal set.
More concisely: For any natural number `n`, there exists an order-preserving embedding of `Fin n` into `Fin (n + 1)` by appending `Fin.last n` to the universal set and using `Fin.castSuccEmb.toEmbedding`.
|
Finset.univ_map_equiv_to_embedding
theorem Finset.univ_map_equiv_to_embedding :
∀ {α : Type u_4} {β : Type u_5} [inst : Fintype α] [inst_1 : Fintype β] (e : α ≃ β),
Finset.map e.toEmbedding Finset.univ = Finset.univ
This theorem states that for any two types `α` and `β` which are finite (`Fintype α` and `Fintype β`), given an equivalence `e` between `α` and `β`, the image of the universal finite set of `α` under the mapping defined by `e` is the universal finite set of `β`. In other words, when `α` and `β` are of the same finite size, mapping the entire set of `α` to `β` using an equivalence will give us the entire set of `β`. This theorem validates the action of an embedding derived from an equivalence on the universal sets in the context of finite sets.
More concisely: For any finite types `α` and `β` and equivalence `e` between them, the image of the universal set of `α` under `e` is the universal set of `β`.
|
Set.toFinset_ofFinset
theorem Set.toFinset_ofFinset :
∀ {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p), p.toFinset = s
The theorem `Set.toFinset_ofFinset` states that for any type `α`, any set `p` of type `α`, and any finite set `s` of type `α`, if every element `x` of type `α` satisfies the condition that `x` is in `s` if and only if `x` is in `p`, then the finite set representation of `p` is equal to `s`. In other words, if a finite set and a general set have exactly the same elements, their finite set representations are the same.
More concisely: If two sets have the same elements and one is finite, then they have equal finite representations.
|
Finset.compl_insert
theorem Finset.compl_insert :
∀ {α : Type u_1} [inst : Fintype α] {s : Finset α} [inst_1 : DecidableEq α] {a : α}, (insert a s)ᶜ = sᶜ.erase a
The theorem `Finset.compl_insert` states that for any type `α` that has finite instances (denoted by `[Fintype α]`), any set `s` of this type `α` (denoted by `s : Finset α`), any element `a` of type `α` (denoted by `a : α`), and given that `α` has decidable equality (`[DecidableEq α]`), the complement of the set that results from inserting element `a` into set `s` (`(insert a s)ᶜ`) is equal to the set obtained by erasing the element `a` from the complement of set `s` (`Finset.erase sᶜ a`). This theorem basically provides us with a property of set complements in the context of finite sets.
More concisely: For any finite type `α` with decidable equality, the complement of `insert a s` equals `Finset.erase sᶜ a`.
|
Set.toFinset_mono
theorem Set.toFinset_mono :
∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊆ t → s.toFinset ⊆ t.toFinset := by
sorry
This theorem, referred to as `Set.toFinset_mono`, states that for any two sets `s` and `t` of some type `α`, if `s` is a subset of `t`, then the finite set corresponding to `s` is also a subset of the finite set corresponding to `t`. Here, `s.toFinset` and `t.toFinset` are the finite versions of the sets `s` and `t` respectively. The condition `Fintype ↑s` and `Fintype ↑t` means that the types `s` and `t` have a finite number of distinct elements. The `⊆` symbol denotes the subset relationship. In other words, all elements of `s` are also elements of `t`. The theorem essentially asserts that this subset relationship is preserved when converting the sets into finite sets.
More concisely: For any two sets `s` and `t` of finite type, if `s` is a subset of `t`, then `s.toFinset` is a subset of `t.toFinset`.
|
Finset.univ_eq_empty
theorem Finset.univ_eq_empty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : IsEmpty α], Finset.univ = ∅
The theorem `Finset.univ_eq_empty` states that for any arbitrary type `α`, given that `α` has a finite number of elements (as denoted by `Fintype α`) and `α` is empty (as denoted by `IsEmpty α`), the universal finite set of type `Finset α`, represented by `Finset.univ`, is identical to the empty set, denoted by `∅`. Essentially, if a type is empty, its corresponding universal finite set is also empty.
More concisely: For any type `α` that is both finite and empty, `Finset.univ (Fintype α) = ∅`.
|
Finset.univ_nonempty
theorem Finset.univ_nonempty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α], Finset.univ.Nonempty := by
sorry
The theorem `Finset.univ_nonempty` states that for any type `α`, given that `α` is a finite type (`Fintype α`) and there exists at least one element of type `α` (`Nonempty α`), the universal set of `α` (`Finset.univ`) is not empty. In other words, if we have a nonempty finite type, its universal set must contain at least one element.
More concisely: If `α` is a finite, nonempty type, then `Finset.univ α` is a nonempty set.
|
Finset.attach_eq_univ
theorem Finset.attach_eq_univ : ∀ {α : Type u_1} {s : Finset α}, s.attach = Finset.univ
This theorem states that for any finite set `s` of a given type `α`, the set that's obtained by attaching `s` (i.e., forming the new set of elements of the subtype `{x // x ∈ s}`) is equal to the universal finite set of type `α`, under the assumption that `α` is a finite type. In other words, every element in the universe of a finite type `α` is associated with an element in the original set `s`.
More concisely: For any finite set `s` of a finite type `α`, the subtype {x // x ∈ s} is equal to the universal finite set of type `α`.
|