LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Finset.Basic

`Finset.mem_singleton` theorem Finset.mem_singleton : ∀ {α : Type u_1} {a b : α}, b ∈ {a} ↔ b = a This theorem, `Finset.mem_singleton`, states that for all types `α` and for all elements `a` and `b` of type `α`, `b` is an element of the singleton set that only contains `a` if and only if `b` is equal to `a`. In other words, in a set with only one element, an element is contained in that set if and only if it's the same as that one element. More concisely: For any type `α` and elements `a` of `α`, the singleton set `{a : α}` contains `a` if and only if `a` is equal to the element in the set.
`Finset.eq_empty_of_forall_not_mem` theorem Finset.eq_empty_of_forall_not_mem : ∀ {α : Type u_1} {s : Finset α}, (∀ (x : α), x ∉ s) → s = ∅ This theorem states that for any type `α` and any finite set `s` of `α`, if every element of type `α` is not in `s`, then `s` must be the empty set. In other words, if no elements of a particular type belong to a certain finite set, then the finite set is necessarily empty. More concisely: If a finite set of type `α` contains no elements of type `α`, then the set is empty.
`Finset.cons_induction_on` theorem Finset.cons_induction_on : ∀ {α : Type u_4} {p : Finset α → Prop} (s : Finset α), p ∅ → (∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (Finset.cons a s h)) → p s The theorem `Finset.cons_induction_on` specifies a scheme for mathematical induction on finite sets. For any type `α`, if we have a property `p` that holds for the empty set, and if the property is such that whenever it holds for any set `s` and some element `a` not in `s`, it also holds for the set obtained by adding `a` to `s`, then `p` holds for all finite sets of type `α`. This is a kind of structural induction where the inductive step involves adding an element to the set. More concisely: If a property `p` holds for the empty set `∅` of type `α` and satisfies `p(s : set α) ∧ a ∉ s → p(s ∪ {a})`, then `p` holds for all finite sets `s` of type `α`.
`Finset.filter_subset` theorem Finset.filter_subset : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), Finset.filter p s ⊆ s This theorem states that for any type `α`, any decidable predicate `p` on `α`, and any finite set `s` of type `α`, the set of elements in `s` that satisfy the predicate `p` (denoted as `Finset.filter p s`) is a subset of `s`. In other words, filtering a finite set by a predicate cannot produce new elements that were not in the original set. More concisely: For any type `α`, decidable predicate `p` on `α`, and finite set `s` of type `α`, `Finset.filter p s` is a subset of `s`.
`Finset.val_eq_zero` theorem Finset.val_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.val = 0 ↔ s = ∅ This theorem states that for any set `s` of a generic type `α`, the value of `s` is zero if and only if `s` is an empty set. In other words, it establishes a relationship between the finiteness of a set in Lean 4 and its emptiness. Specifically, a finite set `s` is empty (denoted as ∅) exactly when its value is zero. More concisely: A set of type `α` in Lean 4 is empty if and only if its value is equal to the empty set (∅) or zero.
`Finset.eq_empty_of_isEmpty` theorem Finset.eq_empty_of_isEmpty : ∀ {α : Type u_1} [inst : IsEmpty α] (s : Finset α), s = ∅ This theorem states that for any type `α` that is empty (as defined by the `IsEmpty` class), any finite set (or `Finset`) of `α` is itself empty. In other words, there are no finite sets of an empty type other than the empty set. More concisely: If `α` is an empty type, then every finite set of `α` is the empty set.
`Mathlib.Data.Finset.Basic._auxLemma.74` theorem Mathlib.Data.Finset.Basic._auxLemma.74 : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ ⊆ s₂) = ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂ This theorem, titled `Mathlib.Data.Finset.Basic._auxLemma.74`, states that for any two finite sets `s₁` and `s₂`, defined over an arbitrary type `α`, the condition that `s₁` is a subset of `s₂` is equivalent to the statement that every element `x` of `s₁` also belongs to `s₂`. In other words, if every element of `s₁` is also in `s₂`, then `s₁` is a subset of `s₂`, and vice versa. More concisely: For finite sets `s₁` and `s₂` over type `α`, `s₁ ⊆ s₂` if and only if `∀ x ∈ s₁, x ∈ s₂`.
`Finset.Nonempty.bex` theorem Finset.Nonempty.bex : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∃ x, x ∈ s This theorem states that for any nonempty finite set `s` of an arbitrary type `α`, there exists an element `x` that belongs to `s`. In other words, if a finite set is not empty, we can always find at least one element in the set. This corresponds to the intuitive understanding of non-emptiness: a set is nonempty if and only if it contains at least one element. More concisely: For any finite non-empty set `s` in type `α`, there exists an element `x ∈ s`.
`Finset.insert_nonempty` theorem Finset.insert_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).Nonempty The theorem `Finset.insert_nonempty` asserts that for any type `α` with a decidable equality relation, any element `a` of type `α`, and any finite set `s` of type `α`, the set resulting from inserting `a` into `s` is nonempty. In other words, if you add an element to a finite set, the resulting set is guaranteed to have at least one element. More concisely: For any type `α` with decidable equality and any finite set `s` of `α` and any `a` in `α`, the set `s.insert a` is nonempty.
`Finset.ext_iff` theorem Finset.ext_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂ This theorem states that for any two finite sets `s₁` and `s₂` of a certain type `α`, `s₁` is equal to `s₂` if and only if for every element `a` of type `α`, `a` is an element of `s₁` if and only if `a` is an element of `s₂`. In other words, two finite sets are equal if they contain exactly the same elements. More concisely: Two finite sets `s₁` and `s₂` of type `α` are equal if and only if they have the same elements.
`Finset.forall_mem_cons` theorem Finset.forall_mem_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop), (∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x This theorem states that for any type `α`, any finite set `s` of `α`, any element `a` of type `α`, and any property `p` pertaining to the elements of `α`, the property `p` holds for all elements in the finite set obtained by adding `a` to `s` (i.e., `Finset.cons a s`) if and only if `p` holds for `a` and for all elements in `s`. In other words, a property is true for all elements of the union set `{a} ∪ s` if and only if it's true for `a` and for all elements of `s`. More concisely: For any type `α`, property `p`, finite set `s` of `α`, and `a` in `α`, `p` holds for the finite set `{a} ∪ s` if and only if `p` holds for `a` and all elements in `s`.
`Finset.coe_subset` theorem Finset.coe_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂ This theorem states that for all types `α` and for all finite sets `s₁` and `s₂` of this type, the coercion of `s₁` is a subset of the coercion of `s₂` if and only if `s₁` is a subset of `s₂`. Coercion here refers to the process of converting one type into another and the `↑` symbol indicates this coercion. The subsets are represented by the `⊆` symbol. This theorem is essentially stating that the subset relationship is preserved under coercion. More concisely: For all types `α` and finite sets `s₁` and `s₂` of type `α`, `↑s₁ ⊆ ↑s₂` if and only if `s₁ ⊆ s₂`.
`Finset.subset_singleton_iff` theorem Finset.subset_singleton_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊆ {a} ↔ s = ∅ ∨ s = {a} This theorem states that for any type `α`, any finite set `s` of `α`, and any element `a` of `α`, the set `s` is a subset of the singleton set `{a}` if and only if `s` is either the empty set or it is equal to the singleton set `{a}`. More concisely: For any type `α` and any finite set `s` of `α`, `s` is a subset of the singleton set `{a}` if and only if `s` is the empty set or `s` = {`a`}.
`Mathlib.Data.Finset.Basic._auxLemma.95` theorem Mathlib.Data.Finset.Basic._auxLemma.95 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = ((a ∧ c) ∧ b) This theorem states that for any three propositions `a`, `b`, and `c`, the logical conjunction of `a`, `b`, and `c` (in the order `a`, `b`, `c`) is equivalent to the logical conjunction of `a`, `c`, and `b` (in the order `a`, `c`, `b`). In other words, it states that 'and' is commutative when joining three items; the order of `b` and `c` does not affect the truth value of the entire expression. This is stated in mathematical logic as: $(a \land b) \land c = (a \land c) \land b$. More concisely: The logical conjunction of three propositions is commutative, that is, `(a ∧ b) ∧ c = a ∧ (b ∧ c)` for any propositions `a`, `b`, and `c`.
`Finset.erase_insert` theorem Finset.erase_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).erase a = s The theorem `Finset.erase_insert` states that for all sets `s` of a certain type `α`, and for all elements `a` of the same type `α` such that `a` does not belong to `s`, if you first insert `a` into `s` and then erase `a` from the resulting set, you get back the original set `s`. This is under the condition that the equality of elements of type `α` is decidable, meaning we can determine whether two elements of type `α` are equal or not. Essentially, it's like saying if you add something to a set and then immediately remove it, you are left with the original set. More concisely: For any decidably-equated type `α` and set `s` of type `λ (a : α), Finset α a`, if `a ∉ s`, then `Finset.erase (Finset.insert a s) = s`.
`Finset.self_mem_range_succ` theorem Finset.self_mem_range_succ : ∀ (n : ℕ), n ∈ Finset.range (n + 1) This theorem states that for any natural number `n`, `n` is an element of the set of natural numbers less than `n + 1`. In mathematical terms, for all natural numbers `n`, `n` belongs to the set `{0, 1, 2, ..., n}`. More concisely: For every natural number `n`, `n` is an element of the set `{m \| m < n + 1}`.
`Finset.insert_val_of_not_mem` theorem Finset.insert_val_of_not_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).val = a ::ₘ s.val The theorem `Finset.insert_val_of_not_mem` asserts that for any type `α` with decidable equality, and for any element `a` of that type and `s` being a finite set of that type, if `a` is not an element of `s`, then the value of the insertion of `a` into `s` equals to the value of `a` prepended to the value of `s`. Here `insert a s` denotes the operation of inserting `a` into the set `s`, and `a ::ₘ s.val` represents the list formed by prepending `a` to the list of elements in `s`. More concisely: If `α` has decidable equality, `a` is not an element of finite set `s` in type `α`, then `insert a s = a :: s.val`.
`Finset.eq_singleton_iff_unique_mem` theorem Finset.eq_singleton_iff_unique_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a This theorem states that for any given set `s` of type `α` and any element `a` of the same type, `s` is a singleton set containing only `a` if and only if `a` is an element of `s` and any other element `x` in `s` is equal to `a`. In other words, `s` equals the set `{a}` exactly when `s` contains `a` and no other distinct elements. More concisely: A set `s` of type `α` is a singleton containing only `a` if and only if `a` is an element of `s` and for all `x` in `s`, `x = a`.
`Mathlib.Data.Finset.Basic._auxLemma.19` theorem Mathlib.Data.Finset.Basic._auxLemma.19 : (¬False) = True This theorem, termed as `Mathlib.Data.Finset.Basic._auxLemma.19`, asserts that the negation of `False` is `True`. In the context of classical logic, the negation of a false statement always results in a true statement. Therefore, `¬False` is logically equivalent to `True`. More concisely: The negation of False is True. (In classical logic)
`Finset.insert_eq_of_mem` theorem Finset.insert_eq_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a s = s This theorem states that for any type `α` that has decidable equality, any finite set `s` of `α`, and any element `a` of `α`, if `a` is already an element of `s`, then inserting `a` into `s` does not change `s`. In other words, inserting an existing element into a finite set has no effect on the set, as sets do not contain duplicate elements. More concisely: For any finite type `α` with decidable equality, adding an existing element to a finite set `s` of `α` does not change `s`.
`Finset.induction` theorem Finset.induction : ∀ {α : Type u_4} {p : Finset α → Prop} [inst : DecidableEq α], p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) → ∀ (s : Finset α), p s This theorem, named `Finset.induction`, states a principle of induction for finite sets, or `Finset`s. Given any type `α` with decidable equality and a property `p` that applies to `Finset`s of type `α`, if the property holds for the empty set and if, for any element `a` of type `α` and any `Finset` `s` of type `α`, the property holding for `s` implies that it holds for the `Finset` resulting from inserting `a` into `s` (provided `a` was not already in `s`), then the property holds for all `Finset`s of type `α`. More concisely: If a property holds for the empty finite set and is closed under adding elements not in the set, then it holds for all finite sets.
`Mathlib.Data.Finset.Basic._auxLemma.80` theorem Mathlib.Data.Finset.Basic._auxLemma.80 : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, (a ∈ s ∪ t) = (a ∈ s ∨ a ∈ t) This theorem, titled `Mathlib.Data.Finset.Basic._auxLemma.80`, states that for any type `α` with decidable equality and for any two finite sets `s` and `t` of this type, and any element `a` of this type, the proposition that `a` is an element of the union of `s` and `t` is equivalent to the proposition that `a` is either an element of `s` or an element of `t`. In other words, it provides a formalization of the basic set theory fact that an element belongs to the union of two sets if and only if it belongs to at least one of the sets. More concisely: For any type `α` with decidable equality, the union of two finite sets `s` and `t` of `α` equals the set of elements that are in `s` or in `t`.
`Finset.singleton_injective` theorem Finset.singleton_injective : ∀ {α : Type u_1}, Function.Injective singleton The theorem `Finset.singleton_injective` states that for all types `α`, the `singleton` function, which takes an element and returns a set containing only that element, is injective. In more mathematical terms, this means that for any two elements `a₁` and `a₂` of type `α`, if the singleton sets `{a₁}` and `{a₂}` are equal, then `a₁` and `a₂` themselves must be equal. More concisely: If two singleton sets in a type `α` are equal, then the elements they contain are equal.
`Mathlib.Data.Finset.Basic._auxLemma.2` theorem Mathlib.Data.Finset.Basic._auxLemma.2 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ s.val) = (a ∈ s) := by sorry This theorem, named `_auxLemma.2` in the module `Mathlib.Data.Finset.Basic`, states that for any type `α`, any element `a` of type `α`, and any finite set `s` of elements of type `α`, the element `a` is in the underlying value (`s.val`) of the finite set `s` if and only if the element `a` is in the finite set `s` itself. This asserts the equivalence between the membership in the set and the membership in its underlying value. More concisely: For any type α, any element a of α, and any finite set s of elements of α, the element a is in set s if and only if a is in the underlying value s.val of s.
`Mathlib.Data.Finset.Basic._auxLemma.39` theorem Mathlib.Data.Finset.Basic._auxLemma.39 : ∀ {α : Type u_1} {s : Finset α} {a : α}, ({a} ⊆ s) = (a ∈ s) := by sorry This theorem states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, the singleton set containing `a` is a subset of `s` if and only if `a` is an element of `s`. This theorem formalizes a basic fact about set theory: an element belongs to a set if and only if the set that contains only this element is a subset of the original set. More concisely: For any type `α`, set `s` of type `α`, and element `a` of type `α`, the singleton set `{a}` is a subset of `s` if and only if `a` is an element of `s`.
`Finset.disjoint_val` theorem Finset.disjoint_val : ∀ {α : Type u_1} {s t : Finset α}, s.val.Disjoint t.val ↔ Disjoint s t The theorem `Finset.disjoint_val` states that for any two finite sets `s` and `t` of any arbitrary type `α`, the multiset values of `s` and `t` are disjoint if and only if the finite sets `s` and `t` themselves are disjoint. Here, two multisets are considered disjoint if they have no elements in common, and two elements of a lattice are disjoint if their infimum is the bottom element. More concisely: For any finite sets `s` and `t` of type `α` in Lean, their multisets have no common elements if and only if `s` and `t` are disjoint.
`Finset.cons_eq_insert` theorem Finset.cons_eq_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s), Finset.cons a s h = insert a s := by sorry This theorem, named `Finset.cons_eq_insert`, states that for any type `α` with a decidable equality relation, any element `a` of type `α`, and any finite set `s` of type `α` such that `a` is not a member of `s`, the operation of constructing a new finite set from `a` and `s` using the `Finset.cons` function is equivalent to the operation of inserting `a` into `s`. In other words, given these constraints, `Finset.cons a s h` and `insert a s` will result in the same finite set. More concisely: For any type `α` with decidable equality and any finite set `s` of `α` not containing `a` in `α`, `Finset.cons a s` and `insert a s` yield equal finite sets.
`Finset.insert_erase_invOn` theorem Finset.insert_erase_invOn : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, Set.InvOn (insert a) (fun s => s.erase a) {s \| a ∈ s} {s \| a ∉ s} The theorem `Finset.insert_erase_invOn` states that for any type `α` with decidable equality and any element `a` of type `α`, the function `insert a` and the function `erase s a` are inverses of each other for the relevant domains. More specifically, `insert a` acts as inverse in the set where `a` does not belong to `s` and `erase s a` acts as inverse in the set where `a` belongs to `s`. Here, `s` is a set of `α`. This means that if you insert an element `a` into a set from which it has been erased, you will get back your original set; and similarly, if you erase an element `a` from a set where it has been inserted, you will also retrieve your initial set. More concisely: For any type `α` with decidable equality and any set `s` of `α`, the functions `insert a` and `erase s a` are inverse bijections when `a` is not in `s` and `a` is in `s`, respectively.
`Finset.insert_empty` theorem Finset.insert_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, insert a ∅ = {a} This theorem states that for any type `α` with decidable equality and any element `a` of this type, inserting `a` into an empty `Finset` (finite set) results in a `Finset` containing only `a`. In other words, if you start with an empty set and add an element to it, the resulting set will just be the singleton containing that element. The theorem generalizes the intuitive notion that adding an element to an empty collection results in a collection containing just that one element. More concisely: For any type `α` with decidable equality and any element `a` of type `α`, the singleton set `{a}` is the result of adding `a` to an empty `Finset` of type `α`. In Lean notation, `{x \| x ∈ ∅ → x = a}` is equal to `{a}`.
`Finset.Nonempty.cons_induction` theorem Finset.Nonempty.cons_induction : ∀ {α : Type u_4} {p : (s : Finset α) → s.Nonempty → Prop}, (∀ (a : α), p {a} ⋯) → (∀ ⦃a : α⦄ (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯) → ∀ {s : Finset α} (hs : s.Nonempty), p s hs The theorem `Finset.Nonempty.cons_induction` states that to prove a property `p` about a nonempty finite set `s` of some type `α`, it is sufficient to verify two conditions. Firstly, `p` must hold for every singleton set - a set containing just one element `a` of type `α`. Secondly, if `p` is true for some nonempty finite set `t` and an element `a` is not in `t`, then `p` remains true when `a` is added to `t` to form a new set. In other words, the theorem provides a method for inductive reasoning over nonempty finite sets. More concisely: Given a property `p` and a nonempty finite set `s` of type `α`, if `p` holds for all singletons and for every `a` not in a set `t` with `p(t)`, then `p` holds for `s`.
`Finset.filter_true_of_mem` theorem Finset.filter_true_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (∀ x ∈ s, p x) → Finset.filter p s = s The theorem `Finset.filter_true_of_mem` asserts that, for any type `α`, any predicate `p` on `α` that is decidable, and any finite set `s` of type `α`, if every element `x` in `s` satisfies the predicate `p` (formally, for all `x` in `s`, `p(x)` holds), then filtering `s` by `p` leaves `s` unchanged. Essentially, it states that if all elements of a finite set meet a certain condition, then filtering that set based on that condition yields the original set. More concisely: If `s` is a finite set of elements from type `α` and `p` is a decidable predicate on `α` such that `p(x)` holds for all `x` in `s`, then `Filter p s = s`.
`Finset.mem_cons_self` theorem Finset.mem_cons_self : ∀ {α : Type u_1} (a : α) (s : Finset α) {h : a ∉ s}, a ∈ Finset.cons a s h The theorem `Finset.mem_cons_self` states that for any type `α`, any element `a` of type `α`, and any finite set `s` of elements of type `α`, if `a` is not an element of `s`, then `a` is an element of the finite set that results from the operation `Finset.cons a s h`. The `Finset.cons` operation creates a new finite set by adding the element `a` to the set `s`. Here, `h` is the proof that `a` is not in `s`. Therefore, this theorem essentially states that an element is in the set that results from adding it to another set. More concisely: If `a` is not an element of finite set `s`, then `a` is an element of the set obtained by adding `a` to `s`.
`List.toFinset_cons` theorem List.toFinset_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, (a :: l).toFinset = insert a l.toFinset This theorem states that for any type `α` with decidable equality (denoted by `DecidableEq α`), for any list `l` of elements of type `α`, and for any element `a` of the same type, converting a list that starts with element `a` and is followed by list `l` into a finite set (using the `List.toFinset` function) is the same as inserting element `a` into the finite set version of list `l`. In other words, if you have a list starting with an element and then convert it to a set, it's the same as first converting the list to a set and then adding the element to the set. More concisely: For any type `α` with decidable equality, the function `List.toFinset` that maps a list `a :: l : list α` to the set `{x : α \| x ∈ l} ∪ {a}` is equal to the function that first maps `l` to the set `{x : α \| x ∈ l}`, and then maps the resulting set to the set `{x : α \| x ∈ l ∪ {a}}`.
`Finset.subset_empty` theorem Finset.subset_empty : ∀ {α : Type u_1} {s : Finset α}, s ⊆ ∅ ↔ s = ∅ This theorem states that for all types `α` and all finite sets `s` of type `α`, `s` is a subset of the empty set if and only if `s` is equal to the empty set. In other words, the only finite set that can be a subset of the empty set is the empty set itself. More concisely: A finite set is a subset of the empty set if and only if it is equal to the empty set.
`Mathlib.Data.Finset.Basic._auxLemma.51` theorem Mathlib.Data.Finset.Basic._auxLemma.51 : ∀ {α : Type u_1} {s t : Finset α}, Disjoint s t = ∀ ⦃a : α⦄, a ∈ s → a ∉ t This theorem states that for any type `α` and any two finite sets `s` and `t` of this type, `s` and `t` are disjoint if and only if for all elements `a` of type `α`, if `a` belongs to `s`, then `a` does not belong to `t`. In other words, no element can be in both `s` and `t` at the same time if the sets are disjoint. This is a generalization of the concept of disjoint sets in set theory. More concisely: For any type `α` and finite sets `s` and `t` of type `α`, `s` and `t` are disjoint if and only if no element of `α` belongs to both `s` and `t`.
`Mathlib.Data.Finset.Basic._auxLemma.174` theorem Mathlib.Data.Finset.Basic._auxLemma.174 : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.Nonempty = (l ≠ []) This theorem states that for any type `α`, any element `x` of type `α`, any Boolean-valued function `p` on `α`, and any list `as` of type `α`, the proposition that `x` is an element of the list obtained by filtering `as` with `p` is equivalent to the conjunction of the propositions that `x` is an element of `as` and `p` applied to `x` returns `true`. In other words, an item is in the filtered list if and only if it is in the original list and it satisfies the filtering condition. More concisely: For any type `α`, any element `x` of type `α`, any Boolean-valued function `p` on `α`, and any list `as` of type `α`, the element `x` belongs to the filtered list `[x \| x ∈ as \| p x]` if and only if `x` belongs to `as` and `p x` evaluates to `true`.
`Finset.union_comm` theorem Finset.union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∪ s₂ = s₂ ∪ s₁ The theorem `Finset.union_comm` states that for any type `α` with decidable equality (`DecidableEq α`) and for any two finite sets (`Finset α`) `s₁` and `s₂`, the union of `s₁` and `s₂` is the same as the union of `s₂` and `s₁`. In other words, the operation of taking the union of two finite sets is commutative. More concisely: For any type `α` with decidable equality and any two finite sets `s₁` and `s₂` of type `Finset α`, `s₁ ∎ s₂` equals `s₂ ∎ s₁`, where `∎` denotes the finite set union operation.
`Mathlib.Data.Finset.Basic._auxLemma.23` theorem Mathlib.Data.Finset.Basic._auxLemma.23 : ∀ {α : Type u_1} {s : Finset α}, (s.val = 0) = (s = ∅) This theorem, titled `_auxLemma.23` from the module `Mathlib.Data.Finset.Basic`, states that for any type `α` and any finite set `s` of type `α`, the value of `s` being zero is equivalent to `s` being an empty set. In other words, in the context of finite sets, a set is empty if and only if its value is zero. More concisely: A finite set `s` of type `α` is empty if and only if its value is zero.
`Finset.filter_eq` theorem Finset.filter_eq : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), Finset.filter (Eq b) s = if b ∈ s then {b} else ∅ This theorem states that for any given set `s` of a certain type `β` (where `β` has decidable equality) and any element `b` of type `β`, if you filter `s` by keeping only the elements that are equal to `b`, the resulting set will contain at most the element `b`. In other words, after the filtering process, the resulting set will either be a singleton set containing `b` (if `b` is an element of `s`), or an empty set (if `b` is not an element of `s`). More concisely: Given a set `s` of type `β` with decidable equality and an element `b` of type `β`, the filter `{x : s \| x = b}` has at most one element.
`Finset.union_sdiff_self_eq_union` theorem Finset.union_sdiff_self_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t \ s = s ∪ t The theorem `Finset.union_sdiff_self_eq_union` says that for any type `α` with decidable equality and any two finite sets `s` and `t` of type `α`, the union of `s` and the set difference `t \ s` is equal to the union of `s` and `t`. That is, adding all elements of `s` to the set obtained by removing all elements of `s` from `t` results in the same set as simply uniting `s` and `t`. This is expressed in the language of set theory, where `\` denotes set difference, and `∪` denotes union. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, `(s ∪ (t \ s)) = (s ∪ t)`.
`Finset.filter_insert` theorem Finset.filter_insert : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (a : α) (s : Finset α), Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s The `Finset.filter_insert` theorem states that for any type `α`, a predicate `p` that has decidable truth values for each `α`, a decidable equality on `α`, an element `a` of type `α`, and a finite set `s` of elements of type `α`, the operation of filtering the set obtained by inserting `a` into `s` using the predicate `p` is equivalent to: if `p a` is true, then inserting `a` into the set obtained by filtering `s` using `p`; otherwise, it's just the set obtained by filtering `s` using `p`. In other words, when filtering a set where an element has been added, if the element satisfies the predicate, it appears in the filtered set; otherwise, it doesn't affect the filtered set. More concisely: For any type `α`, decidable `p : α → Prop`, decidable equality on `α`, `a : α`, and finite `s : Finset α`, `a ∈ filter (p) (insert a s) <-> p a`.
`Finset.inter_eq_right` theorem Finset.inter_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ∩ s = s ↔ s ⊆ t The theorem `Finset.inter_eq_right` states that for any type `α` with decidable equality, and for any two finite sets `s` and `t` of this type, the intersection of `t` and `s` being equal to `s` is equivalent to `s` being a subset of `t`. In other words, if the intersection of `t` and `s` yields `s`, then all elements of `s` must be within `t`. This theorem applies to any general type with decidable equality, meaning we can determine whether two elements of the type are equal or not. More concisely: For any type `α` with decidable equality, sets `s` and `t` in `Finset α`, the equality `s = t ∩ s` implies `s ⊆ t`.
`Finset.not_nonempty_iff_eq_empty` theorem Finset.not_nonempty_iff_eq_empty : ∀ {α : Type u_1} {s : Finset α}, ¬s.Nonempty ↔ s = ∅ This theorem states that for any given type `α` and a finite set `s` of this type, the set `s` is not nonempty if and only if the set `s` is empty. In other words, a finite set is not nonempty if it doesn't contain any elements, which is equivalent to saying that the set is empty. More concisely: A finite set is nonempty if and only if it is not empty.
`Finset.forall_of_forall_insert` theorem Finset.forall_of_forall_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} {a : α} {s : Finset α}, (∀ x ∈ insert a s, p x) → ∀ x ∈ s, p x This theorem, named `Finset.forall_of_forall_insert`, states that for a given type `α` with decidable equality, a predicate `p`, an element `a` of type `α`, and a finite set `s` of type `α`, if the predicate holds for all elements in the set obtained by inserting `a` into `s`, then the predicate also holds for all elements in the original set `s`. This theorem is particularly useful in proofs by induction. More concisely: If `α` has decidable equality, `p` is a predicate on `α`, `a` is an element of `α`, and `s` is a finite set of `α` such that `p` holds for all elements in `s ∪ {a}` implies `p` holds for all elements in `s`, then `p` holds for all elements in `s`.
`Finset.filter_or` theorem Finset.filter_or : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : DecidableEq α] (s : Finset α), Finset.filter (fun a => p a ∨ q a) s = Finset.filter p s ∪ Finset.filter q s This theorem, `Finset.filter_or`, states that for any type `α`, given two predicates `p` and `q` that can be decided for each element of `α`, and a finite set `s` of type `α` with decidable equality, filtering the set `s` with a predicate that is the logical disjunction (or) of `p` and `q` is equivalent to taking the union of the set filtered by predicate `p` and the set filtered by predicate `q`. More formally, if `p` and `q` are predicates on `α` and `s` is a finite set of `α`, then the set of elements in `s` for which `p` or `q` holds is equal to the union of the set of elements in `s` for which `p` holds and the set of elements in `s` for which `q` holds. More concisely: For any finite set `s` and predicates `p` and `q` on type `α` with decidable equality, `{x : α \| p x or q x} = {x : α \| p x} ∪ {x : α \| q x}`.
`Finset.disjUnion_eq_union` theorem Finset.disjUnion_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (h : Disjoint s t), s.disjUnion t h = s ∪ t This theorem states that, for any type `α` that has decidable equality, given two finite sets `s` and `t` of type `α`, if `s` and `t` are disjoint (in the sense that the infimum of any element that is less than or equal to both `s` and `t` is the bottom element of the order), then the disjoint union of `s` and `t` is equal to the ordinary union of `s` and `t`. In other words, when two sets are disjoint, the disjoint union operation and the standard union operation yield the same result. This theorem can be seen as a specification of the `Finset.disjUnion` operation, relating it to the standard union of sets. More concisely: For finite sets `s` and `t` of type `α` with decidable equality, if `s` and `t` are disjoint, then their disjoint union is equal to their ordinary union.
`Finset.inter_eq_left` theorem Finset.inter_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∩ t = s ↔ s ⊆ t This theorem states that for any type `α` that has decidable equality, and for any two finite sets `s` and `t` of type `α`, the intersection of `s` and `t` is equal to `s` if and only if `s` is a subset of `t`. In other words, it asserts that for any two finite sets, the intersection being equal to one of the sets implies that this set is contained within the other set, and conversely if one set is contained within the other, then their intersection is the set that is contained. More concisely: For any finite sets `s` and `t` of type `α` with decidable equality, `s` is a subset of `t` if and only if `s` is equal to their intersection.
`Finset.Nonempty.empty_ssubset` theorem Finset.Nonempty.empty_ssubset : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∅ ⊂ s The theorem `Finset.Nonempty.empty_ssubset` states that for any type `α` and any finite set `s` of type `α`, if `s` is nonempty, then the empty set is a strict subset of `s`. In the context of set theory, a set A is a strict subset of a set B if every element of A is also an element of B, and there's at least one element in B that is not in A. So, this theorem is saying that if a set is not empty, then there's at least one element in it that is not in the empty set, making the empty set a strict subset of it. More concisely: If `s` is a finite nonempty set, then the empty set is a proper subset of `s`.
`Finset.erase_subset` theorem Finset.erase_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s.erase a ⊆ s The theorem `Finset.erase_subset` states that for any type `α` equipped with a decidable equality relation, and for any element `a` of type `α` and any finite set `s` of elements of type `α`, the set obtained by erasing the element `a` from `s` (denoted `Finset.erase s a`) is a subset of `s`. In other words, every element in the set after erasing `a` is also in the original set `s`. More concisely: For any type `α` with decidable equality and any finite set `s` of elements from `α` and any `a` in `α`, `Finset.erase s a ⊆ s`.
`Mathlib.Data.Finset.Basic._auxLemma.64` theorem Mathlib.Data.Finset.Basic._auxLemma.64 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, (a ∈ insert b s) = (a = b ∨ a ∈ s) This theorem, named `Mathlib.Data.Finset.Basic._auxLemma.64`, states that for any type `α` which has decidable equality, any finite set `s` of type `α`, and any two elements `a` and `b` of type `α`, the proposition that `a` belongs to the set resulting from inserting `b` into `s` is equivalent to the proposition that `a` is equal to `b` or `a` belongs to the original set `s`. In other words, an element belongs to the set obtained by adding a new element into a finite set if and only if it is either equal to the newly added element or it was in the original set. More concisely: For any type `α` with decidable equality and finite set `s` of type `α`, the element `a` is in the set `s.insert(b)` if and only if `a = b` or `a` is in `s`.
`Mathlib.Data.Finset.Basic._auxLemma.45` theorem Mathlib.Data.Finset.Basic._auxLemma.45 : ∀ {a b c : Prop}, (a ∨ b → c) = ((a → c) ∧ (b → c)) This theorem, named `Mathlib.Data.Finset.Basic._auxLemma.45`, states that for any three propositional statements `a`, `b`, and `c`, the proposition that `a OR b` implies `c` is logically equivalent to the conjunction of two propositions, specifically that `a` implies `c` AND `b` implies `c`. In other words, if `c` follows from either `a` or `b`, it must follow from `a` and also from `b` separately. More concisely: The proposition `(a ∨ b) → c` is logically equivalent to `(a → c) ∧ (b → c)`.
`Finset.filter_eq'` theorem Finset.filter_eq' : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), Finset.filter (fun a => a = b) s = if b ∈ s then {b} else ∅ This theorem states that for a given finite set `s` of any type `β` with decidable equality, when we filter `s` by retaining only those elements that are equal to a specific element `b`, the resulting set is either a singleton set containing `b` (if `b` is in `s`), or it is an empty set (if `b` is not in `s`). Simply put, after filtering out all elements from a finite set that do not equal a given value, only that value remains, if it was originally in the set. More concisely: For any finite set `s` of type `β` with decidable equality, the set `{x : s \| x = b}` is a singleton containing `b` if `b` is in `s`, or is empty otherwise.
`Finset.Nonempty.mono` theorem Finset.Nonempty.mono : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.Nonempty → t.Nonempty This theorem states that for any two finite sets `s` and `t` of any type `α`, if `s` is a subset of `t` and `s` is nonempty, then `t` is also nonempty. In other words, if a set `s` has at least one element and all elements of `s` also belong to `t`, then `t` must have at least one element. This is a basic property of subset relationships in set theory. More concisely: If `s` is a nonempty subset of `t`, then `t` is nonempty.
`Finset.mem_union` theorem Finset.mem_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t This theorem states that for any type `α` with decidable equality, given two sets (`s` and `t`) of this type and an element `a` of type `α`, `a` is a member of the union of the two sets if and only if `a` is a member of at least one of the two sets. In other words, it formalizes the standard property of set union in the context of finite sets (Finsets) in the Lean 4 theorem prover. More concisely: For any decidably equal type `α` and sets `s` and `t` of type `α`, `a` is in the union of `s` and `t` if and only if `a` is in `s` or `a` is in `t`.
`Finset.filter_eq_empty_iff` theorem Finset.filter_eq_empty_iff : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, Finset.filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x This theorem, `Finset.filter_eq_empty_iff`, states that for any type `α`, any decidable predicate `p` on `α`, and any finite set `s` of elements from `α`, the condition that the filter of `s` with respect to `p` returning an empty set is equivalent to the condition that for all elements `x` in `s`, `p` does not hold for `x`. In other words, the set resulting from filtering `s` with `p` is empty if and only if there is no element in `s` for which the predicate `p` is true. More concisely: For any type `α`, decidable predicate `p` on `α`, and finite set `s` from `α`, the filter of `s` with respect to `p` is empty if and only if no element in `s` satisfies `p`.
`Finset.coe_eq_singleton` theorem Finset.coe_eq_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, ↑s = {a} ↔ s = {a} This theorem states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, the coercion of the finite set `s` to a set is equal to the singleton set that only contains the element `a` if and only if the finite set `s` itself is equal to that singleton set. In other words, it describes the equivalence between a finite set being a singleton and its coerced set being a singleton in Lean 4. More concisely: For any type `α` and any finite set `s` of type `α` with exactly one element `a`, the coercion of `s` to a set is equal to the singleton set `{a}` if and only if `s` itself is equal to `{a}`.
`Finset.mem_insert_self` theorem Finset.mem_insert_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ insert a s := by sorry The theorem `Finset.mem_insert_self` states that for any type `α` with decidable equality (represented by `[inst : DecidableEq α]`), for any element `a` of type `α`, and for any finite set `s` of elements of the same type `α` (represented by `s : Finset α`), `a` is a member of the set obtained by inserting `a` into `s`. In other words, if you insert an element into a finite set, the resulting set definitely contains that element. More concisely: For any type `α` with decidable equality and any finite set `s` of elements from `α`, the inserted element `a` is an element of the set `Finset.insert a s`.
`Finset.empty_val` theorem Finset.empty_val : ∀ {α : Type u_1}, ∅.val = 0 This theorem states that for any type `α`, the value of an empty finite set (`∅`) is equal to zero. In other words, the cardinality (or size) of an empty set, regardless of the type of its elements, is always zero. More concisely: The cardinality of an empty set is equal to zero, for any type `α`.
`Finset.disjoint_erase_comm` theorem Finset.disjoint_erase_comm : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, Disjoint (s.erase a) t ↔ Disjoint s (t.erase a) The theorem `Finset.disjoint_erase_comm` states that for any two given finite sets `s` and `t` and an element `a` of a type `α` with decidable equality, removing `a` from `s` and checking if the resulting set is disjoint from `t` is equivalent to removing `a` from `t` and checking if `s` is disjoint from the resulting set. In other words, the operation of erasing an element from a finite set commutes with the operation of checking disjointness of two finite sets. More concisely: For finite sets `s` and `t` and an element `a` of type `α` with decidable equality, `(s \\ {a}).disjoint t <-> t \\ {a}.disjoint s`.
`Finset.Nonempty.attach` theorem Finset.Nonempty.attach : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.attach.Nonempty This theorem, `Finset.Nonempty.attach`, is an alias of the reverse direction of the theorem `Finset.attach_nonempty_iff`. It states that for any type `α` and any finite set `s` of type `α`, if the set `s` is non-empty, then the set `s.attach`, which consists of elements of `s` along with their membership proofs, is also non-empty. More concisely: If `s` is a finite non-empty set, then `s.attach` is a non-empty set.
`Finset.not_mem_mono` theorem Finset.not_mem_mono : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → ∀ {a : α}, a ∉ t → a ∉ s This theorem states that for any type `α` and any two finite sets `s` and `t` of this type, if `s` is a subset of `t`, then for any element `a` of type `α`, if `a` is not in `t`, then `a` is also not in `s`. In other words, if a certain item doesn't belong to a larger set, then it certainly doesn't belong to any of its subsets. More concisely: If `s` is a subset of `t` and `a` is an element not in `t`, then `a` is not in `s`.
`Mathlib.Data.Finset.Basic._auxLemma.144` theorem Mathlib.Data.Finset.Basic._auxLemma.144 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) = ∃ x, ¬p x := by sorry This theorem states that, for any two propositions `a` and `b`, the existence of a proof of `b` given a proof of `a` is equivalent to the conjunction of `a` and `b`. In other words, there exists a proof of `b` under the assumption that `a` is true if and only if both `a` and `b` are true. More concisely: The theorem asserts that for all propositions `a` and `b`, `(∃ (p : proof a), b) ↔ a ∧ b`.
`Finset.sdiff_eq_empty_iff_subset` theorem Finset.sdiff_eq_empty_iff_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t = ∅ ↔ s ⊆ t The theorem `Finset.sdiff_eq_empty_iff_subset` states that for any type `α` with decidable equality, and for any two finite sets `s` and `t` of type `α`, the set difference of `s` and `t` being an empty set is equivalent to `s` being a subset of `t`. In other words, it asserts that all elements of `s` are in `t` if and only if there are no elements in `s` that are not in `t`. More concisely: For finite sets `s` and `t` of type `α` with decidable equality, `s \ t = ∅` if and only if `s ⊆ t`.
`Mathlib.Data.Finset.Basic._auxLemma.6` theorem Mathlib.Data.Finset.Basic._auxLemma.6 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ ↑s) = (a ∈ s) This theorem, from the `Mathlib.Data.Finset.Basic` library, states that for any type `α`, any element `a` of type `α`, and any finite set `s` of elements of type `α`, the condition "`a` belongs to the underlying set of `s`" is equivalent to the condition "`a` belongs to `s`". In mathematical terms, it says that an element being in a finite set is the same as it being in the set's underlying set. It means that the element's presence in the finset is not affected by its implementation details. More concisely: For any type `α`, any element `a` of type `α`, and any finite set `s` of elements of type `α`, `a` is in the underlying set of `s` if and only if `a` is in `s`.
`Finset.singleton_subset_iff` theorem Finset.singleton_subset_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ s This theorem, `Finset.singleton_subset_iff`, states that for any type `α`, given a finite set `s` of type `α` and an element `a` of type `α`, the singleton set `{a}` is a subset of `s` if and only if `a` is an element of `s`. In other words, the singleton set `{a}` being a subset of `s` is equivalent to the condition that `a` belongs to `s`. More concisely: For any type `α` and any finite set `s` of type `α` and element `a` of type `α`, the singleton set `{a}` is a subset of `s` if and only if `a` is an element of `s`. In mathematical notation, `{a} ⊆ s` if and only if `a ∈ s`.
`Finset.filter_mem_eq_inter` theorem Finset.filter_mem_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} [inst_1 : (i : α) → Decidable (i ∈ t)], Finset.filter (fun i => i ∈ t) s = s ∩ t This theorem states that for any type `α` with decidable equality, and for any two finite sets `s` and `t` of type `α`, the operation of filtering `s` by the membership predicate for `t` (i.e., selecting all elements of `s` that are also in `t`) is equivalent to the intersection of `s` and `t`. More succinctly, given decidable predicates for equality and set membership in `α`, filtering a finite set `s` to find the elements in another set `t` is the same as finding the intersection of `s` and `t`. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, the set of elements in `s` that are also in `t` (obtained by filtering `s` with the membership predicate for `t`) equals the intersection of `s` and `t`.
`Finset.mem_def` theorem Finset.mem_def : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ s ↔ a ∈ s.val This theorem states that for any type `α`, any element `a` of that type, and any finite set `s` of type `α`, `a` is a member of `s` if and only if `a` is a member of the underlying value of `s`. This essentially means that an element's membership in a finite set is equivalent to its membership in the set's internal representation. More concisely: For any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, `a` is an element of `s` if and only if `a` is an element of the underlying set of `s`.
`Mathlib.Data.Finset.Basic._auxLemma.32` theorem Mathlib.Data.Finset.Basic._auxLemma.32 : ∀ {α : Type u_1} (a : α), ({a} = ∅) = False This theorem states that for any type `α`, and any element `a` of that type, the singleton set containing only `a` is not equal to the empty set. In other words, a set containing at least one element, `a`, cannot be empty. This statement holds universally, regardless of the particular type `α` and element `a`. More concisely: For any type `α` and element `a` of `α`, the singleton set `{a : α}` is not equal to the empty set.
`Finset.range_one` theorem Finset.range_one : Finset.range 1 = {0} The theorem `Finset.range_one` states that the set of natural numbers less than 1 (`Finset.range 1`) is the set containing only the number 0. In other words, the range of 1 in the set of natural numbers, as defined in the `Finset.range` function, is simply the set `{0}`. More concisely: The set of natural numbers less than 1 is equal to the singleton set {0}.
`Finset.coe_union` theorem Finset.coe_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂ := by sorry This theorem is stating that for any given type `α` which has decidable equality, and any two finite sets `s₁` and `s₂` of type `α`, the underlying set of the union of `s₁` and `s₂` is equal to the union of the underlying sets of `s₁` and `s₂`. In other words, it says that the operation of taking the union of two finite sets commutes with the operation of taking the underlying set of a finite set. More concisely: For any type `α` with decidable equality and finite sets `s₁` and `s₂` of type `α`, the underlying set of `s₁ ∪ s₂` equals the underlying set of `s₁ �∪ s₂`.
`Finset.disjoint_sdiff_inter` theorem Finset.disjoint_sdiff_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Disjoint (s \ t) (s ∩ t) This theorem states that for any given type `α` with decidable equality and any two finite sets `s` and `t` of this type, the set difference (denoted by `s \ t`) and the intersection (denoted by `s ∩ t`) of `s` and `t` are disjoint. In other words, there is no element in `α` that can be less than or equal to both the set difference and the intersection of `s` and `t`. Here, the notion of "less than or equal to" is with respect to the partial order defined in the `α` type's lattice structure, and 'disjoint' means that the greatest lower bound (infimum) of the two sets is the bottom element of the lattice. More concisely: For any type `α` with decidable equality, the set differences and intersections of two finite sets `s` and `t` in `α` are disjoint with respect to the lattice structure, meaning their infimum is the bottom element.
`Finset.inter_subset_inter` theorem Finset.inter_subset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {x y s t : Finset α}, x ⊆ y → s ⊆ t → x ∩ s ⊆ y ∩ t This theorem states that for any type `α` equipped with a decidable equality operation, given four finite sets `x`, `y`, `s`, and `t` of this type, if `x` is a subset of `y` and `s` is a subset of `t`, then the intersection of `x` and `s` is a subset of the intersection of `y` and `t`. This is a generalization of the principle from set theory that intersecting with a subset yields a subset of the original intersection. More concisely: For any type `α` with decidable equality, if `x` is a subset of `y` and `s` is a subset of `t`, then the intersection of `x` and `s` is a subset of the intersection of `y` and `t`.
`Finset.insert_erase` theorem Finset.insert_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a (s.erase a) = s This theorem, called `Finset.insert_erase`, states that for any type `α` that has decidable equality (`DecidableEq α`), for any finite set `s` of type `α` (`Finset α`), and for any element `a` of type `α`, if `a` is an element of `s` (`a ∈ s`), then inserting `a` into the set obtained from `s` by erasing `a` (`insert a (Finset.erase s a)`) results in the original set `s`. In other words, if you remove an element from a set and then add it back, you get the original set. More concisely: For any type `α` with decidable equality and any finite set `s` of type `α`, `insert a (Finset.erase s a) = s`, where `a` is an element of `s`.
`Mathlib.Data.Finset.Basic._auxLemma.46` theorem Mathlib.Data.Finset.Basic._auxLemma.46 : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x) This theorem states that for any type `α` and any two predicates `p` and `q` on `α`, the assertion that for every element of `α` both `p` and `q` hold is equivalent to the assertion that for every element of `α`, `p` holds and for every element of `α`, `q` holds. In other words, it shows the equivalence between the global conjunction of two properties and the conjunction of their global truth. More concisely: For any type `α` and predicates `p` and `q` on `α`, the assertion that for all `x : α`, `p x` and `q x` hold is equivalent to the assertion that for all `x : α`, `p x` holds and for all `x : α`, `q x` holds.
`Finset.union_insert` theorem Finset.union_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), s ∪ insert a t = insert a (s ∪ t) The theorem `Finset.union_insert` states that for any type `α` with decidable equality, and for any element `a` of type `α` and sets `s` and `t` of type `Finset α` (finite sets of `α`), the union of `s` and the insertion of `a` into `t` is equal to the insertion of `a` into the union of `s` and `t`. In other words, it doesn't matter whether we first insert an element into a set and then take the union, or first take the union and then insert the element; the result will be the same. More concisely: For any type `α` with decidable equality, and finite sets `s` and `t` of type `Finset α` and element `a` of type `α`, `a ∉ s → s ∪ {a} = {a} ∪ s`. (Assuming `{a} ∪ s` and `s ∪ {a}` mean the set union of `s` and `{a}` and `{a}` and `s` respectively, and `a ∉ s` denotes that `a` is not an element of `s`.)
`Finset.erase_ssubset` theorem Finset.erase_ssubset : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∈ s → s.erase a ⊂ s The theorem `Finset.erase_ssubset` states that for any type `α` with decidable equality, any element `a` of type `α`, and any finite set `s` of elements of type `α`, if `a` is an element of `s`, then the set resulting from erasing `a` from `s` (denoted as `Finset.erase s a`) is a strict subset of `s`. In other words, removing an element from a set results in a smaller set. More concisely: For any type `α` with decidable equality, if `a` is an element of a finite set `s` of type `α`, then `Finset.erase s a` is a strict subset of `s`.
`Finset.union_subset_right` theorem Finset.union_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ t ⊆ u → t ⊆ u := by sorry The theorem `Finset.union_subset_right` asserts that for any type `α` with decidable equality, and for any three finite sets (`Finset`) `s`, `t`, and `u` of type `α`, if the union of `s` and `t` is a subset of `u`, then `t` is a subset of `u`. More concisely: If `s` and `t` are finite sets and `s ∪ t` is a subset of `u`, then `t` is a subset of `u`.
`List.mem_toFinset` theorem List.mem_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, a ∈ l.toFinset ↔ a ∈ l := by sorry This theorem states that, for any type `α` which has decidable equality, any list `l` of type `α`, and any element `a` of type `α`, the element `a` is a member of the finset obtained by removing duplicates from the list `l` if and only if `a` is a member of the list `l` itself. In other words, converting a list to a finset does not affect the membership of an element in the list. More concisely: For any type `α` with decidable equality, any list `l` of `α`, and any element `a` of `α`, `a` is in the finset obtained by removing duplicates from `l` if and only if `a` is in `l`.
`Multiset.toFinset_nsmul` theorem Multiset.toFinset_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (n : ℕ), n ≠ 0 → (n • s).toFinset = s.toFinset The theorem `Multiset.toFinset_nsmul` states that for any type `α` with decidable equality, for any multiset `s` of type `α`, and for any natural number `n` that is not zero, the finset obtained by removing duplicates from the multiset resulting from `n` times scalar multiplication of `s` is equal to the finset obtained by removing duplicates from `s` itself. In other words, multiple scalar multiplication of a multiset does not change the set of unique elements in the multiset. More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, the finset obtained from `n` times scalar multiplication of `s` (without duplicates) is equal to the finset `s` itself (without duplicates), for any non-zero natural number `n`.
`Finset.sdiff_disjoint` theorem Finset.sdiff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint (t \ s) s The theorem `Finset.sdiff_disjoint` states that for any type `α` which has a decidable equality and given any two finite sets `s` and `t` of type `α`, the set difference `t \ s` is disjoint with set `s`. In the context of lattice theory, two elements are disjoint if their greatest lower bound (infimum) is the bottom element. Here, it implies that there is no element in the set `s` that is also in the set `t \ s`, that is, the set `s` and the set `t \ s` have no common elements. More concisely: For finite sets `s` and `t` of type `α` with decidable equality, `s` has no elements in common with the set difference `t \ s`.
`Finset.Nonempty.eq_singleton_default` theorem Finset.Nonempty.eq_singleton_default : ∀ {α : Type u_1} [inst : Unique α] {s : Finset α}, s.Nonempty → s = {default} This theorem, `Finset.Nonempty.eq_singleton_default`, states that for any non-empty finite set `s` of a type `α`, if `α` has a unique value (denoted by `[inst : Unique α]`), then the set `s` is equal to a singleton set containing only this unique value (denoted by `{default}`). In other words, in the context where there is only one value of a certain type, any non-empty finite set of that type can only contain that unique value. More concisely: Given a non-empty finite set `s` of a type `α` with a unique value `default`, then `s` equals the singleton set `{default}`.
`Finset.filter_subset_filter` theorem Finset.filter_subset_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s t : Finset α}, s ⊆ t → Finset.filter p s ⊆ Finset.filter p t The theorem `Finset.filter_subset_filter` states that for any type `α`, and any decidable predicate `p` over `α`, if a finite set `s` is a subset of another finite set `t` (both of type `α`), then the set obtained by filtering `s` using predicate `p` is a subset of the set obtained by filtering `t` using the same predicate. In other words, if we have two finite sets `s` and `t` such that every element of `s` is also an element of `t`, then all elements of `s` that satisfy a certain condition (defined by `p`) will also be part of the set of elements of `t` satisfying the same condition. This theorem thus deals with the preservation of subset relations under the operation of filtering sets based on some criterion. More concisely: For any type `α` and decidable predicate `p` over `α`, if `s` is a subset of `t` (both finite sets of `α`), then the filtered sets `s \| p` and `t \| p` satisfy the subset relation.
`Finset.val_toFinset` theorem Finset.val_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.val.toFinset = s This theorem, `Finset.val_toFinset`, states that for any type `α` that has decidable equality (denoted by `DecidableEq α`), for any `Finset` `s` of type `α`, if we convert the underlying multiset of `s` (represented by `s.val`) into a `Finset` using the `Multiset.toFinset` function, we get `s` itself. In other words, the operation of removing duplicates from the multiset of a `Finset` and converting it back to a `Finset` leaves the original `Finset` unchanged. More concisely: For any type `α` with decidable equality and any `Finset` `s` of type `α`, the conversion of `s.val` to a `Finset` using `Multiset.toFinset` equals `s`.
`Finset.coe_nonempty` theorem Finset.coe_nonempty : ∀ {α : Type u_1} {s : Finset α}, (↑s).Nonempty ↔ s.Nonempty The theorem `Finset.coe_nonempty` states that for any given type `α` and any finite set `s` of that type, the property that the set `s` is nonempty (which means it contains at least one element) is equivalent to the property that the coercion of `s` to a set is also nonempty. In other words, a finite set `s` is nonempty if and only if the corresponding set `↑s` (obtained by forgetting that `s` is finite) is nonempty. More concisely: A finite set `s` of type `α` is nonempty if and only if the coerced set `↑s` is nonempty.
`Finset.union_eq_right` theorem Finset.union_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t = t ↔ s ⊆ t This theorem states that for any given type `α` that has decidable equality (meaning that given any two elements of type `α`, we can decide whether they are equal or not), and for any two finite sets `s` and `t` of type `α`, the union of `s` and `t` is equal to `t` if and only if `s` is a subset of `t`. In other words, if every element in `s` is also in `t`, then the union of `s` and `t` will be the same as `t`. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, `s ∪ t = t` if and only if `s ⊆ t`.
`Finset.union_eq_left` theorem Finset.union_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t = s ↔ t ⊆ s The theorem `Finset.union_eq_left` states that for any type `α` with decidable equality and for any two finite sets `s` and `t` of type `α`, the union of `s` and `t` is equal to `s` if and only if `t` is a subset of `s`. In other words, adding all elements of `t` to `s` doesn't change `s` if every element of `t` is already in `s`. More concisely: For any type `α` with decidable equality and for finite sets `s` and `t` of type `α`, `s ∪ t = s` if and only if `t ⊆ s`.
`Finset.eq_of_not_mem_of_mem_insert` theorem Finset.eq_of_not_mem_of_mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ insert a s → b ∉ s → b = a This theorem states that for any type `α` with decidable equality, given a finite set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `b` belongs to the set obtained by inserting `a` into `s` (`b ∈ insert a s`), and `b` does not belong to the original set `s` (`b ∉ s`), then `b` must be equal to `a` (`b = a`). In other words, the theorem asserts that, when inserting an element into a finite set, any new element found in the resulting set, which was not in the original, must be the one that was inserted. More concisely: Given a finite type `α` with decidable equality, if `a` is an element of `α` not in a finite set `s` of type `α`, and `insert a s` contains an element `b` not equal to `a`, then `b = a`.
`Finset.coe_eq_empty` theorem Finset.coe_eq_empty : ∀ {α : Type u_1} {s : Finset α}, ↑s = ∅ ↔ s = ∅ This theorem states that for any type `α` and any finite set `s` of type `α`, the coercion of `s` to a set results in the empty set if and only if `s` itself is the empty set. In other words, a finite set in Lean is empty if and only if its set-theoretic counterpart is also empty. More concisely: For any type `α`, the coercion of a finite set `s` of type `α` to a set is the empty set if and only if `s` is the empty set.
`Finset.insert_union` theorem Finset.insert_union : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), insert a s ∪ t = insert a (s ∪ t) The theorem `Finset.insert_union` asserts that for any type `α` that has a decidable equality, given an element `a` of type `α` and two finite sets `s` and `t` of type `α`, inserting `a` into the union of `s` and `t` is the same as the union of the set obtained by inserting `a` into `s` and the set `t`. This states a fundamental property of sets: the order of insertion and union operations does not change the resulting set. More concisely: For any type `α` with decidable equality, the set `(s ∪ t).insert a` is equal to `(s.insert a ∪ t)`, where `s` and `t` are finite sets of type `α` and `a` is an element of type `α`.
`Finset.choose_spec` theorem Finset.choose_spec : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a), Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp) The theorem `Finset.choose_spec` states that for any type `α`, a predicate `p` on `α` that is decidable, and a finite set `l` of elements of type `α`, if there exists exactly one element `a` in `l` that satisfies the predicate `p`, then the element returned by the `Finset.choose` function for `p`, `l` and the proof of uniqueness, is contained in `l` and satisfies predicate `p`. In other words, the function `Finset.choose` correctly identifies the unique element in the finite set that satisfies the given decidable predicate. More concisely: If `p` is a decidable predicate on a type `α`, and `l` is a finite set of elements from `α` with exactly one element satisfying `p`, then `Finset.choose l p` is defined and is that element.
`Finset.sdiff_inter_self_left` theorem Finset.sdiff_inter_self_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ (s ∩ t) = s \ t This theorem states that for any type `α` that has a decidable equality, and for any two finite sets `s` and `t` of elements of type `α`, the difference of `s` and the intersection of `s` and `t` is equal to the difference of `s` and `t`. In mathematical terms, it means that for all sets `s` and `t`, we have `s \ (s ∩ t) = s \ t`. This is a property related to set operations. More concisely: For any finite sets `s` and `t` of a type `α` with decidable equality, the difference `s \ (s ∩ t)` equals `s \ t`.
`Finset.insert_eq` theorem Finset.insert_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), insert a s = {a} ∪ s := by sorry The theorem `Finset.insert_eq` states that for any given type `α` with decidable equality, for any element `a` of type `α`, and for any finite set `s` of elements of type `α`, inserting the element `a` into the set `s` is equivalent to forming the union of the singleton set containing `a` and the set `s`. More concisely: For any decidably equated type `α` and any finite set `s` of elements from `α`, the singleton set `{a}` and the set `s ∪ {a}` are equal. (Here, `a` is an arbitrary element of type `α`.)
`Finset.val_inj` theorem Finset.val_inj : ∀ {α : Type u_1} {s t : Finset α}, s.val = t.val ↔ s = t This theorem states that for any two finite sets `s` and `t` of some type `α`, the equivalence between the underlying value lists of `s` and `t` is the same as the equivalence between `s` and `t` themselves. In other words, if the lists of values for `s` and `t` are identical, then the two finite sets `s` and `t` are also identical, and vice versa. More concisely: For any type `α` and finite sets `s` and `t` of type `α`, `list.eq s t` if and only if `s = t`.
`Finset.filter_union` theorem Finset.filter_union : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s₁ s₂ : Finset α), Finset.filter p (s₁ ∪ s₂) = Finset.filter p s₁ ∪ Finset.filter p s₂ The theorem `Finset.filter_union` states that for any type `α`, any predicate `p` on `α` that is decidable, any two finite sets `s₁` and `s₂` of `α`, and given that equality in `α` is decidable, filtering the union of `s₁` and `s₂` with the predicate `p` is the same as taking the union of the filter of `s₁` with `p` and the filter of `s₂` with `p`. In other words, it asserts that the operation of filtering a finite set with a decidable predicate distributes over the operation of taking the union of two finite sets, much like how multiplication distributes over addition in basic arithmetic. More concisely: For any decidable predicate `p` on a type `α` and finite sets `s₁` and `s₂` of `α` with decidable equality, `(s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p`.
`Finset.disjoint_left` theorem Finset.disjoint_left : ∀ {α : Type u_1} {s t : Finset α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t This theorem is about the concept of "disjoint" subsets in the context of finite sets, or "finsets", in Lean 4. It states that for all types `α` and all finite sets `s` and `t` of type `α`, `s` and `t` are disjoint if and only if for every element `a` of type `α`, if `a` is in `s` then `a` is not in `t`. In other words, two finite sets are disjoint if they have no elements in common. More concisely: Two finite sets `s` and `t` of type `α` in Lean 4 are disjoint if and only if they have no common elements.
`Finset.Subset.trans` theorem Finset.Subset.trans : ∀ {α : Type u_1} {s₁ s₂ s₃ : Finset α}, s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ This theorem, `Finset.Subset.trans`, states that for any three finite sets (`Finset`) `s₁`, `s₂`, and `s₃` of any type `α`, if `s₁` is a subset of `s₂` and `s₂` is a subset of `s₃`, then `s₁` is also a subset of `s₃`. This is a formal statement of the transitivity property for subset relations among finite sets. More concisely: If `s₁ ⊆ s₂` and `s₂ ⊆ s₃`, then `s₁ ⊆ s₃` (`s₁` is a subset of `s₃` if `s₁` is a subset of `s₂` and `s₂` is a subset of `s₃`).
`Finset.mk.injEq` theorem Finset.mk.injEq : ∀ {α : Type u_4} (val : Multiset α) (nodup : val.Nodup) (val_1 : Multiset α) (nodup_1 : val_1.Nodup), ({ val := val, nodup := nodup } = { val := val_1, nodup := nodup_1 }) = (val = val_1) The theorem `Finset.mk.injEq` states that for any type `α`, and for any two multisets `val` and `val_1` of type `α` that have no duplicate elements (satisfying the `Multiset.Nodup` condition), the equality of two `Finset` objects, each constructed with `val` and `val_1` respectively along with their no-duplicates properties, is equivalent to the equality of `val` and `val_1` themselves. This implies that two `Finset`s are identical if and only if their underlying multisets are identical. More concisely: For any type `α` and multisets `val` and `val_1` of type `α` with no duplicate elements, the equality of the `Finset` objects constructed from `val` and `val_1` respectively implies and is implied by the equality of `val` and `val_1`.
`Mathlib.Data.Finset.Basic._auxLemma.94` theorem Mathlib.Data.Finset.Basic._auxLemma.94 : ∀ {a b c : Prop}, (a ∧ b ∧ c) = (b ∧ a ∧ c) This theorem states that in the realm of propositional logic, the order of conjunctions does not affect the truth value of the overall statement. More specifically, for any propositions `a`, `b`, and `c`, the conjunction `a ∧ b ∧ c` (read as "a and b and c") is logically equivalent to the conjunction `b ∧ a ∧ c` (read as "b and a and c"). This is a demonstration of the commutative property of conjunction in logic. More concisely: In propositional logic, the order of conjuncted propositions does not affect their truth value, i.e., `a ∧ b ∧ c` is logically equivalent to `b ∧ a ∧ c` for all propositions `a`, `b`, and `c`.
`Finset.nonempty_range_succ` theorem Finset.nonempty_range_succ : ∀ {n : ℕ}, (Finset.range (n + 1)).Nonempty This theorem states that for every natural number `n`, the set of natural numbers less than `n + 1` (represented by `Finset.range (n + 1)`) is not empty. This is intuitively clear as the set of numbers less than `n + 1` always contains at least the number `n`, hence it is indeed non-empty. More concisely: For every natural number `n`, the finite set of natural numbers `{i \| i < n + 1}` is non-empty.
`Finset.sdiff_inter_self_right` theorem Finset.sdiff_inter_self_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ (t ∩ s) = s \ t The theorem `Finset.sdiff_inter_self_right` states that for any two finite sets `s` and `t` of any type `α` that has a decidable equality, the symmetric difference of `s` with the intersection of `t` and `s` is the same as the symmetric difference of `s` with `t`. In other words, removing the elements of `s` that are in both `t` and `s` is the same as removing the elements of `s` that are in `t`. More concisely: For finite sets `s` and `t` of type `α` with decidable equality, `(s \ (s ∩ t)) = (s \ t)`.
`Finset.not_mem_range_self` theorem Finset.not_mem_range_self : ∀ {n : ℕ}, n ∉ Finset.range n The theorem `Finset.not_mem_range_self` states that for any natural number `n`, `n` is not an element of the set of natural numbers less than `n`. In other words, any given natural number `n` is not included in its own range. More concisely: For all natural numbers `n`, `n` is not an element of the finite set of natural numbers less than `n`.
`Finset.singleton_subset_set_iff` theorem Finset.singleton_subset_set_iff : ∀ {α : Type u_1} {s : Set α} {a : α}, ↑{a} ⊆ s ↔ a ∈ s This theorem states that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, the singleton set containing only `a` is a subset of `s` if and only if `a` is an element of `s`. In other words, every element of the singleton set `{a}` is in `s` exactly when `a` itself is in `s`. This theorem bridges the relationship between set membership and subset relation for singleton sets. More concisely: For any type `α` and set `s` of type `α`, the singleton set {`a`} is a subset of `s` if and only if `a` is an element of `s`.
`Mathlib.Data.Finset.Basic._auxLemma.113` theorem Mathlib.Data.Finset.Basic._auxLemma.113 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑s \ {a} = ↑(s.erase a) The theorem `Mathlib.Data.Finset.Basic._auxLemma.113` states that for any type `α` that has decidable equality, and for any element `a` of type `α` and any finite set `s` of elements of type `α`, removing the element `a` from the set `s` in two different ways leads to the same result. More specifically, it states that the set difference of `s` and the singleton set `{a}` is equal to the set obtained by using the `Finset.erase` function to remove `a` from `s`. More concisely: For any type `α` with decidable equality and any finite set `s` of elements from `α` and any `a` in `s`, the set difference `s \ {a}` is equal to the set obtained by erasing `a` from `s` using the `Finset.erase` function.
`Mathlib.Data.Finset.Basic._auxLemma.20` theorem Mathlib.Data.Finset.Basic._auxLemma.20 : ∀ {α : Type u_1} (a : α), (a ∈ ∅) = False This theorem, from the Mathlib library in Lean 4, states that for any type `α` and for any element `a` of type `α`, the element `a` does not belong to an empty set. In mathematical notation, this can be represented as `∀ α, a : α, a ∉ ∅`. More concisely: For any type `α` and element `a` of type `α`, `a` is not an element of the empty set. In mathematical notation, `∀ α a : α, a ∉ ∅`.
`Finset.induction_on_union` theorem Finset.induction_on_union : ∀ {α : Type u_1} [inst : DecidableEq α] (P : Finset α → Finset α → Prop), (∀ {a b : Finset α}, P a b → P b a) → (∀ {a : Finset α}, P a ∅) → (∀ {a b : α}, P {a} {b}) → (∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c) → ∀ (a b : Finset α), P a b This theorem states that to establish a relation (denoted by P) between pairs of finite sets (referred to as `Finset`) of some type `α` that has decidable equality, we need to satisfy four conditions: 1. The relation is symmetric, i.e., if the relation holds between a finite set `a` and another finite set `b`, then it also holds between `b` and `a`. 2. The relation holds between any finite set `a` and the empty set. 3. The relation holds for pairs of single-element finite sets. 4. If the relation holds for a finite set `a` and another finite set `c`, and it also holds for a finite set `b` and `c`, then it holds for the union of `a` and `b` (`a ∪ b`) and `c`. If these conditions are fulfilled, then for any pair of finite sets `a` and `b`, the relation P holds. More concisely: Given a decidable equality relation P on finite sets of type α, if P is symmetric, holds for every finite set and the empty set, and is transitive, then P holds for any two finite sets.
`Multiset.toFinset_eq` theorem Multiset.toFinset_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (n : s.Nodup), { val := s, nodup := n } = s.toFinset := by sorry This theorem states that for any type `α` which has a decidable equality and for any multiset `s` of type `α` which contains no duplicate elements, the finset created by the `{ val := s, nodup := n }` expression is equivalent to the finset obtained by applying the `Multiset.toFinset` function to `s`. Here, `n` is the stated property that `s` contains no duplicates. Hence, if a multiset has no duplicates, explicitly creating a finset from it or using `Multiset.toFinset` function yields the same result. More concisely: For any decidably equated type `α` and multiset `s` of `α` without duplicates, the finset constructed from `s` using the `{ val := s, nodup := true }` expression is equal to the finset obtained by applying `Multiset.toFinset` to `s`.
`Finset.singleton_ne_empty` theorem Finset.singleton_ne_empty : ∀ {α : Type u_1} (a : α), {a} ≠ ∅ This theorem states that for any type `α` and any element `a` of type `α`, a finite set (`Finset`) that contains only `a` is not equal to the empty set. In mathematical terms, a singleton set (a set containing exactly one element) is never considered to be empty. More concisely: For any type `α` and any element `a` of type `α`, the singleton set `{a}` is not equal to the empty set.
`Finset.sdiff_union_inter` theorem Finset.sdiff_union_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ t ∪ s ∩ t = s := by sorry This theorem, `Finset.sdiff_union_inter`, states that for any type `α` which has a decidable equality and for any two finite sets `s` and `t` of type `α`, the union of the set difference of `s` and `t` and the intersection of `s` and `t` is equal to `s`. In other words, the elements of `s` that are not in `t` combined with the elements that `s` and `t` have in common together form `s`. This is an application of the principle of set theory that the union of the difference and intersection of two sets equals the first set. More concisely: For sets `s` and `t` of type `α` with decidable equality, `s = (s \ t) ∪ (s ∩ t)`.
`Finset.union_subset` theorem Finset.union_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ u → t ⊆ u → s ∪ t ⊆ u The `Finset.union_subset` theorem states that for any type `α` that has decidable equality, and for any three finite sets `s`, `t`, and `u` of type `α`, if `s` is a subset of `u` and `t` is a subset of `u`, then the union of `s` and `t` is also a subset of `u`. This is a fundamental property of subsets in set theory. More concisely: If `s` and `t` are finite subsets of type `α` with decidable equality, and `s ⊆ u` and `t ⊆ u` hold, then `s ∪ t ⊆ u`.
`Finset.range_subset` theorem Finset.range_subset : ∀ {n m : ℕ}, Finset.range n ⊆ Finset.range m ↔ n ≤ m The theorem `Finset.range_subset` states that for any two natural numbers `n` and `m`, the set of natural numbers less than `n` is a subset of the set of natural numbers less than `m` if and only if `n` is less than or equal to `m`. In other words, if all natural numbers less than `n` are also less than `m`, then `n` must be less than or equal to `m`. More concisely: For all natural numbers n and m, the set {i : ℕ \| i < n} is subset of {i : ℕ \| i < m} if and only if n ≤ m.
`Finset.coe_range` theorem Finset.coe_range : ∀ (n : ℕ), ↑(Finset.range n) = Set.Iio n This theorem states that for any natural number 'n', the coercion of the set of natural numbers less than 'n' (denoted as 'Finset.range n') is equal to the left-infinite right-open interval of 'n' (denoted as 'Set.Iio n'). In other words, the set of all natural numbers less than a given natural number 'n' and the left-infinite interval of 'n' are equivalent sets. Here, the left-infinite right-open interval is a set of all elements 'x' such that 'x' is less than 'n'. The coercive function (↑) is used to convert the 'Finset' object into a 'Set' object. More concisely: For any natural number n, the coercion of the finite set of natural numbers less than n to a set equals the left-infinite right-open interval of n. In Lean syntax, `Finset.range n ≈ Set.Iio n`.
`Finset.inter_comm` theorem Finset.inter_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∩ s₂ = s₂ ∩ s₁ The theorem `Finset.inter_comm` asserts that for any type `α` with decidable equality (meaning, we can always determine whether two elements of type `α` are equal or not), and for any two finite sets `s₁` and `s₂` of type `α`, the intersection of `s₁` and `s₂` is equal to the intersection of `s₂` and `s₁`. In other words, the operation of intersection on finite sets is commutative. More concisely: For any type `α` with decidable equality and any finite sets `s₁` and `s₂` of type `α`, `s₁ ∩ s₂ = s₂ ∩ s₁`.
`Finset.toList_eq_nil` theorem Finset.toList_eq_nil : ∀ {α : Type u_1} {s : Finset α}, s.toList = [] ↔ s = ∅ This theorem states that for any type `α` and for any finite set `s` of type `α`, the list produced from the finite set `s` using the function `Finset.toList` is empty if and only if the set `s` is empty. In other words, `Finset.toList` returning an empty list is equivalent to the finite set being empty. More concisely: For any type `α`, the list obtained from a finite set `s` of type `α` using `Finset.toList` is empty if and only if `s` is empty.
`Finset.inter_self` theorem Finset.inter_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∩ s = s The theorem `Finset.inter_self` states that for any type `α` that has a decidable equality and for any finite set `s` of type `α`, the intersection of `s` with itself is equal to `s` itself. In other words, if you take a finite set and intersect it with itself, you get the original set back. This makes sense intuitively, as all elements in `s` are certainly in `s`, so the intersection of `s` and `s` contains exactly the same elements as `s`. More concisely: For any finite set `s` of type `α` with decidable equality, `s ∩ s = s`.
`Mathlib.Data.Finset.Basic._auxLemma.17` theorem Mathlib.Data.Finset.Basic._auxLemma.17 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ s) = (a ∈ s.val) := by sorry This theorem, `Mathlib.Data.Finset.Basic._auxLemma.17`, states that for any type `α`, any element `a` of type `α`, and any finite set `s` of type `α`, the predicate of `a` being an element of `s` is equivalent to `a` being an element of the underlying value of `s`. In other words, checking if an element is in a `Finset` is the same as checking if it is in the underlying set of values. More concisely: For any type `α`, the membership relation between an element `a` of `α` and a finite set `s` of type `Finset α` is the same as the membership relation between `a` and the underlying set of `s`.
`Finset.filter_union_filter_neg_eq` theorem Finset.filter_union_filter_neg_eq : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] [inst_2 : (x : α) → Decidable ¬p x] (s : Finset α), Finset.filter p s ∪ Finset.filter (fun a => ¬p a) s = s This theorem states that for any given type `α`, a predicate `p` on `α` which is decidable (meaning it is possible to determine whether `p` holds for any element of `α`), and any finite set `s` of `α`, the union of the set of elements in `s` that satisfy `p` and the set of elements in `s` that do not satisfy `p` is equal to `s` itself. In other words, if you partition a finite set based on whether a given decidable predicate is true or false, and then recombine those parts, you get back the original set. This holds for any decidable equality on `α`. More concisely: For any finite type `α` with decidable equality, and decidable predicate `p` on `α`, the sets `{x : α \| p x}` and `{x : α \| ¬p x}` have a disjoint union equal to `α`.
`Mathlib.Data.Finset.Basic._auxLemma.92` theorem Mathlib.Data.Finset.Basic._auxLemma.92 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a) This theorem, named Mathlib.Data.Finset.Basic._auxLemma.92, establishes the commutativity of logical conjunction in propositional logic. Specifically, it states that for any two propositions `a` and `b`, the statement "`a` and `b`" is equivalent to the statement "`b` and `a`". In LaTeX mathematics, this theorem can be written as: ∀ {a b : Prop}, (a ∧ b) = (b ∧ a). More concisely: The theorem asserts the equality of conjunction commutativity in propositional logic: for all propositions `a` and `b`, `(a ∧ b) = (b ∧ a)`.
`Finset.eq_of_veq` theorem Finset.eq_of_veq : ∀ {α : Type u_1} {s t : Finset α}, s.val = t.val → s = t This theorem states that for any two finite sets `s` and `t` of an arbitrary type `α`, if the underlying value sequences of `s` and `t` are equal, then `s` and `t` must also be equal. The type `α` is not necessarily a number type, but can be any type. This theorem provides a method of equality comparison between two finite sets based on their value sequences. More concisely: If two finite sets `s` and `t` over an arbitrary type `α` have equal value sequences, then `s` and `t` are equal.
`Finset.subset_union_right` theorem Finset.subset_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₂ ⊆ s₁ ∪ s₂ The theorem `Finset.subset_union_right` states that for any given type `α` that has decidable equality, and any two finite sets (`Finset`) `s₁` and `s₂` of type `α`, the set `s₂` is a subset of the union of `s₁` and `s₂`. This is a basic property of sets, which essentially says that if you take a set and union it with another set, the resulting set will always contain the second set. More concisely: For any type `α` with decidable equality and finite sets `s₁` and `s₂` of type `Finset α`, `s₂` is a subset of `s₁ ∪ s₂`.
`Finset.mem_of_mem_erase` theorem Finset.mem_of_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s.erase a → b ∈ s This theorem states that for any type `α` that has decidable equality, and for any `Finset` of `α` named `s`, and for any elements `a` and `b` of `α`, if `b` is an element of the set obtained by erasing `a` from `s`, then `b` is also an element of `s`. In other words, if you remove an element `a` from a finite set `s` and `b` is in the resulting set, then `b` was definitely an element of the original set `s`. More concisely: For any type `α` with decidable equality and any finite set `s` of `α` containing an element `a`, if `b` is in the set `s \ {a}`, then `b` is in `s`.
`Finset.subset_insert_iff` theorem Finset.subset_insert_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Finset α}, s ⊆ insert a t ↔ s.erase a ⊆ t This theorem states that for any type `α` with decidable equality, given an element `a` of type `α`, and two finite sets `s` and `t` of the same type, the set `s` is a subset of the set obtained by inserting `a` into `t` if and only if the set obtained by erasing `a` from `s` is a subset of `t`. This theorem essentially relates the operations of inserting an element into a set and erasing an element from a set with the concept of subset inclusion. More concisely: For any type `α` with decidable equality, and sets `s` and `t` of type `α`, `s ⊆ t` if and only if `s \ {a} ⊆ t` for all `a` in `α`.
`Finset.nonempty_range_iff` theorem Finset.nonempty_range_iff : ∀ {n : ℕ}, (Finset.range n).Nonempty ↔ n ≠ 0 This theorem states that for any natural number `n`, the range of `n` (which is defined as the set of natural numbers less than `n`) is non-empty if and only if `n` is not equal to zero. In other words, there exist natural numbers less than `n` precisely when `n` is not zero. More concisely: The set of natural numbers less than a given natural number `n` is non-empty if and only if `n` is non-zero.
`Finset.val_injective` theorem Finset.val_injective : ∀ {α : Type u_1}, Function.Injective Finset.val The theorem `Finset.val_injective` states that for all types `α`, the function `Finset.val` is injective. In other words, if two finsets have the same multiset of elements (as given by `Finset.val`), then the two finsets are themselves the same. This corresponds to the property of injectivity, where if `f(x) = f(y)` then `x = y`, applied to our function `Finset.val`. More concisely: If two finsets have the same multiset of elements, then they are equal.
`Mathlib.Data.Finset.Basic._auxLemma.108` theorem Mathlib.Data.Finset.Basic._auxLemma.108 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, (s.erase a = s) = (a ∉ s) This theorem states that for any type `α` with decidable equality, any finite set `s` of elements of type `α`, and any element `a` of type `α`, the statement that the result of "erasing" `a` from `s` is equal to `s` itself, is equivalent to the statement that `a` is not an element of `s`. In other words, if removing an element from a set results in the same set, then that element was not in the set to begin with. More concisely: For any type `α` with decidable equality, a finite set `s` of elements from `α`, and an element `a` not in `s`, the set `s` with `a` removed is equal to `s` if and only if `a` was not an element of `s` to begin with.
`Finset.mem_range` theorem Finset.mem_range : ∀ {n m : ℕ}, m ∈ Finset.range n ↔ m < n This theorem states that for any two natural numbers 'n' and 'm', 'm' is a member of the set 'Finset.range n' if and only if 'm' is less than 'n'. In other words, a natural number 'm' belongs to the set of natural numbers less than 'n' exactly when 'm' is less than 'n'. More concisely: For any natural numbers n and m, m is an element of Finset.range n if and only if m < n.
`Finset.mem_union_left` theorem Finset.mem_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t The theorem `Finset.mem_union_left` states that for any type `α` that has decidable equality (denoted by `DecidableEq α`), for any finite set `s` of `α` (denoted by `Finset α`), and for any element `a` of `α`, if `a` is a member of `s`, then `a` is also a member of the union of `s` and any other finite set `t` of `α`. In other words, if an element belongs to a set, then it belongs to the union of that set with any other set. More concisely: If `α` has decidable equality and `s` is a finite set of `α`, then for all `a` in `α` such that `a` is in `s`, `a` is also in `s ∪ t`.
`Finset.eq_of_mem_of_not_mem_erase` theorem Finset.eq_of_mem_of_not_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s → b ∉ s.erase a → b = a This theorem states that for any type `α` equipped with a decidable equality relation, given a finite set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `b` is an element of `s` and `b` is not an element of the set obtained by erasing `a` from `s`, then `b` must be equal to `a`. In other words, if an element is in the original set but is not in the set after erasing a specific element, it must be because that element is the one that was erased. More concisely: If `α` is a type with decidable equality, `s` is a finite subset of `α`, and `a, b ∈ α` with `b ∈ s` and `b ∉ s \ {a}`, then `a = b`.
`Mathlib.Data.Finset.Basic._auxLemma.111` theorem Mathlib.Data.Finset.Basic._auxLemma.111 : ∀ {a b c : Prop}, (a ∧ (b ∨ c)) = (a ∧ b ∨ a ∧ c) This theorem states that for any three propositions `a`, `b`, and `c`, the proposition "a AND (b OR c)" is logically equivalent to the proposition "(a AND b) OR (a AND c)". This is a statement of distributive law of logic, similar to the distributive law in arithmetic where `a * (b + c) = a * b + a * c`. More concisely: The propositions `a AND (b OR c)` and `(a AND b) OR (a AND c)` are logically equivalent.
`Finset.range_zero` theorem Finset.range_zero : Finset.range 0 = ∅ The theorem `Finset.range_zero` states that the set of natural numbers less than zero, represented by `Finset.range 0`, is an empty set, denoted by `∅`. This is because there are no natural numbers less than zero. More concisely: The set of natural numbers less than 0 is empty. (or) The finite set of natural numbers with start 0 and size greater than 0 is empty.
`Finset.singleton_nonempty` theorem Finset.singleton_nonempty : ∀ {α : Type u_1} (a : α), {a}.Nonempty This theorem states that for any given type `α` and an element `a` of this type, a finite set containing only `a` (written as `{a}`) is nonempty. Simply put, a singleton set (a set containing only one element) is always nonempty, regardless of the type of its element. More concisely: For any type `α` and element `a` of type `α`, the singleton set `{a}` is nonempty.
`Finset.mem_erase_of_ne_of_mem` theorem Finset.mem_erase_of_ne_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ≠ b → a ∈ s → a ∈ s.erase b This theorem states that for any given type `α` that has decidable equality, for any finite set `s` of type `α`, and for any two elements `a` and `b` of type `α`, if `a` is not equal to `b` and `a` is a member of `s`, then `a` is also a member of the set resulting from erasing `b` from `s`. In other words, if you remove an element `b` from a set `s`, any other element `a` that was in `s` and is not equal to `b` will still be in the resulting set. More concisely: If `s` is a finite set of decidably equal type `α` and `a` is an element of `s` different from `b` in `s`, then `a` is still in the set `s \ {b}`.
`Mathlib.Data.Finset.Basic._auxLemma.7` theorem Mathlib.Data.Finset.Basic._auxLemma.7 : ∀ {α : Type u_1} {s : Finset α} (x : ↑↑s), (↑x ∈ s) = True This theorem, `Mathlib.Data.Finset.Basic._auxLemma.7`, states that for any type `α` and for any finite set `s` of type `α`, any element `x` already in the double-coerced set `s` (i.e., `x` is an element of `s` when `s` is coerced twice) is indeed an element of `s`. In other words, it confirms that double-coercion does not change the membership of an element in this set. This is always true. More concisely: For any type `α` and finite set `s` of type `α`, an element `x` in `s` remains an element of `s` after double-coercion.
`Finset.nodup` theorem Finset.nodup : ∀ {α : Type u_4} (self : Finset α), self.val.Nodup The theorem `Finset.nodup` states that for any set (represented by `Finset α`) of a certain type `α`, the list of elements in the set (represented by `self.val`) contains no duplicates. In other words, every element of a `Finset` in Lean 4 is unique, which is consistent with the mathematical definition of a set. More concisely: For any set `S` represented as a `Finset α` in Lean 4, the elements in `S.val` are all distinct.
`Finset.mem_singleton_self` theorem Finset.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ {a} This theorem states that for any given type `α` and any element `a` of that type, `a` is an element of the set that only contains `a`. In other words, `a` exists in the singleton set `{a}`. This is a fundamental property of singleton sets. More concisely: For any type `α` and its element `a`, `a` belongs to the singleton set `{a}`.
`Finset.coe_inj` theorem Finset.coe_inj : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ = ↑s₂ ↔ s₁ = s₂ The theorem `Finset.coe_inj` states that for any two finite sets `s₁` and `s₂` of an arbitrary type `α`, the condition that their corresponding sets of elements (`↑s₁` and `↑s₂`) are equal is equivalent to `s₁` and `s₂` being equal. This is an injectivity property of the coercion from `Finset` to `Set` in Lean. Essentially, it means that two finite sets are the same if and only if their underlying sets of elements are the same. More concisely: The coercion from finite sets to sets is an injection, that is, two finite sets are equal if and only if their underlying sets of elements are equal.
`Mathlib.Data.Finset.Basic._auxLemma.10` theorem Mathlib.Data.Finset.Basic._auxLemma.10 : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (↑s₁ ⊆ ↑s₂) = (s₁ ⊆ s₂) := by sorry This theorem from the Mathlib library in Lean 4 states that for any two finite sets (`Finset`) `s₁` and `s₂` of any type `α`, the condition that the set `s₁` is a subset of `s₂` (expressed as `↑s₁ ⊆ ↑s₂`, where `↑` denotes the coercion of a `Finset` to a `Set`) is equivalent to the condition that `s₁` is a subset of `s₂` in the `Finset` sense (expressed as `s₁ ⊆ s₂`). Thus, the subset relation holds in the same way for finite sets whether they are considered as `Set`s or as `Finset`s. More concisely: The theorem asserts that for any two finite sets `s₁` and `s₂` of type `α`, the relation `s₁ ⊆ s₂` holding in the `Finset` sense is equivalent to `↑s₁ ⊆ ↑s₂` holding as sets, where `↑` denotes the coercion of `Finset` to `Set`.
`Finset.subset_iff` theorem Finset.subset_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂ This theorem, `Finset.subset_iff`, states that for all sets `s₁` and `s₂` of a certain type `α`, `s₁` is a subset of `s₂` if and only if for any element `x` of type `α`, if `x` is in `s₁` then `x` must also be in `s₂`. This theorem is defining the subset relationship in terms of individual element membership in the sets. More concisely: A set `s₁` is a subset of set `s₂` if and only if every element in `s₁` is also an element of `s₂`.
`Finset.Nonempty.not_disjoint` theorem Finset.Nonempty.not_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∩ t).Nonempty → ¬Disjoint s t This theorem, `Finset.Nonempty.not_disjoint`, states that for any type `α` with a decidable equality and any two finite sets `s` and `t` of type `α`, if the intersection of `s` and `t` is nonempty, then `s` and `t` are not disjoint. In other words, if there is at least one element that is in both `s` and `t`, then `s` and `t` share some common element, hence they are not disjoint. This theorem is the converse of `Finset.not_disjoint_iff_nonempty_inter`. The concept of disjointness here is generalized from the concept of disjoint sets, meaning that the greatest lower bound (infimum) of the two sets is the bottom element. More concisely: If two finite sets of a type with decidable equality have a nonempty intersection, then they are not disjoint.
`Finset.filter_inter_distrib` theorem Finset.filter_inter_distrib : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s t : Finset α), Finset.filter p (s ∩ t) = Finset.filter p s ∩ Finset.filter p t This theorem states that for any type `α`, a predicate `p` on `α` that is decidable for all elements of `α`, and two finite sets `s` and `t` of `α`, the operation of filtering the intersection of `s` and `t` by `p` (i.e., retaining only the elements of `s ∩ t` that satisfy `p`) is equivalent to the intersection of the sets obtained by filtering `s` and `t` individually by `p`. In other words, for decidable predicates and decidable equality on `α`, filtering distributes over set intersection. More concisely: For any type `α` with decidable equality and any decidable predicate `p` on `α`, the filtering of the intersection of two finite sets `s` and `t` by `p` equals the intersection of the filterings of `s` and `t` by `p`.
`Finset.ssubset_iff` theorem Finset.ssubset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t The theorem `Finset.ssubset_iff` states that for any type `α` with decidable equality and any two finite sets `s` and `t` of type `α`, `s` is a strict subset of `t` if and only if there exists an element `a` not in `s` such that adding `a` to `s` results in a set that is a subset of `t`. In other words, there's at least one element in `t` that's not in `s`, and adding it to `s` would still keep it within `t`. More concisely: For finite sets `s` and `t` of type `α` with decidable equality, `s` is a strict subset of `t` if and only if there exists an element `a` in `t` not in `s` such that `s ∪ {a} ⊆ t`.
`Finset.le_iff_subset` theorem Finset.le_iff_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ≤ s₂ ↔ s₁ ⊆ s₂ This theorem states that for any two finite sets `s₁` and `s₂` of the same type `α`, `s₁` is less than or equal to `s₂` if and only if `s₁` is a subset of `s₂`. In the context of sets, the less than or equal to relationship is defined in terms of subset inclusion. More concisely: For any finite sets `s₁` and `s₂` of type `α`, `s₁ ⊆ s₂` if and only if `s₁ ≤ s₂` (where `≤` denotes subset inclusion).
`Finset.mem_cons` theorem Finset.mem_cons : ∀ {α : Type u_1} {s : Finset α} {a b : α} {h : a ∉ s}, b ∈ Finset.cons a s h ↔ b = a ∨ b ∈ s The theorem `Finset.mem_cons` states that for any type α, any finite set `s` of type α, and any two elements `a` and `b` of type α where `a` is not in `s`, the element `b` is in the finite set resulting from consing `a` onto `s` (`Finset.cons a s h`) if and only if `b` is equal to `a` or `b` is in `s`. In other words, an element `b` is in the set created from adding `a` to `s` exactly when `b` is either equal to `a` or already in `s`. More concisely: For any type α and finite set s of type α, the element b is in the set s \cup {a}, where a is not in s, if and only if b is equal to a or is in s.
`Mathlib.Data.Finset.Basic._auxLemma.143` theorem Mathlib.Data.Finset.Basic._auxLemma.143 : ∀ {a : Prop}, (¬¬a) = a This theorem states that for any type `α` and a property `p` that can be applied to elements of type `α`, the negation of the statement "for all elements `x` of type `α`, the property `p` holds" is equivalent to the statement "there exists an element `x` of type `α` for which the property `p` does not hold". In terms of mathematical logic, this is saying that ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x). More concisely: The negation of "for all x in α, property p(x) holds" is equivalent to "there exists an x in α such that not p(x) holds".
`Mathlib.Data.Finset.Basic._auxLemma.28` theorem Mathlib.Data.Finset.Basic._auxLemma.28 : ∀ {α : Type u_1} {a b : α}, (b ∈ {a}) = (b = a) This theorem states that for any type `α` and any two elements `a` and `b` of type `α`, `b` is an element of the singleton set containing only `a` if and only if `b` is equal to `a`. In other words, in a set with only one element, the question of membership for any given element boils down to whether or not it is equal to the single member of the set. More concisely: For any type `α` and any elements `a, b` of type `α`, `b` is in the singleton set `{a}` if and only if `a = b`.
`Mathlib.Data.Finset.Basic._auxLemma.158` theorem Mathlib.Data.Finset.Basic._auxLemma.158 : ∀ {n : ℕ}, (Finset.range n = ∅) = (n = 0) This theorem in Lean 4's `Mathlib.Data.Finset.Basic._auxLemma.158` states that for any proposition `p`, the logical AND (`∧`) of `False` and `p` is always `False`. This is consistent with the standard logic rule that if one of the operands of an AND operation is false, the whole statement becomes false regardless of the other operand. More concisely: The logical AND of `False` and any proposition `p` is equal to `False`.
`Finset.empty_subset` theorem Finset.empty_subset : ∀ {α : Type u_1} (s : Finset α), ∅ ⊆ s This theorem states that for any given set `s` of an arbitrary type `α`, the empty set is a subset of `s`. In other words, no matter what set `s` you choose in any type, the empty set is always considered to be contained within `s`. This is a basic property of sets in mathematics, encapsulated in the context of finitely enumerable sets (or `Finset`s) in Lean 4. More concisely: For any set `s` of type `α`, the empty set is a subset of `s`.
`Finset.subset_singleton_iff'` theorem Finset.subset_singleton_iff' : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊆ {a} ↔ ∀ b ∈ s, b = a This theorem, `Finset.subset_singleton_iff'`, states that for any given type `α`, a finite set `s` of type `α`, and an element `a` of type `α`, the set `s` is a subset of the singleton set `{a}` if and only if every element `b` in `s` is equal to `a`. This is a universal property, meaning it holds for all possible types `α` and all finite sets `s` and elements `a` of type `α`. More concisely: A finite set `s` of type `α` is a subset of the singleton set `{a}` if and only if every element `b` in `s` equals `a`.
`Finset.subset_insert` theorem Finset.subset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s ⊆ insert a s := by sorry The theorem `Finset.subset_insert` states that for any type `α` that has decidable equality, for any element `a` of type `α`, and for any finite set `s` of elements of type `α`, the set `s` is a subset of the set that results from inserting the element `a` into `s`. In other words, it asserts that if you add an element to a set, the original set is always a subset of the new set. More concisely: For any type `α` with decidable equality, any element `a` in `α`, and any finite set `s` in `α`, `s` is a subset of `s.insert a`.
`Finset.not_mem_empty` theorem Finset.not_mem_empty : ∀ {α : Type u_1} (a : α), a ∉ ∅ This theorem states that for any type `α` and any element `a` of that type, `a` is not a member of the empty set. In other words, no element can belong to an empty set. This is a basic property of the empty set in set theory. More concisely: The theorem asserts that for all types `α` and elements `a` of type `α`, `a` is not an element of the empty set.
`Finset.forall_of_forall_cons` theorem Finset.forall_of_forall_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} {p : α → Prop} {h : a ∉ s}, (∀ x ∈ Finset.cons a s h, p x) → ∀ x ∈ s, p x This theorem states that for any type `α`, any finite set `s` of type `α`, any element `a` of type `α`, and any property `p` that elements of type `α` can have, if `a` is not in `s` and every element in the finite set obtained by adding `a` to `s` has property `p`, then every element in `s` also has property `p`. This theorem is useful in proofs by induction. More concisely: If `a` is not in finite set `s` of type `α` and every element in `s ∪ {a}` has property `p`, then every element in `s` has property `p`.
`Finset.subset_union_left` theorem Finset.subset_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ⊆ s₁ ∪ s₂ This theorem states that for any type `α` with a decidable equality and for any two finite sets `s₁` and `s₂` of type `α`, `s₁` is a subset of the union of `s₁` and `s₂`. In other words, every element of `s₁` is also an element of the union of `s₁` and `s₂`. More concisely: For any decidably equal type `α` and finite sets `s₁`, `s₂` of `α`, every element of `s₁` belongs to the union of `s₁` and `s₂`.
`Mathlib.Data.Finset.Basic._auxLemma.25` theorem Mathlib.Data.Finset.Basic._auxLemma.25 : ∀ {α : Type u_1} {s : Finset α}, (¬s.Nonempty) = (s = ∅) This theorem, `Mathlib.Data.Finset.Basic._auxLemma.25`, states that for any type `α` and any finite set `s` of type `α`, the property that `s` is not nonempty is equivalent to the property that `s` is empty. In other words, a finite set is not nonempty if and only if it is the empty set. More concisely: A finite set is nonempty if and only if it is not empty. (Equivalently, a finite set is empty if and only if it is not nonempty.)
`Finset.not_mem_erase` theorem Finset.not_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), a ∉ s.erase a This theorem states that for any type `α` with decidable equality and any element `a` of type `α`, `a` is not a member of the set obtained by erasing `a` from a given finite set `s` of `α`. In other words, once an element is removed from a finite set, it no longer belongs to that set. More concisely: For any finite set `s` of type `α` with decidable equality and any element `a` in `s`, `a` is not an element of the set `s \ {a}`.
`Mathlib.Data.Finset.Basic._auxLemma.101` theorem Mathlib.Data.Finset.Basic._auxLemma.101 : ∀ (α : Sort u), (α → True) = True This theorem, `Mathlib.Data.Finset.Basic._auxLemma.101`, states that for any type `α`, the function type from `α` to `True` is itself `True`. In other words, for any type, a function that takes an element of that type and produces `True` is always truthfully described by `True`. This is a reflection of the fact that in Lean 4, a function from any type to `True` is always true. More concisely: For any type `α`, the constant function from `α` to `True` is equal to `True`.
`Finset.union_val` theorem Finset.union_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).val = s.val ∪ t.val := by sorry The theorem `Finset.union_val` states that for any type `α` which has decidable equality, and for any two finite sets `s` and `t` of type `α`, the union of `s` and `t` (represented as `(s ∪ t).val`) is equal to the union of the values of `s` and `t` (represented as `s.val ∪ t.val`). In other words, the operation of taking the union of two finite sets in `α` corresponds exactly to the operation of taking the union of their underlying sets of values in `α`. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` in `α`, `(s ∪ t).val = s.val ∪ t.val`.
`Finset.disjoint_sdiff` theorem Finset.disjoint_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s (t \ s) This theorem states that for any given type `α` with decidable equality, and for any two finite sets `s` and `t` of this type, `s` and the set difference of `t` and `s` (i.e., `t \ s`) are disjoint. In other words, there are no elements in common between `s` and the set of elements in `t` that are not in `s`. This is a universal statement that holds for all `α`, `s`, and `t` of the specified types. In terms of lattice theory, this means that the infimum (greatest lower bound) of `s` and `t \ s` is the bottom element of the lattice, indicating that these two sets have no elements in common. More concisely: For any type `α` with decidable equality, and for any finite sets `s` and `t` of this type, `s` and `t \ s` are disjoint. (In lattice theory, the infimum of `s` and `t \ s` is the bottom element.)
`Multiset.mem_toFinset` theorem Multiset.mem_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s.toFinset ↔ a ∈ s The theorem `Multiset.mem_toFinset` states that for any type `α` with a decidable equality relation, and for any element `a` of type `α` and multiset `s` of type `α`, `a` is a member of the finset obtained by removing duplicates from `s` if and only if `a` is a member of `s`. This means that converting a multiset to a finset doesn't change the membership status of its elements. More concisely: For any type `α` with decidable equality and any multiset `s` of type `α` and element `a` of type `α`, `a` is in the finset obtained from `s` by removing duplicates if and only if `a` is in `s`.
`Mathlib.Data.Finset.Basic._auxLemma.44` theorem Mathlib.Data.Finset.Basic._auxLemma.44 : ∀ {α : Type u_1} {s : Finset α} {a b : α} {h : a ∉ s}, (b ∈ Finset.cons a s h) = (b = a ∨ b ∈ s) This theorem states that, for any given type `α`, any `Finset` `s` of `α`, and any two elements `a` and `b` of `α` such that `a` is not in `s`, then `b` belongs to the `Finset` obtained by adding `a` to `s` (denoted as `Finset.cons a s h`) if and only if `b` is either equal to `a` or `b` belongs to `s`. In other words, after adding an element `a` to `s`, a new element `b` is either in the original set `s` or it is the newly added element `a`. More concisely: For any type `α`, any `Finset` `s` of `α`, and any `a` not in `s`, `b` is in `Finset.cons a s h` if and only if `b` is in `s` or `b` equals `a`.
`Finset.union_empty` theorem Finset.union_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ ∅ = s The theorem `Finset.union_empty` states that for any type `α` that has decidable equality, and any finite set `s` of type `α`, the union of `s` and the empty set is equal to `s`. In other words, for any finite set `s`, adding nothing to `s` does not change `s`. This corresponds to the mathematical principle that the union of any set with the empty set is the set itself. More concisely: For any finite set `s` of type `α` with decidable equality, `s ∪ {} = s`.
`List.coe_toFinset` theorem List.coe_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), ↑l.toFinset = {a \| a ∈ l} The theorem `List.coe_toFinset` states that for any given type `α` that has decidable equality (`DecidableEq α`), and for any list `l` of type `α`, the conversion of `l` to a finset (`List.toFinset l`) and then applying the coercion function `↑` to this finset results in a set which contains exactly the elements that are in `l`. In other words, it establishes that the process of converting a list to a finset and then coercing it back to a set simply gives us a set of unique elements from the original list, effectively removing any duplicate elements. More concisely: For any type `α` with decidable equality and any list `l` of `α`, the set obtained by converting `l` to a finset and then coercing it back to a set equals the set of unique elements in `l`.
`Finset.val_lt_iff` theorem Finset.val_lt_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁.val < s₂.val ↔ s₁ ⊂ s₂ This theorem, `Finset.val_lt_iff`, states that for any two finite sets `s₁` and `s₂` of the same type `α`, the value of `s₁` is less than the value of `s₂` if and only if `s₁` is a proper subset of `s₂`. In other words, in Lean 4, a finite set is considered to be 'smaller' in value than another finite set only when all elements of the first set are in the second set, but the second set contains at least one element not present in the first. More concisely: For finite sets `s₁` and `s₂` of the same type `α` in Lean 4, `s₁` is less than `s₂` if and only if `s₁` is a proper subset of `s₂`.
`Finset.Subset.antisymm` theorem Finset.Subset.antisymm : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → s₂ ⊆ s₁ → s₁ = s₂ This theorem states that for any two finite sets `s₁` and `s₂` of a certain type `α`, if `s₁` is a subset of `s₂` and `s₂` is a subset of `s₁`, then `s₁` and `s₂` are equal. In mathematical terms, this is a formalization of the antisymmetry property of the subset relation in set theory. More concisely: For any sets `s₁` and `s₂` of type `α`, if `s₁ ⊆ s₂` and `s₂ ⊆ s₁`, then `s₁ = s₂`. (This is the formalization of the antisymmetric property of subset relation in set theory in Lean 4.)
`Finset.sdiff_union_of_subset` theorem Finset.sdiff_union_of_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → s₂ \ s₁ ∪ s₁ = s₂ The theorem `Finset.sdiff_union_of_subset` states that for any type `α` with decidable equality, and for any two finite sets `s₁` and `s₂` of type `α`, if `s₁` is a subset of `s₂`, then the union of the set difference `s₂ \ s₁` and `s₁` is equal to `s₂`. In mathematical terms, if $s₁$ is a subset of $s₂$, then $s₂ \ s₁ \cup s₁ = s₂$. More concisely: For any type `α` with decidable equality and finite sets `s₁` and `s₂` of type `α` with `s₁` a subset of `s₂`, we have `s₂ \ s₁ ∪ s₁ = s₂`. In mathematical notation, $s₂ \setminus s₁ \cup s₁ = s₂$.
`Mathlib.Data.Finset.Basic._auxLemma.99` theorem Mathlib.Data.Finset.Basic._auxLemma.99 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c) This theorem, named `Mathlib.Data.Finset.Basic._auxLemma.99`, asserts that for any three propositions 'a', 'b', and 'c', the conditional that 'c' follows from 'a' and 'b' being true simultaneously, is logically equivalent to the statement that if 'a' is true then 'c' follows from 'b' being true. In other words, `(a ∧ b → c)` is the same as `(a → b → c)`. More concisely: The theorem asserts that `(a ∧ b → c)` is logically equivalent to `(a → (b → c))`.
`Finset.Nonempty.coe_sort` theorem Finset.Nonempty.coe_sort : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → Nonempty { x // x ∈ s } This theorem, referred to as an alias of the reverse direction of `Finset.nonempty_coe_sort`, states that for any given type `α` and any given finite set `s` of that type, if the set `s` is nonempty, then there is a nonempty subtype consisting of elements `x` that belong to the set `s`. In other words, if a finite set is not empty, then we can always find an element in it. More concisely: If `s` is a nonempty finite set, then there exists a nonempty subtype of `α` consisting of elements in `s`.
`Finset.mem_attach` theorem Finset.mem_attach : ∀ {α : Type u_1} (s : Finset α) (x : { x // x ∈ s }), x ∈ s.attach The theorem `Finset.mem_attach` states that for any type `α` and for any finite set `s` of type `α`, every element `x` of the subtype `{ x // x ∈ s }` (which consists of elements of `s` along with a proof that they belong to `s`) is also an element of the set obtained by attaching `s` using the `Finset.attach` function. In other words, every element that is proven to belong to a certain finite set remains in that set when we form a new set via `Finset.attach`. More concisely: For any finite set `s` and all `x` in `s`, `x` is an element of the set obtained by attaching `s` using `Finset.attach`.
`Finset.eq_empty_iff_forall_not_mem` theorem Finset.eq_empty_iff_forall_not_mem : ∀ {α : Type u_1} {s : Finset α}, s = ∅ ↔ ∀ (x : α), x ∉ s This theorem states that for any set `s` of arbitrary type `α`, `s` is equal to the empty set if and only if for all elements `x` of type `α`, `x` is not a member of `s`. Essentially, a set is considered empty if it does not contain any elements. More concisely: A set `s` of type `α` is empty if and only if for all `x` of type `α`, `x ∉ s`.
`Finset.ext` theorem Finset.ext : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ The theorem `Finset.ext` states that for any two finite sets `s₁` and `s₂` of an arbitrary type `α`, if every element `a` of type `α` is in `s₁` if and only if it is in `s₂`, then `s₁` and `s₂` are equal. This theorem underlines the extensionality principle for finite sets in Lean 4, which means that two sets are identical if they contain exactly the same elements. More concisely: If two finite sets have the same elements, then they are equal.
`Finset.coe_sdiff` theorem Finset.coe_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ \ s₂) = ↑s₁ \ ↑s₂ := by sorry This theorem states that for any type `α` with decidable equality, given two finite sets `s₁` and `s₂` of type `α`, the set difference operation (represented as `\`) when applied to `s₁` and `s₂` and then coerced to a set (using `↑` operation) results in the same set as when set difference operation is applied to the coerced sets `s₁` and `s₂`. In mathematical terms, for all finite sets `s₁` and `s₂`, $↑(s₁ \ s₂) = ↑s₁ \ ↑s₂$. Here, the `↑` operation is a type coercion from `Finset` to `Set`, and `\` is the set difference operation. More concisely: For any finite sets `s₁` and `s₂` of type `α` with decidable equality, `↑(s₁ \ s₂) = ↑s₁ \ ↑s₂`. (Where `\` is set difference, `↑` is set coercion from `Finset` to `Set`, and `α` is any type with decidable equality.)
`Finset.erase_insert_eq_erase` theorem Finset.erase_insert_eq_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), (insert a s).erase a = s.erase a This theorem states that for any type `α` which has decidable equality, and for any finite set `s` and element `a` of type `α`, the operation of first inserting the element `a` into the set `s` and then removing `a` is equivalent to simply removing `a` from `s`. In mathematical terms, given a set `s` and an element `a`, the operation `erase (insert a s) a` is equal to `erase s a`. This implies that if an element is added to a set and then removed, it has no net effect on the original set. More concisely: For any finite type `α` with decidable equality, the operation of inserting and then removing an element `a` from a set `s` equals the operation of just removing `a` from `s` (i.e., `erase (insert a s) a = erase s a`).
`Finset.nonempty_iff_ne_empty` theorem Finset.nonempty_iff_ne_empty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty ↔ s ≠ ∅ This theorem, `Finset.nonempty_iff_ne_empty`, states that for any type `α` and any Finite Set `s` of type `α`, `s` is nonempty if and only if `s` is not equal to the empty set. In other words, a finite set `s` has at least one element in it if and only if it's not the case that `s` is the empty set. More concisely: A finite set is nonempty if and only if it is not equal to the empty set.
`Finset.monotone_filter_right` theorem Finset.monotone_filter_right : ∀ {α : Type u_1} (s : Finset α) ⦃p q : α → Prop⦄ [inst : DecidablePred p] [inst_1 : DecidablePred q], p ≤ q → Finset.filter p s ⊆ Finset.filter q s The theorem `Finset.monotone_filter_right` states that for any finset `s` of elements of type `α`, and any two predicates `p` and `q` on `α` such that `p` is a subset of `q` (i.e., `p ≤ q`), the filtering of `s` by `p` is a subset of the filtering of `s` by `q`. This holds under the condition that both `p` and `q` are decidable predicates, meaning that for any element in `α`, it can decisively be told whether it satisfies the predicate `p` or `q`. So, if a property defined by `p` is less restrictive than a property defined by `q`, then the set of elements in `s` satisfying `p` is a subset of the set satisfying `q`. More concisely: For any finset `s` of decidable predicates `p ≤ q` on type `α`, the filtered set `s.filter p` is a subset of `s.filter q`.
`Finset.disjoint_iff_inter_eq_empty` theorem Finset.disjoint_iff_inter_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t ↔ s ∩ t = ∅ This theorem is about finite sets (or "finsets") in a type `α` that has a decidable equality relation. It states that for any two finsets `s` and `t` in `α`, `s` and `t` are disjoint if and only if the intersection of `s` and `t` is the empty set. Here, two finsets are defined to be disjoint if their infimum (greatest lower bound) is the smallest possible element, which in this case is represented by the empty set. This theorem essentially provides a characterization of disjointness in terms of the intersection operation. More concisely: Two finsets in a type with decidable equality are disjoint if and only if their intersection is the empty set.
`Finset.inter_subset_left` theorem Finset.inter_subset_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∩ s₂ ⊆ s₁ The theorem `Finset.inter_subset_left` states that for any type `α` that has decidable equality, and for any two finite sets `s₁` and `s₂` of this type, the intersection of `s₁` and `s₂` is a subset of `s₁`. This reflects the general set theory principle that the intersection of two sets is always a subset of each of the intersecting sets. More concisely: For any type `α` with decidable equality and finite sets `s₁` and `s₂` of `α`, `s₁ ∩ s₂` is a subset of `s₁`.
`Finset.mem_inter` theorem Finset.mem_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ The theorem `Finset.mem_inter` states that for any type `α` with decidable equality, and for any element `a` of type `α` and any two finite sets `s₁` and `s₂` of type `α`, the element `a` is a member of the intersection of `s₁` and `s₂` if and only if `a` is a member of both `s₁` and `s₂`. This theorem formalizes the standard definition of set intersection in the context of finite sets. More concisely: For any type `α` with decidable equality, and for any finite sets `s₁` and `s₂` of type `α`, `a ∈ s₁ ∧ a ∈ s₂` if and only if `a ∈ s₁ ∩ s₂`.
`Finset.disjoint_filter_filter_neg` theorem Finset.disjoint_filter_filter_neg : ∀ {α : Type u_1} (s t : Finset α) (p : α → Prop) [inst : DecidablePred p] [inst_1 : (x : α) → Decidable ¬p x], Disjoint (Finset.filter p s) (Finset.filter (fun a => ¬p a) t) The theorem `Finset.disjoint_filter_filter_neg` states that for any type `α`, any finite sets `s` and `t` of `α`, and any decidable predicate `p` on `α`, the subset of `s` where `p` holds is disjoint from the subset of `t` where `p` does not hold. In other words, there is no element in `s` that both satisfies `p` and is in `t` but does not satisfy `p`. This is equivalent to saying that the intersection of these two subsets (filtered sets) is an empty set. More concisely: For any type `α`, finite sets `s` and `t` of `α`, and decidable predicate `p` on `α`, the filters `{x : α \| p x}` and `{x : α \| ¬p x}` on `α` have empty intersection.
`Finset.filter_val` theorem Finset.filter_val : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), (Finset.filter p s).val = Multiset.filter p s.val This theorem states that for any type `α`, predicate `p` (a function from `α` to a propositional logic value) which is decidable, and a finite set `s` of type `α`, the underlying value (as a multiset) of the finite set filtered by the predicate `p` is equal to the multiset obtained by filtering the underlying value of the finite set `s` by the same predicate `p`. In simpler terms, filtering a finite set and then obtaining the multiset of values is the same as first obtaining the multiset of values from the finite set and then filtering it. More concisely: For any decidable predicate `p` on type `α` and finite set `s` of type `α`, the multiset of elements in `s` satisfying `p` is equal to the multiset of elements in the filtered set `{x \| x ∈ s ∧ p x}`.
`Finset.erase_eq` theorem Finset.erase_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a = s \ {a} := by sorry This theorem states that for any given type `α` that has decidable equality and any finite set `s` of type `α` and any element `a` of type `α`, the operation of erasing `a` from `s` using `Finset.erase` is equivalent to the standard set difference operation of `s` with the singleton set `{a}`. In mathematical terms, `Finset.erase s a` is equivalent to `s \ {a}`. More concisely: For any finite type `α` with decidable equality, the operation `Finset.erase` on type `Finset α` erasing an element `a` is equal to the standard set difference `\` between the set and the singleton set `{a}`.
`Finset.Subset.refl` theorem Finset.Subset.refl : ∀ {α : Type u_1} (s : Finset α), s ⊆ s This theorem states that, for any given finite set `s` of an arbitrary type `α`, `s` is a subset of itself. This is a reflection property of subset relation in set theory, and it holds for all types and all finite sets thereof. More concisely: For any finite set `s` of type `α`, `s` is a subsets of itself.
`Finset.sdiff_subset` theorem Finset.sdiff_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ t ⊆ s The theorem `Finset.sdiff_subset` states that for any type `α` with decidable equality, and any two finite sets `s` and `t` of type `α`, the set difference `s \ t` is a subset of `s`. In other words, all elements of the set `s` minus the set `t` (notated as `s \ t`) originally belong to `s`. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, `s \ t` is a subset of `s`.
`Multiset.toFinset_val` theorem Multiset.toFinset_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.toFinset.val = s.dedup := by sorry This theorem, `Multiset.toFinset_val`, states that for all types `α` that have decidable equality and for all multisets `s` of type `α`, the underlying value (i.e., list of elements) of the finset obtained by applying the `toFinset` function to `s` is the same as the multiset obtained by applying the `dedup` function to `s`. In other words, it asserts that the process of converting a multiset to a finset effectively removes duplicates, resulting in a multiset with no duplicated elements. More concisely: For all types `α` with decidable equality and for all multisets `s` of type `α`, the `toFinset` function applied to `s` yields the same underlying list as applying `dedup` to `s`.
`Finset.nonempty_of_ne_empty` theorem Finset.nonempty_of_ne_empty : ∀ {α : Type u_1} {s : Finset α}, s ≠ ∅ → s.Nonempty This theorem states that for any type `α` and any finite set `s` of type `α`, if `s` is not equal to the empty set, then `s` is nonempty. In other words, it establishes that if a finite set is not equal to the empty set, it must contain at least one element. More concisely: For any finite non-empty set `s` of type `α`, it holds that `s` is nonempty.
`Finset.union_subset_union` theorem Finset.union_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u v : Finset α}, s ⊆ u → t ⊆ v → s ∪ t ⊆ u ∪ v The theorem `Finset.union_subset_union` states that for any type `α` with decidable equality, and any four finite sets `s`, `t`, `u`, `v` of this type, if `s` is a subset of `u` and `t` is a subset of `v`, then the union of `s` and `t` is a subset of the union of `u` and `v`. Here, the union and subset relations are taken with respect to the usual set-theoretic definitions. More concisely: For any type `α` with decidable equality, if `s` is a subset of `u` and `t` is a subset of `v`, then `s ∪ t` is a subset of `u ∪ v`.
`Finset.ssubset_insert` theorem Finset.ssubset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∉ s → s ⊂ insert a s This theorem, `Finset.ssubset_insert`, states that for any type `α` with decidable equality, given a finite set `s` of type `α` and an element `a` of type `α`, if `a` is not in `s`, then `s` is a proper subset of the set obtained by inserting `a` into `s`. In other words, adding a new, previously not present element to a finite set results in a larger set that properly contains the original one. More concisely: For any finite type `α` with decidable equality, if `a` is not in `finset α s`, then `finset.insert a s` is a strictly larger set than `s`.
`Finset.cons_val` theorem Finset.cons_val : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).val = a ::ₘ s.val The theorem `Finset.cons_val` states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α` such that `a` is not in `s`, the value of the finite set constructed by consing `a` onto `s` (i.e., adding `a` to `s` while ensuring `a` is not already in `s`) is equal to the multiset obtained by consing `a` onto the value of `s`. In other words, when you add an element to a finite set while ensuring the element is not already in the set, the underlying multiset of the resulting set is the same as if you had simply added the element to the multiset of the original set. More concisely: For any type `α`, adding an element `a` not in a finite set `s` of type `α` results in a set with the same multiset as if `a` was consed onto the multiset of `s`.
`Finset.inter_singleton_of_mem` theorem Finset.inter_singleton_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∈ s → s ∩ {a} = {a} This theorem states that for every type `α` with decidable equality, every element `a` of type `α`, and every finset `s` of type `α`, if `a` is an element of `s`, then the intersection of `s` and the singleton set containing only `a` is equal to the singleton set containing `a`. In simpler terms, if `a` is in `s`, then the only element in both `s` and `{a}` is `a` itself. More concisely: For every type `α` with decidable equality, if `a` is an element of finite set `s` of type `α`, then `s ∩ {a} = {a}`.
`Finset.Subset.rfl` theorem Finset.Subset.rfl : ∀ {α : Type u_1} {s : Finset α}, s ⊆ s The theorem `Finset.Subset.rfl` states that for any type 'α' and any finite set 's' of type 'α', 's' is a subset of itself. It is a fundamental property of set theory that every set is a subset of itself, and this theorem encodes this fact in the context of finite sets in the Lean 4 theorem prover. More concisely: Every finite set is a subset of itself.
`Finset.sdiff_empty` theorem Finset.sdiff_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, s \ ∅ = s The theorem `Finset.sdiff_empty` states that for any type `α` equipped with a decidable equality relation, and for any finite set `s` of `α`, the set difference between `s` and the empty set is `s` itself. In other words, removing nothing from a set leaves the set unchanged. This concept is often denoted in mathematics as `s \ ∅ = s`. More concisely: For any finite set `s` in a type `α` with decidable equality, `s \ EmptySet = s`.
`Mathlib.Data.Finset.Basic._auxLemma.136` theorem Mathlib.Data.Finset.Basic._auxLemma.136 : ∀ {α : Type u_1} {s : Finset α}, (s = ∅) = ∀ (x : α), x ∉ s := by sorry This theorem, `Mathlib.Data.Finset.Basic._auxLemma.136`, states that for any type `α` and any finite set `s` of type `α`, the condition that `s` is equivalent to the empty set is equivalent to the condition that for any element `x` of type `α`, `x` is not an element of `s`. In other words, a finite set is empty if and only if it does not contain any elements. More concisely: A finite set `s` of type `α` is equivalent to the empty set if and only if there does not exist an element `x` of type `α` such that `x ∈ s`.
`Finset.erase_eq_of_not_mem` theorem Finset.erase_eq_of_not_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → s.erase a = s The theorem `Finset.erase_eq_of_not_mem` states that for any type `α` that has decidable equality (meaning it's possible to determine if any two elements of the type are equal or not), if an element `a` of `α` is not in the finite set `s` (denoted by `a ∉ s`), then removing `a` from `s` (using the `Finset.erase` function) results in the same set `s`. In other words, erasing a non-member from a finite set leaves the set unchanged. More concisely: If `a` is not an element of the finite set `s`, then `Finset.erase a s = s`.
`Mathlib.Data.Finset.Basic._auxLemma.21` theorem Mathlib.Data.Finset.Basic._auxLemma.21 : ∀ {α : Type u_1}, ∅.Nonempty = False This theorem states that for any type `α`, an empty set of that type is not nonempty. In mathematical terms, a set ∅ (empty set) is not nonempty, which means it doesn't contain any elements. This holds true for any type of elements we might consider; the empty set of integers, real numbers, strings, or any other type is not nonempty. More concisely: The empty set of any type is not nonempty.
`Finset.filter_empty` theorem Finset.filter_empty : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Finset.filter p ∅ = ∅ := by sorry This theorem states that for all types `α`, and for any predicate `p` that can be decided for elements of this type, if you filter an empty finite set (`Finset`) based on this predicate, the result will be an empty finite set. In other words, there are no elements in an empty set that could satisfy any given predicate, so the filtered set remains empty. More concisely: For all types `α` and predicates `p` on `α`, the filter of the empty finite set `Finset α` using `p` is also empty.
`Finset.inter_subset_right` theorem Finset.inter_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∩ s₂ ⊆ s₂ The theorem `Finset.inter_subset_right` states that for any type `α` with a decidable equality relation, for any two finite sets (or `Finset`s) `s₁` and `s₂` of type `α`, the intersection of `s₁` and `s₂` (denoted by `s₁ ∩ s₂`) is a subset of `s₂`. This theorem asserts one of the fundamental properties of set intersection in the context of finite sets. More concisely: For any type `α` with decidable equality and for any finite sets `s₁` and `s₂` of type `α`, `s₁ ∩ s₂` is a subset of `s₂`.
`Finset.union_idempotent` theorem Finset.union_idempotent : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ s = s The theorem `Finset.union_idempotent` asserts that for any type `α` with decidable equality (denoted by `[inst : DecidableEq α]`) and for any finite set `s` of type `α` (`s : Finset α`), taking the union of `s` with itself yields `s` again. In other words, if we combine a finite set with itself, the result is just the original set. This is denoted mathematically as `s ∪ s = s`. This is an illustration of the idempotent property in the context of finite sets, stating that the union operation is idempotent. More concisely: For any finite set `s` of type `α` with decidable equality, `s ∪ s = s`.
`Finset.ne_of_mem_erase` theorem Finset.ne_of_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s.erase a → b ≠ a This theorem states that for any type `α` with decidable equality and for any `a` and `b` of type `α`, if `b` is in the set obtained by erasing `a` from a finset `s`, then `b` cannot be equal to `a`. In other words, if an element `b` is in the finset obtained by removing `a` from another finset `s`, then `b` must be different from `a`. More concisely: For any type `α` with decidable equality, and any finset `s` of type `α`, if `a` is an element of `s` and `b` is an element of the finset obtained by erasing `a` from `s`, then `a` and `b` are distinct.
`Finset.ne_empty_of_mem` theorem Finset.ne_empty_of_mem : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ s → s ≠ ∅ This theorem states that for any type `α`, given an element `a` of type `α` and a finite set `s` of elements of type `α`, if `a` is a member of `s`, then `s` cannot be an empty set. This is a fundamental property of sets, as an empty set by definition contains no elements. Therefore, the presence of at least one element is sufficient to establish that a set is not empty. More concisely: For any type `α` and finite set `s` of elements of type `α`, if `a` is an element of `s`, then `s` is non-empty.
`Finset.disjoint_coe` theorem Finset.disjoint_coe : ∀ {α : Type u_1} {s t : Finset α}, Disjoint ↑s ↑t ↔ Disjoint s t This theorem states that for any two finsets `s` and `t` of some type `α`, the property of the coerced sets `↑s` and `↑t` being disjoint is equivalent to the property of the finsets `s` and `t` themselves being disjoint. In the context of lattice theory, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element; this theorem generalizes this concept to finsets. The disjointness checks whether any element `x` that is less than or equal to both `s` and `t` must be less than or equal to the bottom element `⊥`. More concisely: For any finsets `s` and `t` of type `α` in Lean 4, `s` and `t` are disjoint if and only if their coerced sets `↑s` and `↑t` have no common element, i.e., their infimum is the bottom element.
`Finset.nonempty_cons` theorem Finset.nonempty_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).Nonempty := by sorry The theorem `Finset.nonempty_cons` states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α` that does not belong to `s`, the finite set obtained by adjoining `a` to `s` using the `Finset.cons` function is nonempty. This is naturally expected because we are adding an additional element `a` to the finite set `s`, ensuring that the resulting set has at least one element in it. More concisely: For any type `α` and finite set `s` of type `α` without element `a` of type `α`, the set `{a} ∪ s` is nonempty.
`Finset.not_disjoint_iff` theorem Finset.not_disjoint_iff : ∀ {α : Type u_1} {s t : Finset α}, ¬Disjoint s t ↔ ∃ a ∈ s, a ∈ t The theorem `Finset.not_disjoint_iff` states that for any type `α` and any two finite sets `s` and `t` of that type, the assertion that `s` and `t` are not disjoint is equivalent to the existence of an element `a` that is in both `s` and `t`. In other words, two finite sets are not disjoint if and only if there is at least one element they have in common. Here, the `Disjoint` property for two elements is defined as their greatest lower bound (infimum) being the least element of the order. More concisely: Two finite sets `s` and `t` of type `α` are not disjoint if and only if there exists an element `a` in both `s` and `t`.
`Finset.coe_erase` theorem Finset.coe_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑(s.erase a) = ↑s \ {a} := by sorry This theorem states that for any type `α` with decidable equality and any element `a` of type `α` and a finite set `s` of type `α`, the operation of erasing `a` from `s` in the context of finite sets (`Finset.erase s a`) corresponds to the set difference operation in the context of set theory (`↑s \ {a}`). In other words, erasing `a` from `s` in the context of finite sets produces a new set that contains all elements of the original set `s` except for `a`, which is what the set difference operation does. More concisely: For any finite type `α` with decidable equality and any `a : α` and finite set `s : Finset α`, `Finset.erase s a` equals the set difference `↑s \ {a}`.
`Finset.coe_inter` theorem Finset.coe_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ ∩ s₂) = ↑s₁ ∩ ↑s₂ := by sorry The theorem `Finset.coe_inter` asserts that for any given type `α` with a decidable equality and for any two finite sets (`Finset`s) `s₁` and `s₂` of that type, the intersection (`∩`) of `s₁` and `s₂` coalesces (`↑`) to the same set as the coalescence of the intersections of `s₁` and `s₂`. In other words, when two finite sets are intersected, the result is the same whether the intersection is performed before or after the sets are transformed (i.e., coalesced). More concisely: For any decidably equal types `α` and finite sets `s₁` and `s₂` of `α`, the intersection `s₁ ∩ s₂` is equal to the coalesced intersection `(↑ s₁) ∩ (↑ s₂)`.
`Finset.mem_filter` theorem Finset.mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α}, a ∈ Finset.filter p s ↔ a ∈ s ∧ p a This theorem, `Finset.mem_filter`, states that for any type `α`, any decidable predicate `p` on `α`, any finite set `s` of `α`, and any element `a` of `α`, `a` is an element of the filtered set (`Finset.filter p s`) if and only if `a` is an element of the original set `s` and `a` satisfies the predicate `p`. In other words, filtering a finite set with a predicate in Lean only keeps the elements that satisfy the predicate. More concisely: For any type `α`, finite set `s` of `α`, decidable predicate `p` on `α`, and `a` in `α`, `a` is in `Finset.filter p s` if and only if `a` is in `s` and `p(a)` holds.
`Mathlib.Data.Finset.Basic._auxLemma.166` theorem Mathlib.Data.Finset.Basic._auxLemma.166 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.toFinset.Nonempty = (s ≠ 0) This theorem, named `Mathlib.Data.Finset.Basic._auxLemma.166`, states that for any type `α` and any two multisets `s` and `t` of this type, `s` is a subset of `t` if and only if for every element `x` of type `α`, if `x` is an element of `s`, then `x` is also an element of `t`. Here, a multiset is considered as a type of finite sets where duplicates are allowed, and it is implemented as the quotient of a list by list permutation. More concisely: For any type `α`, multisets `s` and `t` of type `α`, `s ⊆ t` if and only if for all `x` in `α`, `x` in `s` implies `x` in `t`.
`Finset.coe_ssubset` theorem Finset.coe_ssubset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂ This theorem states that for all types `α` and for all finite sets `s₁` and `s₂` of this type `α`, the set `s₁` is a strict subset of set `s₂` if and only if the coercion of `s₁` to a set is a strict subset of the coercion of `s₂` to a set. In mathematical terms, it claims that the relation of a proper subset for finsets (`s₁ ⊂ s₂`) corresponds to the same relation for their set-theoretic counterparts (`↑s₁ ⊂ ↑s₂`). More concisely: For all types `α` and finite sets `s₁` and `s₂` of type `α`, `s₁ ⊂ s₂` if and only if `↑s₁ ⊂ ↑s₂`, where `↑` denotes the coercion from a finite set to a set.
`Finset.sdiff_singleton_eq_erase` theorem Finset.sdiff_singleton_eq_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s \ {a} = s.erase a The theorem `Finset.sdiff_singleton_eq_erase` states that for any given type `α` that has decidable equality (`DecidableEq α`) and for any element `a` of type `α` and set `s` of type `Finset α` (which is a finite set in Lean), the operation of set difference `s \ {a}` (which produces a set containing all elements of `s` except `a`) is the same as the operation `Finset.erase s a` (which also removes the element `a` from the set `s`). In mathematical terms, it asserts that for all `s` and `a`, `s \ {a} = Finset.erase s a`. More concisely: For any type `α` with decidable equality and for any `α` element `a` and finite set `s` of type `Finset α`, set difference `s \ {a}` equals `Finset.erase s a`.
`Finset.mem_sdiff` theorem Finset.mem_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s \ t ↔ a ∈ s ∧ a ∉ t The theorem `Finset.mem_sdiff` states that for any type `α` equipped with a decision procedure for equality (`DecidableEq α`), and any two finite sets (`s` and `t`) of that type, for all `a` of type `α`, `a` belongs to the difference of `s` and `t` (notated `s \ t`) if and only if `a` belongs to `s` and `a` does not belong to `t`. This theorem thus characterizes membership in the difference of two finite sets in Lean 4. More concisely: For any type `α` with Decidable Equality, and finite sets `s` and `t` of type `Finset α`, an element `a` belongs to `s \ t` if and only if `a` is in `s` but not in `t`.
`Finset.union_left_comm` theorem Finset.union_left_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ (t ∪ u) = t ∪ (s ∪ u) The theorem `Finset.union_left_comm` states that for any given type `α` with decidable equality and for any three finite sets `s`, `t`, and `u` of type `α`, the union operation is left-commutative. That is, the operation of taking the union of `s` with the union of `t` and `u` (`s ∪ (t ∪ u)`) is the same as taking the union of `t` with the union of `s` and `u` (`t ∪ (s ∪ u)`). In mathematical terms, we could write this as $s \cup (t \cup u) = t \cup (s \cup u)$. More concisely: For any type `α` with decidable equality, the operation of taking the union of a finite set `s` with the union of two other finite sets `t` and `u` is equal to the union of `t` with the union of `s` and `u`. In mathematical notation, `s ∪ (t ∪ u) = t ∪ (s ∪ u)`.
`Finset.union_sdiff_of_subset` theorem Finset.union_sdiff_of_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → s ∪ t \ s = t The theorem `Finset.union_sdiff_of_subset` states that for any type `α` with decidable equality, given any two finite sets `s` and `t` of type `α`, if `s` is a subset of `t`, then the union of `s` and the set difference of `t` and `s` is `t`. This can be viewed as a property of set operations where union with a set difference, under the condition that the first set is a subset of the second one, results in the original second set. More concisely: For any type `α` with decidable equality, if `s` is a subset of `finite set t` in `α`, then `s ∪ (t \ s) = t`.
`Finset.Nonempty.ne_empty` theorem Finset.Nonempty.ne_empty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s ≠ ∅ This theorem states that for any type `α` and any finite set `s` of type `α`, if `s` is nonempty (i.e., it contains at least one element), then `s` is not equal to the empty set. In mathematical terms, given a finite set `s` in an arbitrary universe `α`, if `s` contains at least one element, we can conclusively say that `s` is not the empty set. More concisely: If a finite set `s` is nonempty, then `s` is not the empty set.
`Multiset.toFinset_singleton` theorem Multiset.toFinset_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a}.toFinset = {a} This theorem states that for any type `α` with decidable equality (which means for any two elements of the type, it can be decided whether they are equal or not), and for any element `a` of type `α`, the conversion of a multiset containing only `a` to a finset (which removes any duplicates from the multiset) still results in a set containing only `a`. In other words, given a multiset with a single instance of an element, the process of removing duplicates does not change the set. More concisely: For any decidely equal type `α` and its element `a`, the conversion of the multiset {a} to a finset still contains only the element `a`.
`Finset.disjoint_filter` theorem Finset.disjoint_filter : ∀ {α : Type u_1} {s : Finset α} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q], Disjoint (Finset.filter p s) (Finset.filter q s) ↔ ∀ x ∈ s, p x → ¬q x The theorem `Finset.disjoint_filter` states that for any type `α`, any finite set `s` of type `α`, and any two predicates `p` and `q` on `α`, where both `p` and `q` are decidable properties, the set of elements in `s` satisfying `p` is disjoint from the set of elements in `s` satisfying `q` if and only if for all elements `x` in `s`, whenever `x` satisfies `p`, it does not satisfy `q`. In other words, no element in `s` can satisfy both `p` and `q` at the same time. More concisely: For any type `α`, finite set `s` of `α`, and decidable properties `p` and `q` on `α`, `s`'s subsets `{x \| p x}` and `{x \| q x}` are disjoint if and only if for all `x` in `s`, `p x` implies `~q x`.
`Finset.mem_erase` theorem Finset.mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Finset α}, a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s The theorem `Finset.mem_erase` states that for all types `α` that have a decidable equality relation, and for all objects `a`, `b` of type `α` and a finite set `s` of objects of type `α`, the object `a` is a member of the set obtained by removing `b` from `s` if and only if `a` is not equal to `b` and `a` is a member of `s`. In other words, `a` is in the finite set obtained by erasing `b` from `s` precisely when `a` is not `b` and `a` is in the original set `s`. More concisely: For any type `α` with decidable equality and finite set `s` of `α`, the element `a` belongs to the set `s \ {b} ` if and only if `a` is not equal to `b` and `a` is in `s`.
`Finset.disjoint_iff_ne` theorem Finset.disjoint_iff_ne : ∀ {α : Type u_1} {s t : Finset α}, Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b This theorem states that for any two sets `s` and `t` of any type `α`, the sets are disjoint if and only if for all elements `a` in set `s` and all elements `b` in set `t`, `a` is not equal to `b`. In other words, two sets are disjoint precisely when there is no element that belongs to both sets. Here, disjointness is defined in a general sense, without reference to a specific element-wise operation, extending the concept of disjoint sets in set theory. More concisely: Two sets of type `α` are disjoint if and only if they have no common elements.
`Mathlib.Data.Finset.Basic._auxLemma.119` theorem Mathlib.Data.Finset.Basic._auxLemma.119 : ∀ (p : Prop), (p ∨ ¬p) = True This theorem states that for any given proposition `p`, the logical disjunction of `p` or not `p` is always true. This is a restatement of the principle of excluded middle in logic, which asserts that, for any proposition, either that proposition is true or its negation is true. More concisely: For any proposition `p` in Lean, `p` or not `p` is a logically valid statement. (This is the law of the excluded middle in Lean's logic.)
`Finset.filter_congr` theorem Finset.filter_congr : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {s : Finset α}, (∀ x ∈ s, p x ↔ q x) → Finset.filter p s = Finset.filter q s The theorem `Finset.filter_congr` states that for any set `s` of elements of an arbitrary type `α`, and two predicates `p` and `q` that are decidable for every element of `α`, if for every element `x` in `s`, `x` satisfies `p` if and only if `x` satisfies `q`, then the set of elements of `s` that satisfy `p` (obtained using the `Finset.filter` function) is equal to the set of elements of `s` that satisfy `q`. In other words, if two conditions `p` and `q` are equivalent for all elements in a given set, filtering the set with either condition will result in the same set. More concisely: If `p` and `q` are equivalent predicates on a set `s`, then `Finset.filter s p` equals `Finset.filter s q`.
`Finset.Nonempty.to_set` theorem Finset.Nonempty.to_set : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → (↑s).Nonempty This theorem states that for any given set `s` of any type `α`, if the finset (a finite set in Lean 4) `s` is nonempty, i.e., it contains at least one element, then the coe (coercion) of `s` to a set is also nonempty. In other words, if a finset is not empty, then its equivalent set representation is also not empty. The theorem is an alias of the reverse direction of `Finset.coe_nonempty`. More concisely: If `s` is a nonempty finset in Lean 4, then its corresponding set representation is also nonempty.
`Finset.mem_of_mem_inter_left` theorem Finset.mem_of_mem_inter_left : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ → a ∈ s₁ The theorem `Finset.mem_of_mem_inter_left` states that for any type `α` that has decidable equality, given any elements `a` of type `α` and any two finsets `s₁` and `s₂` of elements of type `α`, if `a` is an element of the intersection of `s₁` and `s₂`, then `a` is an element of `s₁`. In other words, if an element belongs to the intersection of two sets, it must belong to each of the intersecting sets individually, specifically the first set in this case. More concisely: If `α` has decidable equality and `a` is an element of the intersection of finsets `s₁` and `s₂`, then `a` is an element of `s₁`.
`Finset.mem_mk` theorem Finset.mem_mk : ∀ {α : Type u_1} {a : α} {s : Multiset α} {nd : s.Nodup}, a ∈ { val := s, nodup := nd } ↔ a ∈ s The theorem `Finset.mem_mk` states that for all types `α`, elements `a` of type `α`, and multiset `s` of type `α` with property `Multiset.Nodup s` (i.e., `s` has no duplicate entries), the membership of `a` in the `Finset` constructed from `s` (denoted `{ val := s, nodup := nd }`) is equivalent to the membership of `a` in `s`. In other words, an element is a member of a `Finset` if and only if it is a member of the underlying multiset from which the `Finset` was created. More concisely: For any type `α`, multiset `s` of `α` with no duplicates, and element `a` of `α`, `a` is in the `Finset` constructed from `s` if and only if `a` is in `s`.
`Mathlib.Data.Finset.Basic._auxLemma.26` theorem Mathlib.Data.Finset.Basic._auxLemma.26 : ∀ {α : Type u_1} {s : Finset α}, (↑s = ∅) = (s = ∅) This theorem, `Mathlib.Data.Finset.Basic._auxLemma.26`, states that for any type `α` and any finite set `s` of that type, the condition that the coercion of `s` to a set is equivalent to an empty set is the same as saying that `s` itself is an empty set. In other words, a finite set `s` is empty if and only if its set-coerced version is also empty. This is a property of the coercion function for finite sets in Lean. More concisely: For any type α, a finite set s of type α is empty if and only if its set-coerced version is an empty set.
`Mathlib.Data.Finset.Basic._auxLemma.179` theorem Mathlib.Data.Finset.Basic._auxLemma.179 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (s.toList = [a]) = (s = {a}) This theorem, also known as `Mathlib.Data.Finset.Basic._auxLemma.179`, is stating that for any type `α`, and any elements `a` and `b` of type `α`, and a list `l` of elements of type `α`, the condition that `a` is an element of the list that starts with `b` followed by the elements of `l` is equivalent to the condition that `a` equals `b` or `a` is an element of `l`. Essentially, this theorem is expressing the basic membership property of lists in Lean 4. More concisely: For any type `α` and elements `a`, `b` of `α` and list `l` of `α`, `a` is the first element of `l` followed by the remaining elements if and only if `a` equals `b` or `a` is an element of `l`.
`Finset.coe_empty` theorem Finset.coe_empty : ∀ {α : Type u_1}, ↑∅ = ∅ This theorem states that for any type 'α', the coercion of an empty `Finset` (finite set) to a set in Lean 4 is an empty set. In other words, when we transform an empty finite set into a regular set, we still get an empty set. More concisely: For any type 'α', the coercion of an empty Finset to a set in Lean 4 is the empty set.
`Finset.coe_insert` theorem Finset.coe_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑(insert a s) = insert a ↑s This theorem, `Finset.coe_insert`, states that for any type `α` with decidable equality and for any element `a` of type `α` and set `s` of type `Finset α`, the coercion (or type conversion) of the set obtained by inserting `a` into `s` is equal to the set obtained by inserting `a` into the coerced `s`. In other words, adding an element to a finite set and then converting the type is the same as converting the type of the set and then adding the element. More concisely: For any type `α` with decidable equality, the coerced result of inserting an element `a` into a finite set `s` is equal to the result of inserting `a` into the coerced set `s`.
`Finset.forall_mem_insert` theorem Finset.forall_mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (p : α → Prop), (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x The theorem `Finset.forall_mem_insert` states that for any type `α` with decidable equality, an element `a` of type `α`, a finite set `s` of type `α`, and a property `p` that holds for elements of type `α`, the proposition that `p` holds for all elements in the set obtained by inserting `a` into `s` is equivalent to the conjunction of the propositions that `p` holds for `a` and `p` holds for all elements in `s`. In other words, for all elements in the union of `a` and `s`, property `p` holds if and only if `p` holds for `a` and for all elements in `s`. More concisely: For any decidably equal type `α`, set `s` of type `Finset α`, property `p` on `α`, and `a` in `α`, the following are equivalent: `∀ x ∈ s ∪ {a}, p x` and `p a ∧ ∀ x ∈ s, p x`.
`Finset.disjoint_singleton_left` theorem Finset.disjoint_singleton_left : ∀ {α : Type u_1} {s : Finset α} {a : α}, Disjoint {a} s ↔ a ∉ s This theorem states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, the singleton set containing `a` is disjoint with `s` if and only if `a` is not an element of `s`. In terms of lattice theory, this means that if the greatest lower bound (infimum) of `a` and any element of `s` is the bottom element, then `a` does not belong to `s`. More concisely: For any type `α`, finite set `s` of type `α`, and element `a` of type `α`, the singleton set `{a}` is disjoint from `s` if and only if `a` is not in `s`. Equivalently, `a` and every element of `s` have no common lower bound in the lattice sense.
`Finset.val_le_iff` theorem Finset.val_le_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂ This Lean theorem, `Finset.val_le_iff`, states that for all types `α` and for any two finite sets (`Finset`) `s₁` and `s₂` of this type, the multiset values (`val`) of `s₁` is less than or equal to the multiset values of `s₂` if and only if `s₁` is a subset of `s₂`. In other words, a finite set is considered less than or equal to another finite set in terms of their respective multisets if and only if the first set is contained within the second set. More concisely: For any type `α` and finite sets `s₁` and `s₂` of type `Finset α`, `s₁ ⊆ s₂` if and only if `Val s₁ ≤ Val s₂`, where `Val` denotes the multiset value function.
`Finset.range_mono` theorem Finset.range_mono : Monotone Finset.range The theorem `Finset.range_mono` states that the function `Finset.range` is monotone. In other words, if you have two natural numbers `a` and `b` such that `a ≤ b`, applying the `Finset.range` function to both numbers will yield two sets of natural numbers, and the set derived from `a` will be a subset of or equal to the set derived from `b`. The `Finset.range` function gives a set of natural numbers less than the input number, so as the input number increases, the resulting set of natural numbers can only expand or stay the same, hence the monotonicity. More concisely: For all natural numbers `a ≤ b`, `Finset.range a ≤ Finset.range b` holds in the sense of set inclusion.
`Finset.mem_coe` theorem Finset.mem_coe : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ ↑s ↔ a ∈ s This theorem states that for any type `α`, any element `a` of type `α`, and any finite set `s` of type `α`, `a` is an element of the coercion of `s` to a set if and only if `a` is an element of `s`. In other words, an element is in the finite set `s` if it is also in the set obtained by treating `s` as a set (not specifically a finite set), and vice versa. More concisely: For any type `α`, any element `a` of type `α`, and any finite set `s` of type `α`, `a` is in the set `s` if and only if `a` is in the coercion of `s` to a set.
`Finset.cons_induction` theorem Finset.cons_induction : ∀ {α : Type u_4} {p : Finset α → Prop}, p ∅ → (∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (Finset.cons a s h)) → ∀ (s : Finset α), p s This theorem expresses the principle of induction over finite sets in type theory. In more detail, it states that for any type `α` and any property `p` on finite sets of type `α`, if the property holds for the empty set and it also holds for any set when an element not already in the set is added, then the property holds for all finite sets of type `α`. More concisely: If a property holds for the empty set and is preserved under set augmentation, then it holds for all finite sets.
`Finset.coe_singleton` theorem Finset.coe_singleton : ∀ {α : Type u_1} (a : α), ↑{a} = {a} This theorem states that for all types `α` and any element `a` of type `α`, the coercion of a singleton finset containing `a` (notated as `↑{a}`) is equal to a singleton set containing `a` (`{a}`). In simpler terms, a single-element finset and a single-element set containing the same element are equivalent. More concisely: For any type `α` and element `a` of type `α`, the singleton finset `↑{a}` is equal to the singleton set `{a}`.
`Finset.induction_on'` theorem Finset.induction_on' : ∀ {α : Type u_4} {p : Finset α → Prop} [inst : DecidableEq α] (S : Finset α), p ∅ → (∀ {a : α} {s : Finset α}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)) → p S This theorem establishes an induction principle for finite sets, or `Finset`s, in Lean 4. Given a property `p` that applies to `Finset`s of a certain type `α`, if we can verify that `p` holds for the empty set, and that whenever `p` holds for any `Finset` subset of `S` it also holds for the larger `Finset` obtained by adding an element from `S` not already in the subset, then we can conclude that `p` holds for the `Finset` `S` itself. This process requires the type `α` to have decidable equality, meaning for any two elements of type `α`, we can decide whether they are equal. The induction principle can be applied to any property of `Finset`s and this principle allows mathematical reasoning about all `Finset`s by successively considering larger and larger subsets. More concisely: If `α` is a type with decidable equality, then any property `p` holding for the empty `Finset` and satisfying the monotonicity condition that `p` holds for any subset of a `Finset` `S` and any element not in that subset implies `p` holds for `S` union the element, also holds for `S` itself.
`Finset.coe_cons` theorem Finset.coe_cons : ∀ {α : Type u_1} {a : α} {s : Finset α} {h : a ∉ s}, ↑(Finset.cons a s h) = insert a ↑s := by sorry The theorem `Finset.coe_cons` states that for all types `α`, elements `a` of type `α`, and for all finite sets `s` of type `α` where `a` does not belong to `s`, the Coercion of the finite set created by the "cons" operation, which adds `a` to `s`, is equal to the set obtained by inserting `a` into the Coercion of `s`. In mathematical terms, this means that the operation of adding an element to a finite set in Lean 4 (using `Finset.cons`) is equivalent to the operation of inserting an element into the set (using `insert`) in the context of set theory. More concisely: For all types `α` and finite sets `s` of `α` not containing `a` in `α`, the coercion of `Finset.cons a s` equals the coercion of `insert a s`.
`Mathlib.Data.Finset.Basic._auxLemma.47` theorem Mathlib.Data.Finset.Basic._auxLemma.47 : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a = a' → p a) = p a' This is a theorem about properties in the context of mathematical logic and set theory. Specifically, it states that for any type `α`, and any property `p` that a member of `α` might have, and a particular member `a'` of `α`, if we know that `p` holds for any member `a` of `α` if `a` is equal to `a'`, then it is equivalent to say `p` holds specifically for `a'`. In other words, if the property is true for all elements identical to `a'`, then it is equivalent to saying the property is true for `a'`. More concisely: For any type `α` and property `p` on `α`, if for all `a` in `α`, `p(a)` if and only if `a = a'`, then `p(a')` is equivalent to `∀x ∈ α, x = a' �plies p(x)`.
`Finset.erase_injOn'` theorem Finset.erase_injOn' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Set.InjOn (fun s => s.erase a) {s \| a ∈ s} The theorem `Finset.erase_injOn'` states that for any type `α` with a decidable equality and any element `a` of type `α`, the function that erases `a` from a given finite set is injective on the set of all finite sets that contain `a`. In other words, for any two different finite sets that both contain `a`, after removing `a` from both sets, the resulting sets will also be different. More concisely: For any type `α` with decidable equality and any `a` in `α`, the function that removes `a` from a finite set is an injection on the set of all finite sets containing `a`.
`Finset.empty_union` theorem Finset.empty_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ∅ ∪ s = s This theorem, named "Finset.empty_union", states that for any type `α` that has a decidable equality and any finite set `s` of type `α`, the union of the empty set and `s` is equal to `s` itself. Essentially, this is the set theoretical concept that the union of any set with the empty set returns the original set. Thus, in mathematical terms, it can be written as `∅ ∪ s = s` for any finite set `s`. More concisely: The union of the empty set and a finite set is equal to the original set.
`Finset.mem_range_succ_iff` theorem Finset.mem_range_succ_iff : ∀ {a b : ℕ}, a ∈ Finset.range b.succ ↔ a ≤ b The theorem `Finset.mem_range_succ_iff` states that for any two natural numbers 'a' and 'b', 'a' is a member of the set of natural numbers less than or equal to 'b' (i.e., `Finset.range (Nat.succ b)`) if and only if 'a' is less than or equal to 'b'. In other words, a natural number 'a' falls within the range up to the successor of 'b' (which is equivalent to the range from zero to 'b' inclusive) if and only if 'a' does not exceed 'b'. More concisely: For any natural numbers 'a' and 'b', 'a' is in the set of natural numbers less than or equal to 'b' if and only if 'a' is less than or equal to 'b'.
`Finset.range_succ` theorem Finset.range_succ : ∀ {n : ℕ}, Finset.range n.succ = insert n (Finset.range n) This theorem states that for every natural number `n`, the set of natural numbers less than `n+1` (i.e., `Finset.range (Nat.succ n)`) is equivalent to the set obtained by inserting `n` into the set of natural numbers less than `n` (i.e., `insert n (Finset.range n)`). In other words, when you increment a number, the set of natural numbers less than the incremented number can be created by adding the original number to the set of natural numbers less than the original number. More concisely: For every natural number `n`, the set `Finset.range (Nat.succ n)` is equal to `insert n (Finset.range n)`.
`Mathlib.Data.Finset.Basic._auxLemma.9` theorem Mathlib.Data.Finset.Basic._auxLemma.9 : ∀ {α : Type u_1} (s : Finset α), (s ⊆ s) = True This theorem states that for any type `α` and any finite set `s` of that type (`Finset α`), the set `s` is a subset of itself (`s ⊆ s`). This is always true, hence the theorem asserts this statement equals `True`. This is a reflection of the fundamental property of sets in mathematics where every set is considered a subset of itself. More concisely: For any type `α` and finite set `s` of that type (`Finset α`), `s` is a subset of itself (`s ⊆ s`).
`Finset.disjoint_filter_filter'` theorem Finset.disjoint_filter_filter' : ∀ {α : Type u_1} (s t : Finset α) {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q], Disjoint p q → Disjoint (Finset.filter p s) (Finset.filter q t) This theorem states that for any two sets `s` and `t` of any type `α`, and any two decidable predicates `p` and `q`, if `p` and `q` are disjoint (meaning that their intersection is empty), then the sets obtained by filtering `s` and `t` with `p` and `q` respectively, are also disjoint. In other words, if no element of `α` satisfies both `p` and `q`, then no element of the filtered sets will either. The predicates are considered decidable, meaning that there exists a procedure to determine whether `p` or `q` is true for any given element of `α`. More concisely: If sets `s` and `t` of type `α` have disjoint decidable predicates `p` and `q`, then the filtered sets `s \| p` and `t \| q` are also disjoint.
`Finset.inter_subset_union` theorem Finset.inter_subset_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∩ t ⊆ s ∪ t This theorem states that for any type `α` with decidable equality (meaning that for any two elements `a` and `b` of `α`, whether `a = b` is a decidable proposition), and any two finite sets `s` and `t` of `α`, the intersection of `s` and `t` is a subset of the union of `s` and `t`. In mathematical terms, this can be denoted as: for all sets `s` and `t`, we have `s ∩ t ⊆ s ∪ t`. More concisely: For any types `α` with decidable equality and finite sets `s` and `t` of `α`, the intersection of `s` and `t` is a subset of the union of `s` and `t` (i.e., `s ∩ t ⊆ s ∪ t`).
`Finset.mem_insert_of_mem` theorem Finset.mem_insert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ s → a ∈ insert b s The theorem `Finset.mem_insert_of_mem` states that for any given type `α` that has decidable equality, and any `s` which is a finite set of `α`, if an element `a` belongs to `s`, then `a` also belongs to the set obtained by inserting any other element `b` into `s`. In mathematical terms, this is equivalent to saying that if `a` is an element of a set `S`, then `a` is also an element of `S ∪ {b}`, for any `b`. More concisely: If `α` has decidable equality and `a` is an element of a finite set `s` of `α`, then `a` is also an element of the set obtained by inserting any other element `b` into `s`. In mathematical notation, `a ∈ s` implies `a ∈ s ∪ {b}`.
`Finset.sup_eq_union` theorem Finset.sup_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α], Sup.sup = Union.union This theorem, `Finset.sup_eq_union`, states that for any type `α` with decidable equality (i.e., for any two elements `a` and `b` of `α`, it can be decided whether `a = b`), the operation of taking the least upper bound (`Sup.sup`) is the same as the operation of taking the union (`Union.union`). In other words, in a set with decidable equality, the least upper bound of two elements is equivalent to the union of those two elements. More concisely: For any type `α` with decidable equality, the least upper bound of two elements is equal to their set union.
`Finset.not_mem_singleton` theorem Finset.not_mem_singleton : ∀ {α : Type u_1} {a b : α}, a ∉ {b} ↔ a ≠ b This theorem states that for any type `α` and any two elements `a` and `b` of type `α`, `a` is not a member of the singleton set containing only `b` if and only if `a` is not equal to `b`. In other words, an element `a` is not in the one-element set `{b}` precisely when `a` is different from `b`. More concisely: For any type `α` and elements `a, b : α`, `a ∉ {b} ↔ a ≠ b`.
`Finset.sdiff_eq_filter` theorem Finset.sdiff_eq_filter : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ \ s₂ = Finset.filter (fun x => x ∉ s₂) s₁ The theorem `Finset.sdiff_eq_filter` states that for any types `α` that have decidable equality and any two finite sets `s₁` and `s₂` of `α`, the set difference `s₁ \ s₂` is equal to filtering `s₁` with the predicate that checks if an element does not belong to `s₂`. In other words, the operation of removing all elements of `s₂` from `s₁` (i.e., creating the set difference `s₁ \ s₂`) is equivalent to creating a new set from `s₁` that only contains elements which are not in `s₂`. More concisely: For any type `α` with decidable equality and finite sets `s₁` and `s₂` of `α`, `s₁ \ s₂` equals the filter of `s₁` through the predicate `λ x, x ∉ s₂`.
`Multiset.toFinset_zero` theorem Multiset.toFinset_zero : ∀ {α : Type u_1} [inst : DecidableEq α], Multiset.toFinset 0 = ∅ The theorem `Multiset.toFinset_zero` states that for any type `α` that has decidable equality (meaning, we can definitively determine whether any two elements of type `α` are equal or not), the operation of transforming an empty multiset (denoted by `0`) into a finset (a set with no duplicates) results in an empty finset (denoted by `∅`). In other words, the finset version of an empty multiset is also empty, regardless of the type of its elements. More concisely: The theorem asserts that the conversion of an empty multiset to a finset results in the empty finset, for types with decidable equality.
`Finset.coe_injective` theorem Finset.coe_injective : ∀ {α : Type u_4}, Function.Injective Finset.toSet The theorem `Finset.coe_injective` states that for every type `α`, the function `Finset.toSet` is injective. In other words, given any two finite sets (finsets) of elements of type `α`, if their corresponding sets (obtained by the `Finset.toSet` function) are identical, then the original finite sets must also be identical. This means that no two distinct finite sets can map to the same set under the `Finset.toSet` function. More concisely: For any type `α`, the function `Finset.toSet` from `Finset α` to `Set α` is an injection.
`Mathlib.Data.Finset.Basic._auxLemma.3` theorem Mathlib.Data.Finset.Basic._auxLemma.3 : ∀ {α : Type u_1} {a : α} {s : Multiset α} {nd : s.Nodup}, (a ∈ { val := s, nodup := nd }) = (a ∈ s) This theorem states that for any type `α`, any element `a` of this type, and any multiset `s` of type `α` which has no duplicates (represented by `Multiset.Nodup s`), the condition for `a` being an element of the set `{ val := s, nodup := nd }` is equivalent to `a` being an element of the multiset `s` itself. Simply put, it means `a` is an element of a set derived from `s` if and only if `a` is an element of `s`. This set is defined as a multiset `s` with a proof `nd` that it has no duplicates. More concisely: For any type `α`, any element `a` of type `α`, and any multiset `s` of type `α` without duplicates, `a` belongs to the multiset `s` if and only if `a` is an element of the set `{val := s, nodup := ⊤}`.
`Finset.filter_false_of_mem` theorem Finset.filter_false_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (∀ x ∈ s, ¬p x) → Finset.filter p s = ∅ This theorem states that if all elements of a finite set `s` of type `α` fail to satisfy a certain predicate `p`, then the result of filtering `s` with `p` produces an empty set. Here, `p` is a decidable predicate, which means that for any element of `s`, it is decidable whether this element satisfies `p` or not. In other words, if no element of a finite set meets the condition specified by the predicate, filtering the set based on this condition results in an empty set. More concisely: If `s` is a finite set of type `α` and `p` is a decidable predicate such that no element of `s` satisfies `p`, then `Filter.filter p s` equals the empty set.
`Finset.mem_insert` theorem Finset.mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ s The theorem `Finset.mem_insert` states that for any type `α` with decidable equality (as denoted by `[inst : DecidableEq α]`), and for any finite set `s` of type `α` and any elements `a` and `b` of type `α`, the condition "`a` is an element of the finite set obtained by inserting `b` into `s`" is equivalent to the logical disjunction "`a` equals `b` or `a` is an element of `s`". In other words, `a` is in the set formed by adding `b` to `s` if and only if `a` is either `b` or already in `s`. More concisely: For any finite set `s` of type `α` with decidable equality, and any `a, b` in `α`, `a ∈ s.insert b` if and only if `a = b` or `a ∈ s`.
`Finset.insert_subset_iff` theorem Finset.insert_subset_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t The theorem `Finset.insert_subset_iff` states that for any given type `α`, where `α` has a decidable equality relation, and for any given finite sets `s` and `t` of type `α`, along with an element `a` of type `α`, the insertion of `a` into `s` is a subset of `t` if and only if `a` is an element of `t` and `s` is a subset of `t`. In other words, it says that the action of inserting an element into a set and then testing for subset inclusion is equivalent to checking if the element is in the target set and the original set is a subset of the target set. More concisely: For any type `α` with decidable equality and finite sets `s`, `t` of `α` and element `a` of `α`, `a ∈ t` and `s ⊆ t` are equivalent.
`Mathlib.Data.Finset.Basic._auxLemma.118` theorem Mathlib.Data.Finset.Basic._auxLemma.118 : ∀ {a b c : Prop}, (a ∧ b ∨ a ∧ c) = (a ∧ (b ∨ c)) This theorem, `Mathlib.Data.Finset.Basic._auxLemma.118`, states that for any three propositions `a`, `b`, and `c`, the relation `(a ∧ b ∨ a ∧ c) = (a ∧ (b ∨ c))` holds true. This theorem illustrates a property of logical operations where the conjunction (`∧`, logical "and") of a proposition `a` with either `b` or `c` (denoted by `b ∨ c`, logical "or") is equivalent to the disjunction (`∨`) of the conjunction of `a` with `b` and `a` with `c` (`a ∧ b ∨ a ∧ c`). Essentially, it showcases the distributive law of logic. More concisely: The theorem `Mathlib.Data.Finset.Basic._auxLemma.118` in Lean 4 states that `(a ∧ (b ∨ c)) = (a ∧ b ∨ a ∧ c)` for any propositions `a`, `b`, and `c`, which expresses the distributive property of logical conjunction over logical disjunction.
`Finset.nodup_toList` theorem Finset.nodup_toList : ∀ {α : Type u_1} (s : Finset α), s.toList.Nodup The theorem `Finset.nodup_toList` states that for any type `α` and any finite set `s` of that type, the list produced from the finite set `s` using the `Finset.toList` function contains no duplicates. In other words, any element appears at most once in the list. This is expressed in Lean 4 using the `List.Nodup` property. More concisely: For any type `α` and finite set `s` of that type, the list `Finset.toList s` has no repeated elements.
`Finset.union_assoc` theorem Finset.union_assoc : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ s₃ : Finset α), s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) The theorem `Finset.union_assoc` states that for any type `α` that has decidable equality, and any three finite sets (`s₁`, `s₂`, `s₃`) of type `α`, the union operation (`∪`) is associative. In other words, taking the union of `s₁` and `s₂` first, and then taking the union with `s₃`, is the same as taking the union of `s₂` and `s₃` first, and then taking the union with `s₁`. In terms of set theory, this theorem states that $(s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)$. More concisely: For any type `α` with decidable equality and any finite sets `s₁`, `s₂`, `s₃` of type `α`, `(s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)`.
`Finset.coe_filter` theorem Finset.coe_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), ↑(Finset.filter p s) = {x \| x ∈ s ∧ p x} The theorem `Finset.coe_filter` states for any type `α`, decidable predicate `p`, and finite set `s` of type `α`, the co-domain of the function `Finset.filter p s` is equal to the set of elements `x` such that `x` belongs to `s` and the predicate `p` is true for `x`. In other words, it's saying that filtering a finite set `s` with a predicate `p` yields a set containing only those elements of `s` which satisfy the predicate `p`. More concisely: For any type `α`, decidable predicate `p`, and finite set `s` of type `α`, the set of elements in `s` that satisfy `p` is equal to the co-domain of `Finset.filter p s`.
`Mathlib.Data.Finset.Basic._auxLemma.30` theorem Mathlib.Data.Finset.Basic._auxLemma.30 : ∀ {α : Type u_1} {a b : α}, ({a} = {b}) = (a = b) This theorem, from the `Mathlib.Data.Finset.Basic` library, states that for any type `α` and any two elements `a` and `b` of type `α`, the singleton set containing `a` equals the singleton set containing `b` if and only if `a` equals `b`. In mathematical terms, for all `α`, `a`, and `b`, `{a} = {b}` is equivalent to `a = b`. More concisely: For any type `α` and any elements `a` and `b` of type `α`, the singleton sets `{a}` and `{b}` are equal if and only if `a` and `b` are equal.
`Finset.induction_on` theorem Finset.induction_on : ∀ {α : Type u_4} {p : Finset α → Prop} [inst : DecidableEq α] (s : Finset α), p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) → p s The theorem `Finset.induction_on` states that to establish a property `p` about an arbitrary finite set `s` of type `α`, it is sufficient to demonstrate two things: (1) the property `p` holds for the empty set, and (2) for any element `a` of type `α` and any finite set `s` of type `α` where `a` is not in `s`, if the property `p` holds for `s`, then it also holds for the finite set obtained by inserting `a` into `s`. This theorem assumes that equality between elements of type `α` is decidable. More concisely: The theorem `Finset.induction_on` states that for any property `p` on finite sets `s` of type `α`, if `p` holds for the empty set and `p` holds for any `a` not in `s` and the set obtained by inserting `a` into `s`, then `p` holds for all finite sets `s` of type `α`. (Assumes decidable equality on `α`.)
`Finset.eq_empty_or_nonempty` theorem Finset.eq_empty_or_nonempty : ∀ {α : Type u_1} (s : Finset α), s = ∅ ∨ s.Nonempty This theorem states that for any given finite set `s` of any type `α`, `s` is either equal to the empty set or is nonempty. In other words, any finite set must be one of two cases: it contains no elements at all (it is the empty set), or it has at least one element (it is nonempty). More concisely: Every finite set is either empty or nonempty.
`Finset.disjoint_singleton_right` theorem Finset.disjoint_singleton_right : ∀ {α : Type u_1} {s : Finset α} {a : α}, Disjoint s {a} ↔ a ∉ s The theorem `Finset.disjoint_singleton_right` states that for any set `s` of elements of a certain type `α` and any single element `a` of the same type, `s` and `{a}` are disjoint (in the sense that their greatest lower bound, or infimum, is the least element in the order) if and only if `a` is not an element of `s`. In other words, the singleton set `{a}` is disjoint from the set `s` precisely when `a` does not belong to `s`. More concisely: The theorem `Finset.disjoint_right_singleton` asserts that for any set `s` of type `α` and element `a` of type `α`, the singleton set `{a}` is disjoint from `s` if and only if `a` is not in `s`.
`Finset.mem_union_right` theorem Finset.mem_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t The theorem `Finset.mem_union_right` asserts that for any type `α` which has decidable equality and for any element `a` of this type and any finite set `t` of this type, if `a` is an element of `t`, then `a` is also an element of the union of `t` and any other finite set `s` of this type. In mathematical terms, this is expressing that if $a \in t$, then $a \in s \cup t$ for all finite sets $s$, $t$ of a type `α` with decidable equality. More concisely: For any type `α` with decidable equality and any finite sets `t` and `s` of `α`, if `a` is an element of `t`, then `a` is an element of `s ∪ t`.
`Finset.filter_congr_decidable` theorem Finset.filter_congr_decidable : ∀ {α : Type u_1} (s : Finset α) (p : α → Prop) (h : DecidablePred p) [inst : DecidablePred p], Finset.filter p s = Finset.filter p s This theorem states that for any given set `s` of type `Finset α`, and any predicate `p` which is a decidable property on elements of type `α`, the filtered subset of `s` where elements satisfy the predicate `p` remains the same regardless of the decidable instance being used. In other words, the specific decidable instance, which is used to determine whether each element satisfies `p`, does not affect the outcome of the `Finset.filter` operation. This ensures consistency in the filtered results even when multiple decidable instances for the same predicate are present. More concisely: For any decidable predicate `p` on type `α` and finite set `s` of type `Finset α`, the filtered subsets `{x : s \| p x}` are equal for all decidable instances of `p`.
`Finset.coe_toList` theorem Finset.coe_toList : ∀ {α : Type u_1} (s : Finset α), ↑s.toList = s.val The theorem `Finset.coe_toList` states that for any finite set `s` of an arbitrary type `α`, the list obtained by converting the finite set `s` to a list using the function `Finset.toList`, and then converting this list back to a finite set, will be equal to the original finite set `s`. In other words, the process of converting from a finite set to a list and back is a lossless operation. More concisely: For any finite set `s` of type `α`, the conversion of `s` to a list using `Finset.toList` and back to a finite set using `Finset.ofList` results in the original set `s`. In other words, `Finset.ofList (Finset.toList s) = s`.

