Finset.filter_product
theorem Finset.filter_product :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : α → Prop) (q : β → Prop) [inst : DecidablePred p]
[inst_1 : DecidablePred q],
Finset.filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) = Finset.filter p s ×ˢ Finset.filter q t
The theorem `Finset.filter_product` states that for every pair of finite sets `s` and `t` over arbitrary types `α` and `β` respectively, and for any pair of decidable predicates `p` on `α` and `q` on `β`, filtering the Cartesian product `s ×ˢ t` by the conjunction of `p` and `q` (i.e., selecting those pairs `(x, y)` for which `p(x)` and `q(y)` both hold) is equivalent to forming the Cartesian product of `s` filtered by `p` and `t` filtered by `q`. In other words, it asserts that the filtering operation distributes over the Cartesian product of finite sets.
More concisely: For finite sets $s$ and $t$ over types $\alpha$ and $\beta$ respectively, and decidable predicates $p$ on $\alpha$ and $q$ on $\beta$, the sets of pairs $(x, y)$ in $s \times t$ satisfying $p(x) \land q(y)$ and $(x, y) \in (s \times p) \times (t \times q)$ are equal.
|
Finset.Nonempty.product
theorem Finset.Nonempty.product :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty := by
sorry
This theorem states that for any two non-empty sets `s` and `t` of any types `α` and `β` respectively, the product set `s ×ˢ t` is also non-empty. In other words, if we have at least one element in each of the two sets, then there will be at least one ordered pair in the product set created by combining `s` and `t`.
More concisely: For any non-empty sets `s` of type `α` and `t` of type `β`, the product set `s ×ˢ t` is non-empty.
|
Finset.product_subset_product
theorem Finset.product_subset_product :
∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β}, s ⊆ s' → t ⊆ t' → s ×ˢ t ⊆ s' ×ˢ t'
This theorem states that for any two types `α` and `β`, and any four finite sets `s`, `s'` of type `α` and `t`, `t'` of type `β`, if `s` is a subset of `s'` and `t` is a subset of `t'`, then the Cartesian product of `s` and `t` is a subset of the Cartesian product of `s'` and `t'`. In other words, the Cartesian product of two subsets is itself a subset of the Cartesian product of their respective supersets.
More concisely: For any types `α` and `β`, and finite sets `s` of type `α` subset `s'`, `t` of type `β` subset `t'`, `s × t` is a subset of `s' × t'`.
|
Finset.nontrivial_prod_iff
theorem Finset.nontrivial_prod_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β},
(s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)
This theorem states that for any two given finsets 's' and 't' of any types 'α' and 'β' respectively, the Cartesian product of 's' and 't' is nontrivial if and only if both 's' and 't' are nonempty and at least one of them is nontrivial. Here, a nontrivial finset refers to a finset with at least two distinct elements.
More concisely: A finset product is nonempty and has at least two distinct elements if and only if both factors are nonempty and at least one is nontrivial.
|
Mathlib.Data.Finset.Prod._auxLemma.22
theorem Mathlib.Data.Finset.Prod._auxLemma.22 :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, (a ∈ s ∪ t) = (a ∈ s ∨ a ∈ t)
This theorem, `Mathlib.Data.Finset.Prod._auxLemma.22`, states that for any type `α` which has decidable equality, and any two finite sets `s` and `t` of type `α`, and any element `a` of type `α`, the statement "element `a` is in the union of `s` and `t`" is equivalent to the statement "element `a` is in `s` or `a` is in `t`". Essentially, it corresponds to the standard set theory fact that an element is in the union of two sets if and only if it is in one of the sets.
More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, the element `a` is in the union of `s` and `t` if and only if `a` is in `s` or `a` is in `t`.
|
Finset.mem_offDiag
theorem Finset.mem_offDiag :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α}, x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
This theorem states that for any type `α` with decidable equality and any finite set `s` of type `α`, a pair `x` of type `α` is in the off-diagonal of `s` if and only if both elements of the pair are in `s` and the elements of the pair are not equal. In mathematical terms, given a finite set `s` and a pair `(a, b)` of elements from `s`, `(a, b)` is in the off-diagonal set of `s` if and only if `a` and `b` are distinct elements of `s`.
More concisely: For any finite set `s` and distinct elements `a` and `b` in `s` of type `α` with decidable equality, the pair `(a, b)` lies in the off-diagonal of `s`. (Or equivalently, the off-diagonal of `s` consists of all pairs of distinct elements in `s`. )
|
Finset.diag_union_offDiag
theorem Finset.diag_union_offDiag :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.diag ∪ s.offDiag = s ×ˢ s
This theorem states that for any finite set `s` of type `α`, where `α` has decidable equality, the union of the diagonal and off-diagonal of `s` equals the cartesian product of `s` with itself. In other words, the set of all pairs `(a, a)` where `a` is in `s` (denoted as `Finset.diag s`), combined with the set of all pairs `(a, b)` where `a` and `b` are different elements in `s` (denoted as `Finset.offDiag s`), covers the entire set of all possible pairs that can be formed from elements in `s` (denoted as `s ×ˢ s`).
More concisely: For any finite set `s` of type `α` with decidable equality, `Finset.diag s ∪ Finset.offDiag s = s ×ˢ s`.
|
Finset.mem_diag
theorem Finset.mem_diag :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α}, x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2
This theorem states that for any type `α` with a decidable equality and any finite set `s` of type `α`, a pair `x` (of type `α × α`) is a member of the diagonal of `s` if and only if the first element of `x` is a member of `s` and the first and second elements of `x` are equal. In other words, the diagonal of a finite set `s` contains precisely those pairs whose elements are both in `s` and are equal.
More concisely: For any finite set `s` of type `α` with decidable equality, the diagonal of `s` equals the set of pairs `(x, x)` where `x` is in `s`.
|
Finset.coe_product
theorem Finset.coe_product : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), ↑(s ×ˢ t) = ↑s ×ˢ ↑t := by
sorry
This theorem states that for any two finite sets `s` of type `α` and `t` of type `β`, the Cartesian product of `s` and `t` when coerced to a set is equivalent to the Cartesian product of the coerced `s` and `t`. In mathematical terms, given two finite sets S and T, the theorem asserts that $(S \times T)$ is the same as $(S) \times (T)$.
More concisely: For any finite sets `s` of type `α` and `t` of type `β`, the coerced Cartesian product `(s : Set α) × (t : Set β)` is equivalent to the naive Cartesian product `(s : Set α) ×↑ (t : Set β)`.
|
Mathlib.Data.Finset.Prod._auxLemma.29
theorem Mathlib.Data.Finset.Prod._auxLemma.29 :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α}, (x ∈ s.diag) = (x.1 ∈ s ∧ x.1 = x.2)
This theorem states that for any type `α` with decidable equality and for any finite set `s` of type `α`, a pair of elements `(x.1, x.2)` belongs to the diagonal of `s` (i.e., `Finset.diag s`) if and only if the first element of the pair `x.1` belongs to the set `s` and `x.1` is equal to `x.2`. In other words, a pair is in the diagonal of `s` only when both its elements are the same and belong to the set `s`.
More concisely: For any finite set `s` of type `α` with decidable equality, the diagonal of `s` is equal to the set of pairs `(x.1, x.2)` where `x.1` is in `s` and `x.1` equals `x.2`.
|
Finset.Nonempty.fst
theorem Finset.Nonempty.fst :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).Nonempty → s.Nonempty
This theorem states that for any two types `α` and `β`, and any finite sets `s` of type `α` and `t` of type `β`, if the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is nonempty, then `s` is also nonempty. In other words, if there exists at least one pair `(a, b)` such that `a` is in `s` and `b` is in `t`, then there must exist at least one element in `s`.
More concisely: If the Cartesian product of non-empty sets `α` and `β` is nonempty, then `α` is nonempty.
|
Mathlib.Data.Finset.Prod._auxLemma.25
theorem Mathlib.Data.Finset.Prod._auxLemma.25 :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂)
This theorem, named `Mathlib.Data.Finset.Prod._auxLemma.25`, states that for any type `α` with a decidable equality (`DecidableEq α`), and for any elements `a` of type `α` and `s₁`, `s₂` of type `Finset α` (which are finite sets of elements of type `α`), the statement "`a` is in the intersection of `s₁` and `s₂`" is equivalent to the statement "`a` is in `s₁` and `a` is in `s₂`". This theorem essentially formalizes the definition of intersection for finite sets in the context of Lean 4.
More concisely: For any type `α` with decidable equality and any finite sets `s₁` and `s₂` of elements from `α`, the element `a` belongs to the intersection of `s₁` and `s₂` if and only if it belongs to both `s₁` and `s₂`.
|
Finset.coe_offDiag
theorem Finset.coe_offDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ↑s.offDiag = (↑s).offDiag := by
sorry
The theorem `Finset.coe_offDiag` states that for all finite sets `s` of a type `α` with decidable equality, the off-diagonal of `s` when treated as a finite set and then converted into a set (`↑(Finset.offDiag s)`) is equal to the off-diagonal of `s` directly considered as a set (`Set.offDiag ↑s`). In other words, the off-diagonal operation is consistent whether we consider `s` as a finite set or as a set in general.
Here, the off-diagonal of a set `s` is defined as the set of all pairs `(a, b)` such that `a` and `b` are in `s` and `a ≠ b`. The operation `↑` is used to convert a finite set to a general set in Lean 4.
More concisely: For any finite set `s` of type `α` with decidable equality, `Finset.offDiag s = Set.offDiag (↑s)`.
|
Finset.mem_product
theorem Finset.mem_product :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := by
sorry
This theorem states that for any two sets `s` of type `α` and `t` of type `β`, and any ordered pair `p` of type `α × β`, the pair `p` belongs to the Cartesian product of `s` and `t` if and only if the first element of `p` belongs to `s` and the second element of `p` belongs to `t`. The Cartesian product of `s` and `t` is denoted by `s ×ˢ t` in Lean 4.
More concisely: For any sets `s` and `t`, the ordered pair `p` belongs to the Cartesian product `s ×ˢ t` if and only if its first component belongs to `s` and its second component belongs to `t`.
|
Mathlib.Data.Finset.Prod._auxLemma.7
theorem Mathlib.Data.Finset.Prod._auxLemma.7 : ∀ {a b c : Prop}, (a ∧ b ∧ c) = (b ∧ a ∧ c)
This theorem states that for any three propositions `a`, `b`, and `c`, the conjunction of propositions `a`, `b`, and `c` in that order is equal to the conjunction of propositions `b`, `a`, and `c` in that order. In other words, the theorem asserts the commutativity of conjunction for any two propositions in a three-part conjunction while leaving the third proposition in place. Mathematically, it can be written as $(a \land b \land c) = (b \land a \land c)$.
More concisely: The theorem asserts the commutativity of conjunction for any two propositions in a three-part conjunction: $(a \land b \land c) = (b \land a \land c)$.
|
Mathlib.Data.Finset.Prod._auxLemma.30
theorem Mathlib.Data.Finset.Prod._auxLemma.30 :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α},
(x ∈ s.offDiag) = (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2)
The theorem `Mathlib.Data.Finset.Prod._auxLemma.30` asserts that for any type `α` with decidable equality, any finite set `s` of type `α`, and any pair `x` of type `α × α`, the pair `x` belongs to the off-diagonal of set `s` if and only if both elements of the pair belong to `s` and they are not equal to each other. In other words, a pair `(a, b)` is in the off-diagonal of a finite set `s` precisely when `a` and `b` are distinct elements of `s`.
More concisely: For any decidably equal type `α` and finite set `s` of `α`, a pair `(a, b)` is in the off-diagonal of `s` if and only if `a` and `b` are distinct elements of `s`.
|
Finset.product_biUnion
theorem Finset.product_biUnion :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq γ] (s : Finset α) (t : Finset β)
(f : α × β → Finset γ), (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)
The theorem `Finset.product_biUnion` states that for any given sets `s` of type `α`, `t` of type `β` and a function `f` that maps from a product of `α` and `β` to a set of `γ`, where `γ` has decidable equality, the bi-union over the product of `s` and `t` with the function `f` is equivalent to the bi-union over `s` with a function that takes an element `a` of `α` and returns the bi-union over `t` with a function that takes an element `b` of `β` and returns `f` applied to the pair `(a, b)`.
In other words, it emphasizes the distributivity of the bi-union operation over the product operation in the context of finite sets.
More concisely: For any sets `α`, `β`, and function `f` from `α × β` to a decidably equated set `γ`, the bi-union of `f` over the product of sets `s` of type `α` and `t` of type `β` is equal to the bi-union over `s` of the function that maps each `a` in `α` to the bi-union over `t` of `f` applied to `(a, b)`.
|
Mathlib.Data.Finset.Prod._auxLemma.1
theorem Mathlib.Data.Finset.Prod._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {p : α × β}, (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t) := by
sorry
This theorem states that for any two types `α` and `β`, any two finite sets `s` and `t` of these types, and any pair `p` of type `α` and `β`, the condition that `p` belongs to the cartesian product `s ×ˢ t` is equivalent to the condition that the first element of `p` belongs to `s` and the second element of `p` belongs to `t`.
More concisely: For any types `α` and `β`, and finite sets `s` of type `α` and `t` of type `β`, a pair `p` belongs to the cartesian product `s ×ˢ t` if and only if its first component belongs to `s` and its second component belongs to `t`.
|
Finset.Nonempty.snd
theorem Finset.Nonempty.snd :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).Nonempty → t.Nonempty
This theorem, `Finset.Nonempty.snd`, states that for any two types, `α` and `β`, and any two finite sets, `s` and `t`, of these respective types, if the Cartesian product of `s` and `t` is nonempty, it implies that the finite set `t` is also nonempty. In other words, if there exists at least one ordered pair in the product set `s ×ˢ t`, there must exist at least one element in the set `t`.
More concisely: If a finite product of sets is nonempty, then one of the sets is nonempty.
|
Finset.card_product
theorem Finset.card_product :
∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), (s ×ˢ t).card = s.card * t.card
This theorem states that for any two finite sets `s` and `t` of any types `α` and `β` respectively, the cardinality (i.e., the number of elements) of the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is equal to the product of the cardinalities of `s` and `t`. In other words, if you have `s.card` elements in set `s` and `t.card` elements in set `t`, then there will be `s.card * t.card` ordered pairs in the Cartesian product of `s` and `t`.
More concisely: For any finite sets `s` and `t` of types `α` and `β` respectively, the cardinality of their Cartesian product `s ×ˢ t` equals the product of their cardinalities `s.card * t.card`.
|
Finset.offDiag_card
theorem Finset.offDiag_card :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.offDiag.card = s.card * s.card - s.card
The theorem `Finset.offDiag_card` states that for any finite set `s` of a type `α` with decidable equality, the cardinality of the off-diagonal of `s` (denoted as `Finset.offDiag s`), which is the set of all distinct pairs `(a, b)` where `a` and `b` are elements of `s`, is equal to the square of the cardinality of `s` minus the cardinality of `s` itself. In mathematical notation, for a finite set $S$, the size of the off-diagonal set of $S$ is given by $|S|^2 - |S|$.
More concisely: The cardinality of the set of distinct pairs of elements in a finite set is equal to the square of its cardinality minus the cardinality of the set itself.
|
Mathlib.Data.Finset.Prod._auxLemma.15
theorem Mathlib.Data.Finset.Prod._auxLemma.15 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = (a ∧ b ∧ c)
This theorem, `Mathlib.Data.Finset.Prod._auxLemma.15`, states that for any three propositions `a`, `b`, and `c`, the assertion that `a` and `b` are true and `c` is true is logically equivalent to the assertion that `a` is true, and `b` and `c` are also true. This is a property of logical conjunction (the "and" operation denoted by `∧`), demonstrating the associative property of conjunction in propositional logic.
More concisely: The theorem `Mathlib.Data.Finset.Propositional.and_assoc` states that for all propositions `a`, `b`, and `c`, `(a ∧ b) ∧ c` is logically equivalent to `a ∧ b ∧ c`.
|