Finset.infs_compls_eq_diffs
theorem Finset.infs_compls_eq_diffs :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : BooleanAlgebra α] (s t : Finset α), s ⊼ t.compls = s.diffs t := by
sorry
The theorem `Finset.infs_compls_eq_diffs` states that for any two finite sets `s` and `t` of a type `α`, where `α` is a Boolean algebra and has decidable equality, the supremum of `s` and the complement of each element in `t` (`s ⊼ Finset.compls t`) is equal to the set of all elements of the form `a \ b` where `a` is in `s` and `b` is in `t` (`Finset.diffs s t`). This theorem is essentially stating a property about operations on finite sets in a Boolean algebra.
More concisely: For finite sets \(s, t \subseteq \alpha\) in a Boolean algebra with decidable equality, \(sup(s) \cap \bigcap_{x \in t} complement(x) = Finset.diffs(s, t)\).
|
Finset.coe_sups
theorem Finset.coe_sups :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α), ↑(s ⊻ t) = ↑s ⊻ ↑t
The theorem `Finset.coe_sups` states that for all types `α`, given that `α` has decidable equality and is a semilattice for the operation supremum, and given two finite sets `s` and `t` of type `α`, the symmetric difference of the coe (type-cast) of `s` and `t` is equal to the coe of the symmetric difference of `s` and `t`. In simpler terms, the theorem asserts that the operation of taking the symmetric difference commutes with the operation of type-casting from finite sets to sets in the context of semilattice structures with decidable equality.
More concisely: For type-casted finite sets `s` and `t` in a semilattice with decidable equality, `(s ++ t)}^.{Finset α} = s.^.{Finset α} ++ t.^.{Finset α}`, where `++` denotes symmetric difference and `.^` denotes type-casting.
|
Mathlib.Data.Finset.Sups._auxLemma.19
theorem Mathlib.Data.Finset.Sups._auxLemma.19 :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
[inst_3 : DecidableRel Disjoint] {s t : Finset α} {c : α},
(c ∈ s.disjSups t) = ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c
The theorem `Mathlib.Data.Finset.Sups._auxLemma.19` states that for any type `α` with decidable equality, a semilattice structure, an order bot structure and a decidable relation of disjointness, given two finsets `s` and `t` and an element `c` of type `α`, `c` is in the finset of elements obtained by taking the supremum of disjoint elements from `s` and `t` (denoted as `Finset.disjSups s t`) if and only if there exist elements `a` and `b` in `s` and `t` respectively, such that `a` and `b` are disjoint and `c` is the supremum of `a` and `b`.
In other words, an element `c` belongs to the finset of supremums of disjoint pairs from `s` and `t` if and only if `c` is the supremum of some disjoint pair from `s` and `t`.
More concisely: For finsets `s` and `t` over a type `α` with decidable equality, semilattice and order bot structures, and a decidable disjointness relation, an element `c` is in the finset of suprema of disjoint pairs from `s` and `t` if and only if there exist disjoint elements `a` in `s` and `b` in `t` such that `c = a ⨝ b`. (Here, `⨝` denotes the supremum in the semilattice.)
|
Finset.Nonempty.of_compls
theorem Finset.Nonempty.of_compls :
∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.compls.Nonempty → s.Nonempty
This theorem, `Finset.Nonempty.of_compls`, is an alias of the forward direction of the `Finset.compls_nonempty` theorem. It states that for any type `α` that is equipped with a Boolean algebra structure, and for any finite set `s` of `α`, if the set of complements of `s` is nonempty, then `s` itself must be nonempty.
More concisely: If the complements of a finite set in a Boolean algebra are nonempty, then the set itself is nonempty.
|
Mathlib.Data.Finset.Sups._auxLemma.28
theorem Mathlib.Data.Finset.Sups._auxLemma.28 :
∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α} {a : α}, (a ∈ s.compls) = (aᶜ ∈ s)
The theorem `Mathlib.Data.Finset.Sups._auxLemma.28` states that for any type `α` that forms a Boolean algebra, for any finite set `s` of `α`, and for any element `a` of `α`, `a` is an element of the complement of `s` if and only if the complement of `a` is an element of `s`. Here the complement operation is as per the Boolean algebra. This theorem establishes a relationship between an element and its complement in terms of their membership in a set and its complement.
More concisely: For any Boolean algebra `α`, and finite set `s` from `α`, an element `a` is in the complement of `s` if and only if the complement of `a` is in `s`.
|
Finset.compls_compls
theorem Finset.compls_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Finset α), s.compls.compls = s := by
sorry
This theorem states that for any finite set `s` within a Boolean algebra `α`, applying the `Finset.compls` operation twice on `s` will give us back the original set `s`. In other words, the `Finset.compls` operation is an involution in the context of a Boolean algebra, i.e., it is its own inverse. This operation is essentially taking the complement of each element in the set, so this theorem is asserting that taking the complement twice returns to the original element, a well-known property in Boolean algebra.
More concisely: In a Boolean algebra, the complement operation on a finite set is idempotent, that is, applying it twice to a set results in the original set.
|
Mathlib.Data.Finset.Sups._auxLemma.6
theorem Mathlib.Data.Finset.Sups._auxLemma.6 : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ = s₂) = (↑s₁ = ↑s₂)
This theorem, `Mathlib.Data.Finset.Sups._auxLemma.6`, states that for any type `α` and any finite sets `s₁` and `s₂` of that type, `s₁` is equal to `s₂` if and only if the set of elements in `s₁` (denoted by `↑s₁`) is equal to the set of elements in `s₂` (denoted by `↑s₂`). In other words, two finite sets are the same if they contain the same elements.
More concisely: Two finite sets `s₁` and `s₂` of type `α` are equal if and only if their elements are identical, i.e., `↑s₁ = ↑s₂`.
|
Finset.Nonempty.compls
theorem Finset.Nonempty.compls :
∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.Nonempty → s.compls.Nonempty
This theorem, `Finset.Nonempty.compls`, states that for any type `α` that has a Boolean algebra structure, if a finite set `s` of elements of type `α` is nonempty, then the set of complements of `s` (`s.compls`) is also nonempty. This theorem is an alias of the reverse direction of `Finset.compls_nonempty` theorem.
More concisely: For any finite, nonempty set `s` in a Boolean algebra, the set of complements of `s` is nonempty.
|
Finset.coe_infs
theorem Finset.coe_infs :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α), ↑(s ⊼ t) = ↑s ⊼ ↑t
The theorem `Finset.coe_infs` states that for any given types `α`, which has a decidable equality and is a semilattice under the operation of infimum, and any two finsets `s` and `t` of type `α`, the infimum of the union of `s` and `t` is the same as the union of the infimums of `s` and `t`. Essentially, this theorem asserts that the operation of finding the infimum commutes with the operation of taking the union in the context of finsets.
More concisely: For any semilattic type `α` with decidable equality, the infimum of the union of two finsets `s` and `t` over `α` equals the union of the infima of `s` and `t`.
|