LeanAide GPT-4 documentation

Module: Mathlib.Data.Finset.Basic

Finset.mem_singleton

theorem Finset.mem_singleton : ∀ {α : Type u_1} {a b : α}, b ∈ {a} ↔ b = a

Finset.eq_empty_of_forall_not_mem

theorem Finset.eq_empty_of_forall_not_mem : ∀ {α : Type u_1} {s : Finset α}, (∀ (x : α), x ∉ s) → s = ∅

Finset.cons_induction_on

theorem Finset.cons_induction_on : ∀ {α : Type u_4} {p : Finset α → Prop} (s : Finset α), p ∅ → (∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (Finset.cons a s h)) → p s

Finset.filter_subset

theorem Finset.filter_subset : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), Finset.filter p s ⊆ s

Finset.val_eq_zero

theorem Finset.val_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.val = 0 ↔ s = ∅

Finset.eq_empty_of_isEmpty

theorem Finset.eq_empty_of_isEmpty : ∀ {α : Type u_1} [inst : IsEmpty α] (s : Finset α), s = ∅

Mathlib.Data.Finset.Basic._auxLemma.74

theorem Mathlib.Data.Finset.Basic._auxLemma.74 : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ ⊆ s₂) = ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂

Finset.Nonempty.bex

theorem Finset.Nonempty.bex : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∃ x, x ∈ s

