Finset.coe_nsmul
theorem Finset.coe_nsmul :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α) (n : ℕ), ↑(n • s) = n • ↑s
This theorem states that for any type `α` with decidable equality and an additive monoid structure, for any finite set `s` of `α` and any natural number `n`, the coerced result of applying the scalar multiplication `n • s` is the same as the result of applying the scalar multiplication to the coerced set `n • ↑s`. In other words, we can either first perform the scalar multiplication on the set and then coerce it to a different type, or first coerce the set and then perform the scalar multiplication, and the result will be the same.
More concisely: For any decidably equated type `α` with an additive monoid structure, coerced scalar multiplication `n • ↑s` equals `↑(n • s)` for any finite set `s` of `α` and natural number `n`.
|
Finset.zero_mem_zero
theorem Finset.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0
This theorem states that for any type `α` that has a zero element, the zero element is a member of the zero finset. Here, `0 ∈ 0` is a shorthand way of saying that the zero element of the type `α` is in the set that consists only of the zero element of `α`. This is a basic property of any type that has a zero element.
More concisely: For any type `α` with a zero element, the zero element belongs to the zero finset. In mathematical notation, `0 ∈ 0 : Finset α`.
|
Mathlib.Data.Finset.Pointwise._auxLemma.82
theorem Mathlib.Data.Finset.Pointwise._auxLemma.82 :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β} {x : β},
(x ∈ s • t) = ∃ y ∈ s, ∃ z ∈ t, y • z = x
The theorem `Mathlib.Data.Finset.Pointwise._auxLemma.82` states that for any types `α` and `β`, given that `β` has decidable equality and there is a scalar multiplication operation defined between `α` and `β`, for any finite sets `s` of type `α` and `t` of type `β`, and any element `x` of type `β`, the condition of `x` being in the scalar multiplication of `s` and `t` is equivalent to the existence of elements `y` in `s` and `z` in `t` such that the scalar multiplication of `y` and `z` equals `x`.
More concisely: For any types `α` and `β` with decidable equality, and given a scalar multiplication operation between `α` and `β`, the element `x` lies in the scalar multiplication of finite sets `s` of type `α` and `t` of type `β` if and only if there exist `y ∈ s` and `z ∈ t` such that `y * z = x`.
|
Finset.mem_add
theorem Finset.mem_add :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {x : α},
x ∈ s + t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
This theorem, `Finset.mem_add`, states that for any type `α` that has decidable equality and an addition operation, along with any two finite sets `s` and `t` of this type, and any element `x` of the same type, `x` is in the sum of `s` and `t` if and only if there exists an element `y` in `s` and an element `z` in `t` such that `y + z = x`. In other words, an element is in the sum of two finite sets if and only if it can be expressed as the sum of an element from each set.
More concisely: For any type `α` with decidable equality and addition, and finite sets `s` and `t` of `α`, an element `x` is in the sum `s ∪ {t}` if and only if there exist `y ∈ s` and `z ∈ t` such that `y + z = x`.
|
Finset.coe_inv
theorem Finset.coe_inv :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α), ↑s⁻¹ = (↑s)⁻¹
The theorem `Finset.coe_inv` states that for any type `α` that has decidable equality (i.e., for any two elements `a` and `b` of `α`, it is decidable whether `a = b`) and an involutive inverse operation (i.e., an operation where applying the operation twice to any value returns the original value), and for any finite set `s` of `α`, the inverse of the coersion of `s` is equal to the coersion of the inverse of `s`. In other words, taking the inverse before or after coersion yields the same result.
More concisely: For any type `α` with decidable equality and an involutive inverse operation, the coercion of the inverse of a finite set is equal to the inverse of the coercion of the set.
|
Finset.vadd_finset_inter
theorem Finset.vadd_finset_inter :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β]
{s t : Finset β} {a : α}, a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
The theorem `Finset.vadd_finset_inter` states that for any types `α` and `β`, assuming `β` has decidable equality and `α` forms an additive group that acts on `β`, for any finsets `s` and `t` of type `β` and any element `a` of type `α`, the intersection of the translated finset `a +ᵥ s` with `t` is the same as the intersection of the translated finsets `a +ᵥ s` and `a +ᵥ t`. Here, `a +ᵥ s` denotes the translation (vector addition) of the finset `s` by the element `a`.
More concisely: For any additive group `α` acting on a type `β` with decidable equality, and any finsets `s`, `t` of type `β` and element `a` of type `α`, the intersection of translated finsets `a + s` and `t` equals the intersection of translated finsets `a + s` and `a + t`.
|
Finset.subset_div
theorem Finset.subset_div :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {u : Finset α} {s t : Set α},
↑u ⊆ s / t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t'
This theorem states that for any given type `α` with decidable equality and a division operation, if a finite set `u` is a subset of the division of two sets `s` and `t`, then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the division of `s'` and `t'`.
More concisely: Given two sets `s` and `t` with decidable equality and a division operation, if `u` is a finite subset of the division of `s` and `t`, then there exist finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the division of `s'` and `t'`.
|
Finset.zero_smul_finset
theorem Finset.zero_smul_finset :
∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
[inst_3 : DecidableEq β] {s : Finset β}, s.Nonempty → 0 • s = 0
The theorem `Finset.zero_smul_finset` states that for any nonempty finite set `s` of elements of type `β`, where `β` is a type equipped with a zero element and an operation of scalar multiplication by elements of type `α` (which also has a zero element), if equality within `β` is decidable, then the set `s` scaled by zero is equal to the singleton set containing just the zero element. In other words, the multiplication of any nonempty set by zero results in a set containing only the zero element.
More concisely: For any nonempty finite set `s` over a type `β` with decidable equality and scalar multiplication by zero, `s * 0 = {0}`.
|
Finset.card_dvd_card_smul_right
theorem Finset.card_dvd_card_smul_right :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {t : Finset β}
{s : Finset α}, ((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card
The theorem `Finset.card_dvd_card_smul_right` asserts that for any two types `α` and `β`, given a decidable equality on `β`, a group structure on `α`, and a multiplication action of `α` on `β`, if the left cosets of a finite set `t` of type `β` by elements of a finite set `s` of type `α` are pairwise disjoint (meaning that any two distinct cosets have no elements in common, although they may not be distinct), then the size (cardinality) of `t` divides the size of the set obtained by multiplying `s` and `t` (denoted as `s • t`). In other words, the number of elements in `t` is a divisor of the number of elements in the set formed by the group action of `s` on `t`.
More concisely: If `β` has a decidable equality and `α` is a group with a multiplication action on `β`, and the left cosets of a finite set `t` by elements of a finite set `s` are pairwise disjoint, then the cardinality of `t` divides the cardinality of `s • t`.
|
Finset.coe_vadd
theorem Finset.coe_vadd :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (s : Finset α) (t : Finset β),
↑(s +ᵥ t) = ↑s +ᵥ ↑t
The theorem `Finset.coe_vadd` states that for any types `α` and `β`, given `α` has a vector addition operation and `β` has a decidable equality, for any finite sets `s` of type `α` and `t` of type `β`, the operation of lifting `s` to the type `β` and then adding `t` (notated `↑(s +ᵥ t)`) is the same as first lifting `s` and `t` to the type `β` and then adding them (notated `↑s +ᵥ ↑t`). This theorem essentially guarantees the compatibility of the vector addition operation with the type-lifting operation in the context of finite sets.
More concisely: For any types `α` with vector addition and decidable equality `β`, the operation of lifting a finite set `s` of type `α` to type `β` and then performing vector addition with another finite set `t` of type `β` is equivalent to first lifting `s` and `t` separately and then performing vector addition.
|
Finset.coe_mul
theorem Finset.coe_mul :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α), ↑(s * t) = ↑s * ↑t
This theorem, named `Finset.coe_mul`, states that for any type `α` which has decidable equality and a multiplication operation, given two finite sets `s` and `t` of type `α`, the set of all products of elements from `s` and `t` (expressed as `s * t`) is equal to the Cartesian product of `s` and `t` (expressed as `↑s * ↑t`). Here `↑s` and `↑t` represent the conversion (coercion) of the finsets `s` and `t` to sets of `α`. In other words, the theorem shows that multiplication of two finite sets is equivalent to the Cartesian product of the sets when the sets are considered as sets of a type with multiplication.
More concisely: For any type `α` with decidable equality and multiplication, the finite sets `s` and `t` of `α` have equal elements when regarded as sets, i.e., `s * t` (the set of products) is equivalent to `↑s * ↑t` (the Cartesian product).
|
Mathlib.Data.Finset.Pointwise._auxLemma.15
theorem Mathlib.Data.Finset.Pointwise._auxLemma.15 :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] {s : Finset α} {a : α}, (a ∈ s⁻¹) = (a⁻¹ ∈ s)
This theorem, `Mathlib.Data.Finset.Pointwise._auxLemma.15`, holds for any type `α` with decidable equality and an involution as its inverse operation. Given a `Finset` (finite set) `s` of elements from `α` and an element `a` from `α`, the theorem states that `a` being an element of the inverse of `s` is equivalent to the inverse of `a` being an element of `s`. In mathematical terms, for any set `s` and an element `a`, we have $a \in s^{-1} \Leftrightarrow a^{-1} \in s$.
More concisely: For any type `α` with decidable equality and an involution as its inverse operation, the inverse of an element is in a finite set `s` if and only if the element is in the inverse of `s`. In other words, $a \in s^{-1} \Leftrightarrow a^{-1} \in s$.
|
Finset.image_zero
theorem Finset.image_zero :
∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : DecidableEq β] {f : α → β}, Finset.image f 0 = {f 0} := by
sorry
This theorem states that, for any types `α` and `β`, if `α` has a zero element and `β` has decidable equality, then the image of the zero element under any function `f` from `α` to `β` is a finite set containing only the image of the zero element. In other words, if we apply `f` to the zero element of `α` and consider it as a finite set, we get a singleton set consisting of `f(0)`.
More concisely: Given types `α` with a zero element and decidable equality `β`, for any function `f` from `α` to `β`, the image of the zero element under `f` is a singleton set containing `f(0)`.
|
Finset.coe_sub
theorem Finset.coe_sub :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] (s t : Finset α), ↑(s - t) = ↑s - ↑t
The theorem `Finset.coe_sub` states that for any type `α` with decidable equality and a subtraction operation, and for any two finsets `s` and `t` over `α`, the operation of subtracting `t` from `s` (denoted as `s - t`) in the context of finsets and then converting the result to a set (using the operation `↑`) is the same as first converting `s` and `t` to sets and then performing the set subtraction operation. In other words, the order of subtraction and conversion to set does not matter.
More concisely: For any type `α` with decidable equality and subtraction operation, the conversion of `(s - t)` to a set in the context of finsets is equal to the set difference between the sets `(↑s)` and `(↑t)`, for any finsets `s` and `t` over `α`.
|
Finset.coe_smul
theorem Finset.coe_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (s : Finset α) (t : Finset β),
↑(s • t) = ↑s • ↑t
The theorem `Finset.coe_smul` states that for any two finite sets `s` and `t` of types `α` and `β` respectively, where `β` has a decidable equality and there exists a scalar multiplication operation on `α` and `β`, the result of the scalar multiplication of the two sets `s` and `t` when coerced (or converted) to a set is equal to the scalar multiplication of the coerced sets `s` and `t`. In simpler terms, the theorem states that the process of scalar multiplication is consistent under the operation of set coercion.
More concisely: For finite sets $s:\alpha$ and $t:\beta$ with decidable equality and scalar multiplication operations, $(s\cdot c)\cup t = s\cdot (c\cdot t)$, where $\cdot$ denotes scalar multiplication and coercion.
|
Finset.subset_smul
theorem Finset.subset_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {u : Finset β} {s : Set α} {t : Set β},
↑u ⊆ s • t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t'
This theorem states that for any given finite set `u` of type `β`, and two sets `s` of type `α` and `t` of type `β`, if `u` is contained in the scalar product of `s` and `t` (notated as `s • t`), then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the scalar product of `s'` and `t'` (notated as `s' • t'`). This theorem requires a decidable equality on `β` and a scalar multiplication operation defined between `α` and `β`.
More concisely: For any finite sets `u` of type `β`, `s` of type `α`, and `t` of type `β` with a decidable equality and scalar multiplication, if `u` is contained in the scalar product of `s` and `t` (`u ⊆ s • t`), then there exist subsets `s'` of `s` and `t'` of `t` such that `u ⊆ s' • t'`.
|
Mathlib.Data.Finset.Pointwise._auxLemma.6
theorem Mathlib.Data.Finset.Pointwise._auxLemma.6 :
∀ {α : Type u_2} [inst : Zero α] {s : Finset α}, (0 ⊆ s) = (0 ∈ s)
This theorem, titled `Mathlib.Data.Finset.Pointwise._auxLemma.6`, states that for any type `α` that has a `Zero` instance, and for any finite set `s` of type `α`, the condition that the zero element is a subset of `s` is equivalent to the zero element being an element of `s`. The subset notation here is being used to denote that all elements of the singleton set containing zero are also elements of `s`.
More concisely: For any type `α` with a `Zero` instance and any finite set `s` of type `α`, the zero element belongs to `s` if and only if the zero element is a subset of `s`.
|
Finset.subset_add
theorem Finset.subset_add :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {u : Finset α} {s t : Set α},
↑u ⊆ s + t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' + t'
The theorem `Finset.subset_add` asserts that for any type `α` with decidable equality and an addition operation, given a finite set `u` and two other sets `s` and `t`, if `u` is contained within the sum set of `s` and `t` (denoted as `s + t`), then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the sum set of `s'` and `t'`. Here, the notation `⊆` represents subset relation and the `+` operation on sets represents the Minkowski sum.
More concisely: Given a type `α` with decidable equality and an addition operation, if a finite set `u` is contained in the Minkowski sum of finite sets `s` and `t`, then there exist finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is contained in the sum of `s'` and `t'`.
|
Mathlib.Data.Finset.Pointwise._auxLemma.16
theorem Mathlib.Data.Finset.Pointwise._auxLemma.16 :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] {s : Finset α} {a : α}, (a ∈ -s) = (-a ∈ s) := by
sorry
This theorem, `Mathlib.Data.Finset.Pointwise._auxLemma.16`, states that for any type `α` with decidable equality and involutive negation, and for any finite set `s` of type `α` and any element `a` of type `α`, the element `a` belongs to the negation of the set `s` if and only if the negation of `a` belongs to the set `s`. Here, "involutive negation" means that negating any element twice returns the original element; in mathematical notation, for any `a` in `α`, `-(-a) = a`.
More concisely: For any type `α` with decidable equality and involutive negation, the element `a` is in the complement of a finite set `s` of type `α` if and only if the negation of `a` is in `s`.
|
Finset.coe_neg
theorem Finset.coe_neg :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s : Finset α), ↑(-s) = -↑s
The theorem `Finset.coe_neg` states that for any given type `α`, under the conditions that `α` has decidable equality (represented by `DecidableEq α`) and `α` has an involutive negation operation (represented by `InvolutiveNeg α`), for any given finite set `s` of type `α` (represented by `s : Finset α`), the coercion of the negation of `s` is equal to the negation of the coercion of `s`. In other words, negating each element in the set and then taking the whole set as a unit is the same as first taking the set as a unit and then negating it.
More concisely: For any type `α` with decidable equality and an involutive negation operation, the negation of a finite set `s` of type `α` is equal to the set of negations of its elements.
|
Finset.card_smul_finset
theorem Finset.card_smul_finset :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] (a : α)
(s : Finset β), (a • s).card = s.card
This theorem, `Finset.card_smul_finset`, states that for any type `α` that is a group, any type `β` that has a multiplication action by `α`, and any element `a` of `α`, the cardinality (size) of the set obtained by scaling a finite set `s` of `β` by `a` is the same as the cardinality of `s` itself. This assumes that equality for elements of `β` is decidable, which means we can always determine whether two elements of `β` are equal or not. The scaling of the set `s` is defined by the group action of `α` on `β`.
More concisely: For any group `α`, any type `β` with a left action by `α`, and decidably equated `β`, the cardinality of the scaled finite set `{a * x | x ∈ s}` is equal to that of `s`, where `s` is a finite subset of `β` and `a` is an element of `α`.
|
Finset.subset_vsub
theorem Finset.subset_vsub :
∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {u : Finset α} {s t : Set β},
↑u ⊆ s -ᵥ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t'
This theorem states that if a finite set `u` is a subset of the pointwise subtraction of two sets `s` and `t` (denoted as `s -ᵥ t`), then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the pointwise subtraction of `s'` and `t'` (denoted as `s' -ᵥ t'`). This statement is valid for any types `α` and `β` where `α` has a subtractive structure (`VSub`) and decidable equality (`DecidableEq`), and `s` and `t` are sets of elements of type `β`.
More concisely: Given finite sets `u ⊆ s -ᵥ t` in type `β` with `α` having subtractive structure and decidable equality, there exist `s' ⊆ s` and `t' ⊆ t` such that `u ⊆ s' -ᵥ t'`.
|
Mathlib.Data.Finset.Pointwise._auxLemma.2
theorem Mathlib.Data.Finset.Pointwise._auxLemma.2 : ∀ {α : Type u_2} [inst : Zero α] {a : α}, (a ∈ 0) = (a = 0) := by
sorry
This theorem, `Mathlib.Data.Finset.Pointwise._auxLemma.2`, states that for any type `α` equipped with a zero element, any element `a` of type `α` is in the zero set if and only if `a` is equal to zero. The zero set in this context is the set that contains only the zero element.
More concisely: For any type `α` with a zero element, an element `a` lies in the zero set if and only if `a` equals the zero element.
|
Finset.Nonempty.of_inv
theorem Finset.Nonempty.of_inv :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹.Nonempty → s.Nonempty
This theorem, referred to as `Finset.Nonempty.of_inv`, states that for every type `α` with decidable equality and an operation of inversion, if the inverse of a finite set `s` of type `α` is nonempty, then `s` itself is also nonempty.
More concisely: If `s` is a finite nonempty set in a type `α` with decidable equality and an operation of inversion, then its inverse is nonempty. Thus, `s` itself is nonempty.
|
Mathlib.Data.Finset.Pointwise._auxLemma.54
theorem Mathlib.Data.Finset.Pointwise._auxLemma.54 :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {x : α},
(x ∈ s * t) = ∃ y ∈ s, ∃ z ∈ t, y * z = x
The theorem `Mathlib.Data.Finset.Pointwise._auxLemma.54` states that, for any type `α` where equality is decidable and multiplication operation is defined, and given two finite sets `s` and `t` of type `α`, and an element `x` of type `α`, the condition that `x` is in the set product of `s` and `t` is equivalent to there existing an element `y` in `s` and an element `z` in `t` such that the product of `y` and `z` equals `x`. In other words, `x` is in the set product of `s` and `t` if and only if there are elements in `s` and `t` whose multiplication gives `x`.
More concisely: For finite sets $s$ and $t$ of type $\alpha$ where equality is decidable and multiplication is defined, $x$ belongs to the set product $s \times t$ if and only if there exist $y \in s$ and $z \in t$ such that $y \cdot z = x$.
|
Finset.mem_mul
theorem Finset.mem_mul :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {x : α},
x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
The theorem `Finset.mem_mul` states that for any type `α` that has decidable equality and a multiplication operation, for any two finite sets `s` and `t` of type `α`, and any element `x` of type `α`, `x` belongs to the product of `s` and `t` if and only if there exists an element `y` in `s` and an element `z` in `t` such that the product of `y` and `z` equals `x`. In other words, the theorem describes the distributive property of multiplication over finite sets.
More concisely: For any type `α` with decidable equality and multiplication, and finite sets `s` and `t` of type `α`, an element `x` lies in the product of `s` and `t` if and only if there exist elements `y` in `s` and `z` in `t` such that `x = y * z`.
|
Finset.card_dvd_card_add_right
theorem Finset.card_dvd_card_add_right :
∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s + t).card
This theorem states that for any type `α` that forms an additive group and has a decidable equality, given two finite sets `s` and `t` of this type, if the left cosets of `t` by the elements of `s` are pairwise disjoint (which means no two of them share an element), then the size (cardinality) of `t` divides the size of the union of `s` and `t`. Here, a left coset of `t` by an element `x` of `s` is the set of all elements of the form `x + y` where `y` is in `t`. The theorem provides a connection between the structure of an additive group and the cardinalities of particular finite sets in the group.
More concisely: If `α` is an additive group with decidable equality and `s` and `t` are finite, disjoint sets in `α`, then the cardinality of `t` divides the cardinality of `s ∪ t`.
|
Finset.subset_mul
theorem Finset.subset_mul :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {u : Finset α} {s t : Set α},
↑u ⊆ s * t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'
This theorem states that for any type `α` that has a multiplication operation and where equality is decidable, given a finite set `u` and two sets `s` and `t`, if `u` is a subset of the product set of `s` and `t`, then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is a subset of the product set of `s'` and `t'`.
More concisely: Given a type `α` with decidable equality and a finite subset `u` of the product set `s × t` of two sets `s` and `t`, there exist finite subsets `s'` of `s` and `t'` of `t` such that `u` is a subset of `s' × t'`.
|
Finset.coe_zero
theorem Finset.coe_zero : ∀ {α : Type u_2} [inst : Zero α], ↑0 = 0
This theorem states that for any type `α` that has an instance of `0`, the coercion of `0` (in the context of a finite set `Finset`) to `α` is `0`. In other words, the set-representation `0` (a set with no elements) is equivalent to the numeric `0` in this context.
More concisely: For any type `α` with an instance of `0`, the coercion of `Finset.zero` to `α` equals `α.zero`.
|
Finset.card_dvd_card_vadd_right
theorem Finset.card_dvd_card_vadd_right :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {t : Finset β}
{s : Finset α}, ((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s +ᵥ t).card
The theorem `Finset.card_dvd_card_vadd_right` states that for any types `α` and `β`, given a decidable equality for the type `β`, an addition group structure on `α`, and an addition action of `α` on `β`, if the left cosets of a finite set `t` of type `β` by elements of a finite set `s` of type `α` are pairwise disjoint, then the cardinality of `t` divides the cardinality of the set resulting from the addition of `s` and `t`. In this context, `x +ᵥ t` denotes the left coset of `t` by `x`, and `s +ᵥ t` is the union of all such cosets for `x` in `s`.
More concisely: If `β` has decidable equality, `α` has an additive group structure, and `s` and `t` are finite sets of types `α` and `β`, respectively, such that the left cosets of `t` by elements of `s` are pairwise disjoint, then the cardinality of `t` divides the cardinality of `s +ᵥ t`.
|
Finset.card_dvd_card_mul_left
theorem Finset.card_dvd_card_mul_left :
∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
((fun b => Finset.image (fun a => a * b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s * t).card
This theorem states that for any two finite sets `s` and `t` of elements of a group `α` with decidable equality, if the right cosets of `s` by elements of `t` are pairwise disjoint (i.e., each pair of different right cosets has no elements in common), then the cardinality (or size) of `s` divides the cardinality of the product set `s * t`. Here, the "right coset" of `s` by an element `b` of `t` is the set of all products `a * b` where `a` is an element of `s`, and the product set `s * t` is the set of all products `a * b` where `a` is in `s` and `b` is in `t`.
More concisely: If two finite sets of elements in a group have pairwise disjoint right cosets, then the cardinality of their product is a multiple of the cardinality of one set.
|
Finset.image_one
theorem Finset.image_one :
∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : DecidableEq β] {f : α → β}, Finset.image f 1 = {f 1} := by
sorry
This theorem, named 'Finset.image_one', states that for any types `α` and `β`, given that `α` has a defined "one" element (denoted by the typeclass `One α`) and `β` has decidable equality (indicated by `DecidableEq β`), for any function `f` from `α` to `β`, the image of the singleton finset containing only the "one" element of `α` under `f` is the singleton finset containing `f` applied to the "one" element of `α`. In other words, if we apply `f` to each element in the singleton set containing only the "one" element in `α`, we get a new set containing only the result `f 1`.
More concisely: For functions between types with defined "one" elements and decidable equality, the image of the singleton set containing the "one" element under the function is the singleton set containing the image of the "one" element.
|
Finset.smul_mem_smul_finset_iff
theorem Finset.smul_mem_smul_finset_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s : Finset β}
{b : β} (a : α), a • b ∈ a • s ↔ b ∈ s
The theorem `Finset.smul_mem_smul_finset_iff` states that for any type `α` with an underlying group structure, and any type `β` with a multiplication action by `α`, given any finite set `s` of elements of type `β`, and any elements `a` of type `α` and `b` of type `β`, then `a • b` is an element of the set resulting from scaling each element of `s` by `a` if and only if `b` is an element of `s`. The equality on type `β` is assumed to be decidable. In other words, the scaling action of an element from a group `α` doesn't change the membership of an element in a finite set.
More concisely: For any type `α` with a group structure, any type `β` with a left action by `α`, and a finite set `s` of elements in `β`, an element `a` in `α`, and an element `b` in `β`, `a • b` is in the scaled set `{a * x | x ∈ s}` if and only if `b` is in `s`.
|
Finset.card_dvd_card_add_left
theorem Finset.card_dvd_card_add_left :
∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
((fun b => Finset.image (fun a => a + b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s + t).card
This theorem states that for any two finite sets `s` and `t` in an additive group `α` with decidable equality, if the right cosets of `s` by elements of `t` are pairwise disjoint (i.e., each pair of these cosets has an empty intersection), then the cardinality (size) of `s` divides the cardinality of the sum-set of `s` and `t`. Here, the right coset of `s` by `b` is defined as the set of all elements of the form `a + b` for `a` in `s`, and the sum-set of `s` and `t` includes all elements of the form `a + b` for `a` in `s` and `b` in `t`.
More concisely: If `s` and `t` are finite subsets of an additive group with decidable equality, and the right cosets of `s` by elements of `t` are pairwise disjoint, then the cardinality of `s` divides the cardinality of `s + t`.
|
Finset.coe_smul_finset
theorem Finset.coe_smul_finset :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α) (s : Finset β),
↑(a • s) = a • ↑s
The theorem `Finset.coe_smul_finset` states that for any types `α` and `β`, given that `β` has a decidable equality and that `α` can be multiplied with `β` (i.e., `α` is a scalar and `β` is a space that allows scalar multiplication), for any scalar `a` of type `α` and any finite set `s` of type `β`, the scalar multiplication of `a` and `s` (denoted as `a • s`) coerced to a set is equal to the scalar multiplication of `a` and the coerced set `s` (denoted as `a • ↑s`). In other words, scalar multiplication distributes over the coercion of a finite set to a set.
More concisely: For any scalar `α` and finite set `β`, if `β` has decidable equality and `α` can be multiplied with `β`, then `a • s` equals `a • ↑s` for any scalar `a` of type `α` and finite set `s` of type `β`.
|
Finset.coe_vadd_finset
theorem Finset.coe_vadd_finset :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α) (s : Finset β),
↑(a +ᵥ s) = a +ᵥ ↑s
The theorem `Finset.coe_vadd_finset` states that for any given types `α` and `β`, provided that `β` has a decidable equality and `α` and `β` together form a vector addition structure (`VAdd α β`), for any given element `a` of type `α` and a finite set `s` of elements of type `β`, the set obtained by vector-adding `a` to each element of `s` and then converting to a set (`↑(a +ᵥ s)`) is the same as the set obtained by first converting `s` to a set and then vector-adding `a` to each element (`a +ᵥ ↑s`). In mathematical terms, this is saying that the vector addition operation commutes with the operation of converting a finite set to a set.
More concisely: For any type `α` and `β` with decidable equality and a vector addition structure `VAdd α β`, the operation of converting a finite set `s` of type `β` to a set and then vector-adding an element `a` of type `α`, `a +ᵥ ↑s`, is equal to vector-adding `a` to each element of `s` and then converting the resulting finite set to a set, `↑(a +ᵥ s)`.
|
Finset.card_vadd_finset
theorem Finset.card_vadd_finset :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] (a : α)
(s : Finset β), (a +ᵥ s).card = s.card
This theorem, `Finset.card_vadd_finset`, states that for any type `α` which is an additive group, and any type `β` which is a set on which `α` acts additively, and for which equality is decidable, the cardinality of the set that results from vector addition of an element `a` of `α` with all elements of a finite set `s` of `β` is the same as the cardinality of the original set `s`. In other words, adding a group element to every member of a finite set does not change the size of the set.
More concisely: For any additive group `α`, set `β` on which `α` acts additively with decidable equality, and finite set `s` in `β`, the cardinality of `s` is equal to the cardinality of `{a + b | a ∈ s, b ∈ β}`, where `+` denotes vector addition.
|
Finset.subset_sub
theorem Finset.subset_sub :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {u : Finset α} {s t : Set α},
↑u ⊆ s - t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' - t'
This theorem states that for any type `α` with decidable equality and a subtraction operation, given a finite set `u`, and two sets `s` and `t` of the same type, if `u` is a subset of the difference of `s` and `t` (denoted by `s - t`), then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t` and `u` is a subset of the difference of `s'` and `t'` (denoted by `s' - t'`).
More concisely: Given a type `α` with decidable equality and subtraction, if `u` is a subset of the difference `s - t` for finite sets `s` and `t` of type `α`, then there exist finite sets `s'` and `t'` such that `u` is a subset of `s' - t'`, `s'` is a subset of `s`, and `t'` is a subset of `t`.
|
Finset.coe_one
theorem Finset.coe_one : ∀ {α : Type u_2} [inst : One α], ↑1 = 1
This theorem states that for any type `α` that has an instance of the `One` typeclass, the coercion of `1` to a `Finset` (finite set) equals `1`. This essentially means that, in the context of finite sets, a single element set with the element as `1` is equivalent to `1`.
More concisely: For any type `α` with an instance of Lean's `One` typeclass, the coercion of `1` to a `Finset α` is equal to the singleton set `{1 : α}`.
|
Mathlib.Data.Finset.Pointwise._auxLemma.53
theorem Mathlib.Data.Finset.Pointwise._auxLemma.53 :
∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ ⊆ s₂) = ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂
This theorem, labeled as `Mathlib.Data.Finset.Pointwise._auxLemma.53`, states that for any type `α`, and any two finite sets `s₁` and `s₂` of this type, `s₁` is a subset of `s₂` if and only if for all elements `x` of type `α`, whenever `x` is in `s₁`, it is also in `s₂`. In other words, all elements of the first set are also elements of the second set.
More concisely: For any type `α` and finite sets `s₁` and `s₂` of type `Finset α`, `s₁ ⊆ s₂` if and only if `∀ x ∈ s₁, x ∈ s₂`.
|
Finset.subset_vadd
theorem Finset.subset_vadd :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {u : Finset β} {s : Set α} {t : Set β},
↑u ⊆ s +ᵥ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' +ᵥ t'
The theorem `Finset.subset_vadd` states that for any two types `α` and `β`, given a `DecidableEq` instance for `β` and a `VAdd` instance for `α` and `β` (which allows for vector addition of `α` and `β`), if you have a finite set `u` of elements of type `β` and two sets `s` and `t` of types `α` and `β` respectively, such that `u` is contained in the vector addition of `s` and `t`, then there exist two finite sets `s'` and `t'` such that `s'` is a subset of `s`, `t'` is a subset of `t`, and `u` is contained in the vector addition of `s'` and `t'`.
In other words, if a finite set is contained in the scalar sum of two sets, we can always find two sub-finite sets of the original sets whose scalar sum still contains the initial finite set.
More concisely: Given finite sets `s` and `t` of types `α` and `β` respectively, if a finite subset `u` of `β` is contained in the vector sum `s + t`, then there exist subsets `s'` of `s` and `t'` of `t` such that `u` is contained in `s' + t'`.
|
Finset.coe_div
theorem Finset.coe_div :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] (s t : Finset α), ↑(s / t) = ↑s / ↑t
This theorem, `Finset.coe_div`, states that for any type `α` that has decidable equality and a division operation, for any two finite sets `s` and `t` of type `α`, the operation of dividing the co-domain of `s` by the co-domain of `t` is the same as the co-domain of the result of dividing `s` by `t`. In other words, division distributes over the co-domain operation for finite sets in this context.
More concisely: For any type `α` with decidable equality and division operation, the co-domain of `s / t` equals the co-domain of `s` divided by the co-domain of `t` for finite sets `s` and `t` of type `α`.
|
Finset.Nonempty.inv
theorem Finset.Nonempty.inv :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s.Nonempty → s⁻¹.Nonempty
This theorem, referred to as the "Alias of the reverse direction of `Finset.inv_nonempty_iff`", establishes that for any type `α` equipped with a decidable equality relation and an inversion operation, if a finite set `s` of type `α` is nonempty, then the set consisting of the inverses of the elements in `s`, denoted as `s⁻¹`, is also nonempty.
More concisely: If `α` is a type with decidable equality and inversion operations, then a nonempty finite set `s` of `α` has a nonempty inverse set `s⁻¹`.
|
Finset.smul_finset_inter
theorem Finset.smul_finset_inter :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
{a : α}, a • (s ∩ t) = a • s ∩ a • t
This theorem, `Finset.smul_finset_inter`, states that for any types `α` and `β`, given that `β` has a decidable equality, `α` forms a group and there's a multiplication action from `α` to `β`. If `s` and `t` are finite sets of type `β` and `a` is an element of type `α`, then the operation of scaling the intersection of `s` and `t` by `a` is equal to the intersection of individually scaling `s` and `t` by `a`. This is analogous to the distributive property of multiplication over intersection in set theory.
More concisely: For any type `α` forming a group with decidable equality, and a multiplication action from `α` to type `β`, if `s` and `t` are finite sets of type `β`, then scaling the intersection of `s` and `t` by an element `a` in `α` is equal to the intersection of individually scaling `s` and `t` by `a`.
|
Finset.card_dvd_card_mul_right
theorem Finset.card_dvd_card_mul_right :
∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s * t).card
This theorem states that for any type `α` that forms a group and has decidable equality, given two finite sets `s` and `t` of this type, if the left cosets of `t` by elements of `s` are pairwise disjoint, then the cardinality (size) of `t` divides the cardinality of the product `s * t`.
In other words, in the context of group theory, if we form all the left cosets of set `t` by multiplying it with elements from set `s` and none of these cosets intersect, then the number of elements in `t` is a divisor of the number of elements in the set formed by the product of `s` and `t`.
More concisely: If `α` is a group with decidable equality and `s` and `t` are finite subsets of `α` such that the left cosets of `t` by elements of `s` are pairwise disjoint, then the cardinality of `t` divides the cardinality of `s × t`.
|
Finset.card_inv
theorem Finset.card_inv :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α), s⁻¹.card = s.card
The theorem `Finset.card_inv` states that for any given type `α` which has decidable equality and an involution operation (meaning applying the operation twice will return the original value), the cardinality (i.e., the number of elements) of the inverse `s⁻¹` of a finite set `s` of type `α` is equal to the cardinality of `s` itself. This means that applying the inverse operation to all elements of the set doesn't change the number of distinct elements in the set.
More concisely: For any finite set `s` of type `α` with decidable equality and an involution operation, the cardinality of `s` is equal to the cardinality of its inverse.
|
Finset.coe_pow
theorem Finset.coe_pow :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α) (n : ℕ), ↑(s ^ n) = ↑s ^ n
The theorem `Finset.coe_pow` states that for any type `α` that has decidable equality and a monoid structure, any finset `s` of type `α`, and any natural number `n`, lifting `s` to the power of `n` (using the monoid operation for finsets) and then taking the "set" corresponding to the resultant finset is the same as first taking the "set" corresponding to `s` and then taking it to the power of `n` (using the monoid operation for sets). In other words, the operations of taking power and "set" corresponding to a finset commute.
More concisely: For any type `α` with decidable equality and a monoid structure, the operation of taking the power of a finset `s` in the monoid of finsets and then taking the underlying set is equal to taking the underlying set of `s` and then raising it to the power in the monoid of sets.
|
Finset.coe_add
theorem Finset.coe_add :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α), ↑(s + t) = ↑s + ↑t
The theorem `Finset.coe_add` states that for any type `α` with decidable equality and an addition operation, and for any two finite sets `s` and `t` of type `α`, the set formed by adding each pair of elements, one from `s` and one from `t` (`s + t`), is equal to the set obtained by adding the sets `s` and `t` themselves (`↑s + ↑t`). In other words, the operation of summing the sets commutes with the operation of taking the sum of pairs. This is expressed in the context of "coercions" where `↑s` denotes the coercion (conversion) of the finite set `s` to a set.
More concisely: For any type `α` with decidable equality and addition operation, the sum of finite sets `s` and `t` as sets (`↑s + ↑t`) is equal to the set of pairs `(x, y)` with `x ∈ s` and `y ∈ t` (`s + t`).
|
Mathlib.Data.Finset.Pointwise._auxLemma.60
theorem Mathlib.Data.Finset.Pointwise._auxLemma.60 :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α} {a : α},
(a ∈ s / t) = ∃ b ∈ s, ∃ c ∈ t, b / c = a
This theorem, `Mathlib.Data.Finset.Pointwise._auxLemma.60`, states that for any type `α` that has decidable equality and a division operation, for any two finite sets `s` and `t` of elements of `α`, and for any element `a` in `α`, the condition of `a` being in the set resulting from dividing every element of `s` by every element of `t` is equivalent to the existence of an element `b` in `s` and an element `c` in `t` such that `b / c` equals `a`.
More concisely: For any type `α` with decidable equality and division, the element `a` is in the set of quotients of every element in finite sets `s` and `t` if and only if there exist `b` in `s` and `c` in `t` such that `b / c = a`.
|
Finset.mem_zero
theorem Finset.mem_zero : ∀ {α : Type u_2} [inst : Zero α] {a : α}, a ∈ 0 ↔ a = 0
This theorem states that for any type `α` that has a zero element (indicated by `[inst : Zero α]`), an element `a` of type `α` is a member of the zero set if and only if `a` is equal to zero. In mathematical terms, for any type `α` with a zero, `a ∈ 0` is equivalent to `a = 0`.
More concisely: For any type `α` with a zero element, `a` is an element of the zero set if and only if `a` equals the zero element itself.
|