InfClosed.dual
theorem InfClosed.dual :
∀ {α : Type u_2} [inst : Lattice α] {s : Set α}, InfClosed s → SupClosed (⇑OrderDual.ofDual ⁻¹' s)
This theorem, `InfClosed.dual`, states that for any type `α` that forms a lattice and for any set `s` of elements from `α` that is inf-closed (i.e., for any two elements `a` and `b` in `s`, the infimum of `a` and `b` also belongs to `s`), the preimage of `s` under the operation of `OrderDual.ofDual` (which is essentially the identity function from the order dual of a linear order), is sup-closed. In other words, if you take any two elements from this preimage set, their supremum will still belong to this set. This theorem forms an alias of the reverse direction of another theorem, `supClosed_preimage_ofDual`.
More concisely: For any inf-closed set `s` of elements in a lattice `α`, the preimage of `s` under the order dual function is sup-closed.
|
supClosed_supClosure
theorem supClosed_supClosure : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, SupClosed (supClosure s) := by
sorry
The theorem `supClosed_supClosure` states that for every type `α` that forms a join-semilattice (denoted as `SemilatticeSup α`), and for every set `s` of this type `α`, the closure under join operation (`supClosure`) of the set `s` is supremum-closed (`SupClosed`). In other words, for any two elements `a` and `b` in the closure of the set, their supremum (join) also belongs to the closure. This is a property of join-semilattices, where every subset generates a sub-structure that is also a join-semilattice.
More concisely: For every join-semilattice type `α` and set `s` of elements in `α`, the supremum of any two elements in the supremum-closure of `s` lies in the supremum-closure of `s`.
|
SupClosed.preimage
theorem SupClosed.preimage :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {s : Set α}
[inst_2 : FunLike F β α] [inst_3 : SupHomClass F β α], SupClosed s → ∀ (f : F), SupClosed (⇑f ⁻¹' s)
The theorem `SupClosed.preimage` states that for any types `F`, `α`, `β`, where `α` and `β` are semilattice sup types, a set `s` of type `α`, a function-like object `f` of type `F` from `β` to `α`, and a sup-homomorphism class instance for `F`, `β`, and `α`, if the set `s` is sup-closed (i.e., for all elements `a` and `b` in `s`, their least upper bound `a ⊔ b` is also in `s`), then the preimage of `s` under the function `f` (denoted by `⇑f ⁻¹' s`) is also sup-closed.
More concisely: If `s` is a sup-closed set in a semilattice `α` and `f` is a sup-homomorphism from a semilattice `β` to `α`, then the preimage `f⁻¹(s)` is a sup-closed set in `β`.
|
SupClosed.finsetSup'_mem
theorem SupClosed.finsetSup'_mem :
∀ {α : Type u_2} [inst : SemilatticeSup α] {ι : Type u_4} {f : ι → α} {s : Set α} {t : Finset ι},
SupClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s
This theorem states that for all types `α` and `ι` with `α` being a join-semilattice, and given a function `f` from `ι` to `α`, a set `s` of type `α`, and a nonempty finite set `t` of type `ι`, if the set `s` is sup-closed (i.e., for any two elements `a` and `b` in `s`, their supremum also belongs to `s`), and every element of `t` mapped via `f` is in `s`, then the supremum of the image of `t` under `f` also belongs to `s`. In other words, if a set `s` is sup-closed, then it also contains the supremum of any nonempty finite subset of `s` under a function `f`.
More concisely: If `α` is a join-semilattice, `f` is a function from a nonempty finite set `ι` to `α`, `s` is a sup-closed subset of `α`, and for all `i` in `t`, `f(i)` is in `s`, then the supremum of `f``(t)` is in `s`.
|
InfClosed.image
theorem InfClosed.image :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {s : Set α}
[inst_2 : FunLike F α β] [inst_3 : InfHomClass F α β], InfClosed s → ∀ (f : F), InfClosed (⇑f '' s)
This theorem states that if a set `s` of elements in a semilattice `α` is inf-closed (that is, the infimum of any two elements in `s` is also in `s`) and there is a function `f` of type `F` that behaves like a homomorphism preserving infimum operations (an `InfHomClass`) from `α` to another semilattice `β`, then the image of `s` under `f` is also inf-closed in `β`. In simple terms, applying an infimum-preserving function to an inf-closed set results in an inf-closed set.
More concisely: If `s` is an inf-closed set in a semilattice `α` and `f` is a function from `α` to another semilattice `β` that preserves infima, then the image of `s` under `f` is an inf-closed set in `β`.
|
SupClosed.dual
theorem SupClosed.dual :
∀ {α : Type u_2} [inst : Lattice α] {s : Set α}, SupClosed s → InfClosed (⇑OrderDual.ofDual ⁻¹' s)
The theorem `SupClosed.dual` states that for any type `α` that forms a lattice, and for any set `s` of elements from `α`, if the set `s` is sup-closed (i.e., for any two elements `a` and `b` in `s`, their supremum `a ⊔ b` also belongs to `s`), then the preimage of `s` under the identity function from the OrderDual (a structure in which the order of the elements is reversed) is inf-closed (i.e., for any two elements `a` and `b` in this preimage set, their infimum `a ⊓ b` also belongs to this set).
In other words, this theorem is essentially stating a duality property between supremum and infimum in the context of sup-closed and inf-closed sets under the OrderDual transformation.
More concisely: For any sup-closed set in a lattice under OrderDual, its preimage is inf-closed.
|
IsSublattice.dual
theorem IsSublattice.dual :
∀ {α : Type u_2} [inst : Lattice α] {s : Set α}, IsSublattice s → IsSublattice (⇑OrderDual.ofDual ⁻¹' s)
This theorem, referred to as `IsSublattice.dual`, states that for any type `α` that is a lattice, and any set `s` of elements of `α` that forms a sublattice, the preimage of `s` under the function `OrderDual.ofDual` (which is the identity function on the dual of the linear order) also forms a sublattice. Essentially, this theorem ensures that the property of being a sublattice is maintained under the operation of taking the dual and then taking the preimage of a set under the dual map.
More concisely: For any lattice `α` and sublattice `s` of `α`, the preimage of `s` under the order dual function forms a sublattice.
|
Set.Finite.infClosure
theorem Set.Finite.infClosure :
∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s.Finite → (infClosure s).Finite
The theorem states that in a semilattice, if a set is finite, then the semilattice generated by this set, which is a set closed under the infimum operation (also known as "meet" or "greatest lower bound"), is also finite. In other words, if we start with a finite set in a semilattice, the set of all lower bounds that can be obtained by taking the infimum of subsets of this original set is also finite.
More concisely: In a semilattice, the semilattice generated by a finite set is finite.
|
IsSublattice.latticeClosure_eq
theorem IsSublattice.latticeClosure_eq :
∀ {α : Type u_2} [inst : Lattice α] {s : Set α}, IsSublattice s → latticeClosure s = s
This theorem, named `IsSublattice.latticeClosure_eq`, states that for any type `α` with a `Lattice` structure, and any set `s` of type `α`, if `s` forms a sublattice, then the lattice closure of `s` is equal to `s` itself. In other words, if a set `s` is already a sublattice within a given lattice structure, applying the lattice closure operation won't modify `s`; it remains the same.
More concisely: If `s` is a sublattice of a lattice `α`, then the lattice closure of `s` equals `s`.
|
Mathlib.Order.SupClosed._auxLemma.21
theorem Mathlib.Order.SupClosed._auxLemma.21 :
∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, (supClosure s = s) = SupClosed s
This theorem states that for any type `α` that forms a join-semilattice (denoted `SemilatticeSup α`), and any set `s` of elements of type `α`, the set `s` being equal to its sup-closure is equivalent to the set `s` being sup-closed. In other words, a set `s` is sup-closed (i.e., for any two elements `a` and `b` in `s`, their join, or supremum, `a ⊔ b` is also in `s`) if and only if `s` equals its sup-closure (the smallest sup-closed set that contains `s`).
More concisely: For any join-semilattice type `α`, a set `s` of elements is sup-closed if and only if it equals its sup-closure, i.e., the smallest join-closed set containing `s`.
|
IsSublattice.of_dual
theorem IsSublattice.of_dual :
∀ {α : Type u_2} [inst : Lattice α] {s : Set αᵒᵈ}, IsSublattice s → IsSublattice (⇑OrderDual.toDual ⁻¹' s) := by
sorry
This theorem, **Alias of the reverse direction of `isSublattice_preimage_toDual`**, states that for any type `α` which is a lattice and any set `s` of elements from the dual order of `α`, if `s` is a sublattice of the dual order, then the pre-image of `s` under the function `OrderDual.toDual` is a sublattice in the original lattice `α`. In simpler terms, this theorem helps in translating sublattice properties from a dual order of a lattice back to the original lattice.
More concisely: For any lattice `α` and subset `s` of its dual order that is a sublattice, the preimage of `s` under the `OrderDual.toDual` function is a sublattice in `α`.
|
supClosed_sInter
theorem supClosed_sInter :
∀ {α : Type u_2} [inst : SemilatticeSup α] {S : Set (Set α)}, (∀ s ∈ S, SupClosed s) → SupClosed S.sInter := by
sorry
The theorem `supClosed_sInter` states that for any type `α` that forms a semilattice with respect to the operation `sup` (denoted `⊔`), and for any set `S` of sets of elements of type `α`, if every set `s` in `S` is sup-closed, then the intersection over all sets in `S` is also sup-closed. In other words, if every set in `S` has the property that for any two elements `a` and `b` in the set, their supremum `a ⊔ b` is also in the set, then this property holds for the intersection of all sets in `S` as well.
More concisely: If `α` is a semilattice with respect to `⊔` and every `s` in the set `S` of subsets of `α` is sup-closed, then the intersection of all sets in `S` is sup-closed.
|
InfClosed.infClosure_eq
theorem InfClosed.infClosure_eq :
∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, InfClosed s → infClosure s = s
This theorem, referred to as the **Alias of the reverse direction of `infClosure_eq_self`**, states that for any type `α` that is an instance of the `SemilatticeInf` class and any set `s` of elements of type `α`, if the set `s` is inf-closed (i.e., for any two elements `a` and `b` in `s`, their infimum is also in `s`), then the inf-closure of `s` (the smallest inf-closed set containing `s`) is equal to `s` itself. In other words, if a set is inf-closed, its inf-closure does not add any new elements.
More concisely: If `α` is a semilattice with infimum and `s` is an inf-closed set of `α`, then the inf-closure of `s` equals `s`.
|
InfClosed.finsetInf'_mem
theorem InfClosed.finsetInf'_mem :
∀ {α : Type u_2} [inst : SemilatticeInf α] {ι : Type u_4} {f : ι → α} {s : Set α} {t : Finset ι},
InfClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s
This theorem states that for any type `α` that forms a semilattice under an infimum operation, given a function `f` from some type `ι` to `α`, a set `s` of elements of type `α`, and a nonempty finite set `t` of elements of type `ι`, if the set `s` is infimum-closed (meaning that the infimum of any two elements in `s` also belongs to `s`), and every image of an element in `t` under function `f` belongs to `s`, then the infimum of the images of elements in `t` under `f` also belongs to `s`. In mathematical notation, if `s ⊆ α` is infimum-closed and `(∀ i ∈ t, f(i) ∈ s)`, then `inf_{i∈t} f(i) ∈ s`.
More concisely: Given a semilattice `α` with infimum operation, if `s ⊆ α` is infimum-closed and for all `i ∈ t`, `f(i) ∈ s`, then `inf_{i∈t} f(i) ∈ s`.
|
subset_supClosure
theorem subset_supClosure : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s ⊆ supClosure s
This theorem states that for any type `α` that is a join-semilattice, and for any set `s` of elements of type `α`, `s` is a subset of the set generated by the `supClosure` operation applied to `s`. In other words, applying the `supClosure` operation to a set in a join-semilattice will always produce a set that includes the original set. The `supClosure` operation is defined so that it generates a set that is closed under the join operation of the semilattice.
More concisely: For any join-semilattice type `α` and set `s` of elements in `α`, the `supClosure` of `s` includes `s`. In other words, `supClosure s ⊆ {x | ∃y ∈ s, x = sup s {y}}`.
|
Mathlib.Order.SupClosed._auxLemma.32
theorem Mathlib.Order.SupClosed._auxLemma.32 :
∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, (infClosure s = s) = InfClosed s
This theorem states that for any type `α` that has `SemilatticeInf` structure and any set `s` of `α`, the set `s` is closed under the `infClosure` operation if and only if it is `InfClosed`. In other words, a set `s` is equivalent to its "inf-closure" (i.e., the smallest set containing `s` that is closed under taking infimums) if and only if for every pair of elements `a` and `b` in `s`, their infimum `a ⊓ b` is also in `s`. This characterizes the closure operation in a join-semilattice by the property of being closed under infimums.
More concisely: A set of a type with `SemilatticeInf` structure is equal to its inf-closure if and only if it is closed under taking infimums.
|
subset_infClosure
theorem subset_infClosure : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s ⊆ infClosure s
The theorem `subset_infClosure` states that for any set `s` in a type `α`, where `α` forms a semilattice under the infimum operation (expressed as `SemilatticeInf α`), the set `s` is a subset of the set generated by the `infClosure` of `s`. In other words, all elements of `s` are included in the set that is closed under the infimum operation generated from `s`.
More concisely: For any semilattice `α` and set `s` in `α`, `s` is a subset of the set generated by the infimum closure of `s`.
|
InfClosed.preimage
theorem InfClosed.preimage :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {s : Set α}
[inst_2 : FunLike F β α] [inst_3 : InfHomClass F β α], InfClosed s → ∀ (f : F), InfClosed (⇑f ⁻¹' s)
The theorem `InfClosed.preimage` states that for any types `F`, `α`, and `β`, where `α` and `β` are both semilattices with an infimum operation (i.e., a binary operation that returns the greatest lower bound of two elements), if we have a function-like object `f` from `β` to `α` that respects the infimum operation (expressed by the `InfHomClass` attribute), and if a set `s` of elements of type `α` is inf-closed (meaning that the infimum of any two elements in the set is also in the set), then the preimage of `s` under `f` (i.e., the set of all elements of type `β` that `f` maps into `s`) is also inf-closed.
More concisely: If `f` is a function-like object from a semilattice `β` to a semilattice `α` preserving infima, and `s` is an inf-closed set in `α`, then the preimage of `s` under `f` is also inf-closed in `β`.
|
supClosed_univ
theorem supClosed_univ : ∀ {α : Type u_2} [inst : SemilatticeSup α], SupClosed Set.univ
The theorem `supClosed_univ` states that for any type `α` that forms a semilattice with a supremum operation (`SemilatticeSup α`), the universal set (`Set.univ`) is supremum-closed (`SupClosed`). In other words, for any two elements `a` and `b` in the set, the supremum of `a` and `b`, denoted by `a ⊔ b`, is also in the set. This holds true universally for all types that have a supremum operation.
More concisely: For any semilattice type `α` with supremum operation, the universal set is supremum-closed, i.e., the supremum of any two elements in the set belongs to the set.
|
Set.Finite.supClosure
theorem Set.Finite.supClosure :
∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s.Finite → (supClosure s).Finite
The theorem `Set.Finite.supClosure` states that for any finite set `s` in a semilattice `α`, the closure of `s` under the supremum operation (generated by `supClosure`) is also finite. In other words, when a finite set is closed under the join operation in a semilattice, the resulting set remains finite.
More concisely: For any finite set in a semilattice, its closure under the supremum operation is also finite.
|
SupClosed.supClosure_eq
theorem SupClosed.supClosure_eq :
∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, SupClosed s → supClosure s = s
This theorem, known as the **Alias of the reverse direction of supClosure_eq_self**, states that for any type `α` that forms a join-semilattice (denoted by `SemilatticeSup α`), if a set `s` of type `α` is sup-closed (meaning that the supremum (or join) of any two elements in the set is also in the set), then applying the `supClosure` operation to `s` will not change `s`. In other words, a sup-closed set is already closed under the supremum operation, so the `supClosure` operation, which generates a set closed under supremum from any set, has no effect on it.
More concisely: For any join-semilattice type `α`, a sup-closed set `s` is equivalent to its supremum closure, i.e., `supClosure s = s`.
|
infClosed_sInter
theorem infClosed_sInter :
∀ {α : Type u_2} [inst : SemilatticeInf α] {S : Set (Set α)}, (∀ s ∈ S, InfClosed s) → InfClosed S.sInter := by
sorry
The theorem `infClosed_sInter` states that for any type `α` that forms a semilattice under an infimum operation, and any collection `S` of sets of elements of `α`, if every set in `S` is inf-closed (i.e., the infimum of any two elements in the set is also in the set), then the intersection of all sets in `S` is also inf-closed. In mathematical terms, if `S` is a collection of inf-closed sets in a semilattice `α`, then the infimum of any two elements in the intersection of sets in `S` is also in that intersection.
More concisely: If `α` is a semilattice with infimum and every set in the collection `S` of inf-closed sets is in `α`, then the infimum of any two elements in the intersection of sets in `S` belongs to that intersection.
|
infClosed_univ
theorem infClosed_univ : ∀ {α : Type u_2} [inst : SemilatticeInf α], InfClosed Set.univ
The theorem `infClosed_univ` states that for any type `α` that has a structure of `SemilatticeInf` (meaning it has a binary operation `⊓` that is associative, commutative, and idempotent), the universal set of `α` is inf-closed. In other words, for any two elements `a` and `b` in the universal set of `α`, their infimum (i.e., the result of the operation `a ⊓ b`) is also in the universal set.
More concisely: For any type `α` with a `SemilatticeInf` structure, the universal set is closed under the infimum operation.
|
Mathlib.Order.SupClosed._auxLemma.36
theorem Mathlib.Order.SupClosed._auxLemma.36 :
∀ {α : Type u_2} [inst : Lattice α] {s : Set α}, (latticeClosure s = s) = IsSublattice s
This theorem states that for any type `α` which forms a lattice, and for any set `s` of elements of type `α`, the lattice closure of `s` is equal to `s` if and only if `s` is itself a sublattice. In other words, in the context of a lattice, a set is closed under the join operation (i.e., it contains the join of any of its elements) if and only if it forms a sublattice.
More concisely: For any lattice `α` and subset `s` of `α`, `s` is the lattice closure of `s` if and only if `s` is a sublattice.
|
SupClosed.image
theorem SupClosed.image :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {s : Set α}
[inst_2 : FunLike F α β] [inst_3 : SupHomClass F α β], SupClosed s → ∀ (f : F), SupClosed (⇑f '' s)
The theorem `SupClosed.image` states that for any types `F`, `α`, `β`, with `α` and `β` being semilattice sup structures, a set `s` of type `α`, and an injective function-like `F` that maps `α` to `β`, if the set `s` is supremum-closed (i.e., the supremum of any two elements of `s` also belongs to `s`), then the image of `s` under the function `f` of type `F` is also supremum-closed. It means, when `s` is a sup-closed set and `f` is a mapping that preserves sup-operation, then the image of `s` via `f` remains sup-closed in the target domain.
More concisely: If `F` is an injective function-like map between semilattice sup structures `α` and `β`, `s` is a supremum-closed set in `α`, then the image `F[s]` is supremum-closed in `β`.
|
infClosed_infClosure
theorem infClosed_infClosure : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, InfClosed (infClosure s) := by
sorry
The theorem `infClosed_infClosure` states that for any type `α` that forms a semilattice with respect to an "infimum" operation (denoted as `⊓`), and for any set `s` of elements of type `α`, the closure of `s` under the infimum operation is an inf-closed set. Here, a set is said to be inf-closed if for every pair of elements in the set, their infimum is also in the set. Furthermore, the "infimum closure" of a set `s` is the set of all elements that can be expressed as the infimum of some non-empty subset of `s`.
More concisely: For any semilattice type `α` with infimum operation `⊓` and any inf-closed set `s` of elements in `α`, the infimum closure of `s` is equal to the set of all elements that are the infimum of some non-empty subset of `s`.
|