Finset.insert_nonempty

theorem Finset.insert_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).Nonempty

Finset.ext_iff

theorem Finset.ext_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂

Finset.forall_mem_cons

theorem Finset.forall_mem_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop), (∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x

Finset.coe_subset

theorem Finset.coe_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂

Finset.subset_singleton_iff

theorem Finset.subset_singleton_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊆ {a} ↔ s = ∅ ∨ s = {a}

Mathlib.Data.Finset.Basic._auxLemma.95

theorem Mathlib.Data.Finset.Basic._auxLemma.95 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = ((a ∧ c) ∧ b)

Finset.erase_insert

theorem Finset.erase_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).erase a = s

Finset.self_mem_range_succ

theorem Finset.self_mem_range_succ : ∀ (n : ℕ), n ∈ Finset.range (n + 1)

Finset.insert_val_of_not_mem

theorem Finset.insert_val_of_not_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).val = a ::ₘ s.val

Finset.eq_singleton_iff_unique_mem

theorem Finset.eq_singleton_iff_unique_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Mathlib.Data.Finset.Basic._auxLemma.19

theorem Mathlib.Data.Finset.Basic._auxLemma.19 : (¬False) = True

Finset.insert_eq_of_mem

theorem Finset.insert_eq_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a s = s

Finset.induction

theorem Finset.induction : ∀ {α : Type u_4} {p : Finset α → Prop} [inst : DecidableEq α], p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) → ∀ (s : Finset α), p s

Mathlib.Data.Finset.Basic._auxLemma.80

theorem Mathlib.Data.Finset.Basic._auxLemma.80 : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, (a ∈ s ∪ t) = (a ∈ s ∨ a ∈ t)

Finset.singleton_injective

theorem Finset.singleton_injective : ∀ {α : Type u_1}, Function.Injective singleton

Mathlib.Data.Finset.Basic._auxLemma.2

theorem Mathlib.Data.Finset.Basic._auxLemma.2 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ s.val) = (a ∈ s) := by sorry

Mathlib.Data.Finset.Basic._auxLemma.39

theorem Mathlib.Data.Finset.Basic._auxLemma.39 : ∀ {α : Type u_1} {s : Finset α} {a : α}, ({a} ⊆ s) = (a ∈ s) := by sorry

Finset.disjoint_val

theorem Finset.disjoint_val : ∀ {α : Type u_1} {s t : Finset α}, s.val.Disjoint t.val ↔ Disjoint s t

Finset.cons_eq_insert

theorem Finset.cons_eq_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s), Finset.cons a s h = insert a s := by sorry

Finset.insert_erase_invOn

theorem Finset.insert_erase_invOn : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, Set.InvOn (insert a) (fun s => s.erase a) {s | a ∈ s} {s | a ∉ s}

Finset.insert_empty

theorem Finset.insert_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, insert a ∅ = {a}

Finset.Nonempty.cons_induction

theorem Finset.Nonempty.cons_induction : ∀ {α : Type u_4} {p : (s : Finset α) → s.Nonempty → Prop}, (∀ (a : α), p {a} ⋯) → (∀ ⦃a : α⦄ (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯) → ∀ {s : Finset α} (hs : s.Nonempty), p s hs

Finset.filter_true_of_mem

theorem Finset.filter_true_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (∀ x ∈ s, p x) → Finset.filter p s = s

Finset.mem_cons_self

theorem Finset.mem_cons_self : ∀ {α : Type u_1} (a : α) (s : Finset α) {h : a ∉ s}, a ∈ Finset.cons a s h

List.toFinset_cons

theorem List.toFinset_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, (a :: l).toFinset = insert a l.toFinset

Finset.subset_empty

theorem Finset.subset_empty : ∀ {α : Type u_1} {s : Finset α}, s ⊆ ∅ ↔ s = ∅

Mathlib.Data.Finset.Basic._auxLemma.51

theorem Mathlib.Data.Finset.Basic._auxLemma.51 : ∀ {α : Type u_1} {s t : Finset α}, Disjoint s t = ∀ ⦃a : α⦄, a ∈ s → a ∉ t

Mathlib.Data.Finset.Basic._auxLemma.174

theorem Mathlib.Data.Finset.Basic._auxLemma.174 : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.Nonempty = (l ≠ [])

Finset.union_comm

theorem Finset.union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∪ s₂ = s₂ ∪ s₁

Mathlib.Data.Finset.Basic._auxLemma.23

theorem Mathlib.Data.Finset.Basic._auxLemma.23 : ∀ {α : Type u_1} {s : Finset α}, (s.val = 0) = (s = ∅)

Finset.filter_eq

theorem Finset.filter_eq : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), Finset.filter (Eq b) s = if b ∈ s then {b} else ∅

`Finset.mem_singleton`

`Finset.eq_empty_of_forall_not_mem`

`Finset.cons_induction_on`

`Finset.filter_subset`

`Finset.val_eq_zero`

`Finset.eq_empty_of_isEmpty`

`Mathlib.Data.Finset.Basic._auxLemma.74`

`Finset.Nonempty.bex`

`Finset.insert_nonempty`

`Finset.ext_iff`

`Finset.forall_mem_cons`

`Finset.coe_subset`

`Finset.subset_singleton_iff`

`Mathlib.Data.Finset.Basic._auxLemma.95`

`Finset.erase_insert`

`Finset.self_mem_range_succ`

`Finset.insert_val_of_not_mem`

`Finset.eq_singleton_iff_unique_mem`

`Mathlib.Data.Finset.Basic._auxLemma.19`

`Finset.insert_eq_of_mem`

`Finset.induction`

`Mathlib.Data.Finset.Basic._auxLemma.80`

`Finset.singleton_injective`

`Mathlib.Data.Finset.Basic._auxLemma.2`

`Mathlib.Data.Finset.Basic._auxLemma.39`

`Finset.disjoint_val`

`Finset.cons_eq_insert`

`Finset.insert_erase_invOn`

`Finset.insert_empty`

`Finset.Nonempty.cons_induction`

`Finset.filter_true_of_mem`

`Finset.mem_cons_self`

`List.toFinset_cons`

`Finset.subset_empty`

`Mathlib.Data.Finset.Basic._auxLemma.51`

`Mathlib.Data.Finset.Basic._auxLemma.174`

`Finset.union_comm`

`Mathlib.Data.Finset.Basic._auxLemma.23`

`Finset.filter_eq`

`Finset.union_sdiff_self_eq_union`

`Finset.filter_insert`

`Finset.inter_eq_right`

`Finset.not_nonempty_iff_eq_empty`

`Finset.forall_of_forall_insert`

`Finset.filter_or`

`Finset.disjUnion_eq_union`

`Finset.inter_eq_left`

`Finset.Nonempty.empty_ssubset`

`Finset.erase_subset`

`Mathlib.Data.Finset.Basic._auxLemma.64`

`Mathlib.Data.Finset.Basic._auxLemma.45`

`Finset.filter_eq'`

`Finset.Nonempty.mono`

`Finset.mem_union`

`Finset.filter_eq_empty_iff`

`Finset.coe_eq_singleton`

`Finset.mem_insert_self`

`Finset.empty_val`

`Finset.disjoint_erase_comm`

`Finset.Nonempty.attach`

`Finset.not_mem_mono`

`Mathlib.Data.Finset.Basic._auxLemma.144`

`Finset.sdiff_eq_empty_iff_subset`

`Mathlib.Data.Finset.Basic._auxLemma.6`

`Finset.singleton_subset_iff`

`Finset.filter_mem_eq_inter`

`Finset.mem_def`

`Mathlib.Data.Finset.Basic._auxLemma.32`

`Finset.range_one`

`Finset.coe_union`

`Finset.disjoint_sdiff_inter`

`Finset.inter_subset_inter`

`Finset.insert_erase`

`Mathlib.Data.Finset.Basic._auxLemma.46`