CompleteLattice.IsSupClosedCompact.isSupFiniteCompact
theorem CompleteLattice.IsSupClosedCompact.isSupFiniteCompact :
∀ (α : Type u_2) [inst : CompleteLattice α],
CompleteLattice.IsSupClosedCompact α → CompleteLattice.IsSupFiniteCompact α
This theorem, referred to as the "Alias" of the reverse direction of `CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact`, states that for any complete lattice α, if α has the property that any supremum-closed, non-empty subset contains its supremum (sSup), then α also has the property that any subset has a finite subset with the same supremum (sSup). In other words, the condition of being a supremum-closed compact lattice implies that the lattice is also a supremum-finite compact lattice.
More concisely: In a complete lattice, if every supremum-closed, non-empty subset has its supremum, then every subset has a finite sup-subset with the same supremum.
|
CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt
theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt :
∀ {α : Type u_3} [inst : CompleteLattice α] {k : α},
CompleteLattice.IsCompactElement k →
∀ {s : Set α}, s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → (∀ x ∈ s, x < k) → sSup s < k
The theorem `CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt` states that for any type `α` equipped with a complete lattice structure, given a compact element `k` and any non-empty directed set `s` of elements from `α` that are strictly less than `k`, the supremum (`sSup`) of the set `s` is also strictly less than `k`. Here, a set is directed if for any two elements in the set, there is a third element in the set that is larger than or equal to the first two. And an element is compact if for any set whose supremum is greater or equal to the element, there exists a finite subset whose supremum is also greater or equal to the element.
More concisely: For any complete lattice `α` and compact element `k` in `α`, if `s` is a non-empty directed set of elements strictly less than `k`, then `sSup(s)` is strictly less than `k`.
|
CompleteLattice.WellFounded.finite_ne_bot_of_independent
theorem CompleteLattice.WellFounded.finite_ne_bot_of_independent :
∀ {α : Type u_2} [inst : CompleteLattice α],
(WellFounded fun x x_1 => x > x_1) →
∀ {ι : Type u_3} {t : ι → α}, CompleteLattice.Independent t → {i | t i ≠ ⊥}.Finite
The theorem `CompleteLattice.WellFounded.finite_ne_bot_of_independent` states that for any type `α` with a `CompleteLattice` structure, if the greater-than relation on `α` is well-founded, then for any type `ι` and any function `t : ι → α`, if the function `t` is independent (meaning for any subset of `ι`, the join of the images under `t` equals the join of the function `t` at each element of the subset), then the set of indices `i` such that `t i` is not the bottom element of the lattice is finite. This theorem links the concepts of well-foundedness, independence, and finiteness in the context of complete lattices.
More concisely: In a complete lattice with well-founded greater-than relation, the images under an independent function from a type to the lattice, excluding the bottom element, form a finite set.
|
exists_setIndependent_isCompl_sSup_atoms
theorem exists_setIndependent_isCompl_sSup_atoms :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsModularLattice α] [inst_2 : IsCompactlyGenerated α],
sSup {a | IsAtom a} = ⊤ →
∀ (b : α), ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
This theorem states that, in an atomic lattice, every element `b` can be complemented by the supremum of a set `s`, where each element of `s` is an atom (an element with no elements between it and the bottom element, excluding the bottom element itself). This holds in a complete lattice that is also modular and compactly generated, and where the supremum of all atoms is the top element. The set `s` has the property of being an independent set, which means each element in it is disjoint from the supremum of the rest of the set.
More concisely: In a complete, modular, compactly generated atomic lattice with a top element, every atom has a complement equal to the supremum of an independent set of atoms.
|
Mathlib.Order.CompactlyGenerated.Basic._auxLemma.14
theorem Mathlib.Order.CompactlyGenerated.Basic._auxLemma.14 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α}, (iSup s = ⊥) = ∀ (i : ι), s i = ⊥ := by
sorry
This theorem states that for any type `α` and index type `ι`, where `α` is a complete lattice, and `s` is a function from `ι` to `α`, the indexed supremum (`iSup`) of `s` is equal to the bottom element (`⊥`) if and only if all elements of `s` are equal to the bottom element. In other words, the supremum of a set of elements in a complete lattice is the bottom element if and only if each element in the set is the bottom element.
More concisely: For any complete lattice `α` and index type `ι`, the indexed supremum `iSup` of a function `s : ι → α` is the bottom element `⊥` if and only if all elements in the image of `s` are equal to `⊥`.
|
CompleteLattice.wellFounded_characterisations
theorem CompleteLattice.wellFounded_characterisations :
∀ (α : Type u_2) [inst : CompleteLattice α],
[WellFounded fun x x_1 => x > x_1, CompleteLattice.IsSupFiniteCompact α, CompleteLattice.IsSupClosedCompact α,
∀ (k : α), CompleteLattice.IsCompactElement k].TFAE
This theorem states that for any type `α` that forms a complete lattice, the following four properties are equivalent:
1. The relation `x > x_1` is well-founded, i.e., there are no infinitely decreasing chains.
2. The complete lattice has the sup-finite compactness property, i.e., any subset has a finite subset with the same supremum.
3. The complete lattice has the sup-closed compactness property, i.e., any non-empty subset that is closed under taking suprema contains its own supremum.
4. Every element `k` of the complete lattice is a compact element, i.e., for any set with supremum above `k`, there exists a finite subset also with supremum above `k`.
In other words, for a complete lattice, these four properties - well-foundedness of the greater-than relation, sup-finite compactness, sup-closed compactness, and compactness of each element – either all hold or all fail together.
More concisely: A complete lattice is well-founded if and only if it satisfies the sup-finite compactness, sup-closed compactness, and compactness properties for every element.
|
Mathlib.Order.CompactlyGenerated.Basic._auxLemma.13
theorem Mathlib.Order.CompactlyGenerated.Basic._auxLemma.13 :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b = (a ⊓ b = ⊥)
This theorem states that for any type `α` which is a semilattice with respect to the infimum operation and has a bottom element, and for any two elements `a` and `b` of that type, `a` and `b` are disjoint (defined as every element `x` that is less than or equal to both `a` and `b` must also be less than or equal to the bottom element) if and only if the infimum of `a` and `b` is the bottom element. This theorem is generalizing the property of disjoint sets, where the intersection of two disjoint sets is empty, to an arbitrary semilattice with a bottom element.
More concisely: For any semilattice with a bottom element α, elements a and b are disjoint if and only if their infimum is the bottom element.
|
CompleteLattice.IsSupFiniteCompact.wellFounded
theorem CompleteLattice.IsSupFiniteCompact.wellFounded :
∀ (α : Type u_2) [inst : CompleteLattice α],
CompleteLattice.IsSupFiniteCompact α → WellFounded fun x x_1 => x > x_1
This theorem states that for any type `α` that is a complete lattice, if the compactness property holds (which means that for any subset of `α`, there exists a finite subset that has the same supremum), then the relation of being strictly greater than is well-founded on `α`. In other words, there isn't an infinite descending chain of elements in `α` under the "greater than" relation.
More concisely: If `α` is a complete lattice with the compactness property, then the strict order relation is well-founded on `α`.
|
CompleteLattice.IsCompactElement.exists_finset_of_le_iSup
theorem CompleteLattice.IsCompactElement.exists_finset_of_le_iSup :
∀ (α : Type u_2) [inst : CompleteLattice α] {k : α},
CompleteLattice.IsCompactElement k → ∀ {ι : Type u_3} (f : ι → α), k ≤ ⨆ i, f i → ∃ s, k ≤ ⨆ i ∈ s, f i
The theorem `CompleteLattice.IsCompactElement.exists_finset_of_le_iSup` states that for any type `α` that forms a complete lattice, and any element `k` of `α` that is a "compact element" (also known as "finite" or "S-compact"), and for any function `f` from another type `ι` to `α`, if `k` is less than or equal to the supremum (denoted by `⨆`) of the range of `f`, then there exists a finite subset `s` of `ι` such that `k` is less than or equal to the supremum of the range of `f` restricted to `s`. This theorem shows that in a complete lattice, the supremum of an infinite set can be approximated by the supremum of a finite subset if the compactness condition is satisfied.
More concisely: Given a complete lattice `α`, a compact element `k` of `α`, and a function `f` from a type `ι` to `α` such that `k` is less than or equal to the supremum of `f`, there exists a finite subset `s` of `ι` such that `k` is less than or equal to the supremum of `f` restricted to `s`.
|
CompleteLattice.Iic_coatomic_of_compact_element
theorem CompleteLattice.Iic_coatomic_of_compact_element :
∀ {α : Type u_2} [inst : CompleteLattice α] {k : α}, CompleteLattice.IsCompactElement k → IsCoatomic ↑(Set.Iic k)
The theorem `CompleteLattice.Iic_coatomic_of_compact_element` states that in the context of a complete lattice of any type `α`, for a compact element `k` in that lattice, any element `b` which is less than `k` lies beneath a "maximal element below `k`". In other words, the interval from the bottom element to `k`, denoted as `[⊥, k]`, is coatomic. A set is coatomic if every element of it (except the supremum) is below some atom. Here, an atom is an element that is minimal: there is no other element between it and the bottom element. This theorem thus establishes a specific property concerning the structure and distribution of elements in the interval `[⊥, k]` for a compact element `k` in a complete lattice.
More concisely: In a complete lattice, for any compact element `k`, the interval `[⊥, k]` is coatomic, meaning every element in it (except `k`) is below some atom.
|
inf_sSup_eq_iSup_inf_sup_finset
theorem inf_sSup_eq_iSup_inf_sup_finset :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsCompactlyGenerated α] {a : α} {s : Set α},
a ⊓ sSup s = ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
This theorem states that for any type `α` that forms a complete lattice and is compactly generated, along with any element `a` of this type and any set `s` of elements of this type, the infimum of `a` and the supremum of `s` is equal to the supremum over all subsets `t` of `s` of the infimum of `a` and the supremum of `t` (with no modification made by the identity function). In more mathematical terms, we have $\inf(a, \sup s) = \bigvee \{ \inf(a, \sup t) \mid t \subseteq s \}$. This is equivalent to the upper continuity property of the type `α`.
More concisely: For any complete lattice `α` with compact generation, the infimum of an element `a` and the supremum of a set `s` equals the supremum over all subsets `t` of `s` of the infimum of `a` and the supremum of `t`.
|
DirectedOn.sSup_inf_eq
theorem DirectedOn.sSup_inf_eq :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsCompactlyGenerated α] {a : α} {s : Set α},
DirectedOn (fun x x_1 => x ≤ x_1) s → sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a
This theorem states that, for any type `α` that forms a complete lattice and is compactly generated, given an element `a` of `α` and a subset `s` of `α` that is directed (in the sense that for any two elements in the subset, there exists an element in the subset that is greater than or equal to both), the supremum of `s` intersected with `a` equals to the supremum of the set of all intersections of `a` with elements in `s`. This property sometimes leads to `α` being described as upper continuous.
More concisely: For any complete lattice `α` that is compactly generated, the supremum of the intersection of an element `a` in `α` with a directed set `s` subset of `α` equals the supremum of the set of intersections of `a` with elements in `s`.
|
complementedLattice_of_sSup_atoms_eq_top
theorem complementedLattice_of_sSup_atoms_eq_top :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsModularLattice α] [inst_2 : IsCompactlyGenerated α],
sSup {a | IsAtom a} = ⊤ → ComplementedLattice α
This theorem, referenced as Theorem 6.6 in a source denoted as [calugareanu], states that for any type `α` that forms a complete, modular and compactly generated lattice, if the supremum (least upper bound) of all its atoms (elements with no other element between them and the bottom element, that are not the bottom element themselves) equals the top element (`⊤`), then `α` is a complemented lattice. In simpler terms, if the greatest of all smallest meaningful pieces in this structure fills the entire structure, then every element in the structure has a "complement" or opposing piece.
More concisely: If a complete, modular and compactly generated lattice's supremum of atoms equals the top element, then every element has a complement.
|
CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le :
∀ (α : Type u_2) [inst : CompleteLattice α] (k : α),
CompleteLattice.IsCompactElement k ↔
∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
An element `k` in a complete lattice is compact if and only if for any directed set, if the supremum (`sSup`) of the set is greater than or equal to `k`, then there exists an element in the set that is greater than or equal to `k`. Put in another way, a compact element in a complete lattice is one where, if the set's supremum is at least as big as the element, then there is a point in the set where we already reached or exceeded the value of the compact element. This point is reached without the need for the entire set, and this captures the intuition behind the compactness of the element. The directedness of the set ensures that for any two elements in the set, there is a third element that is greater than or equal to both.
More concisely: A complete lattice element `k` is compact if and only if for every directed set with supremum greater than or equal to `k`, there exists an element in the set that is greater than or equal to `k`.
|
IsCompactlyGenerated.exists_sSup_eq
theorem IsCompactlyGenerated.exists_sSup_eq :
∀ {α : Type u_3} [inst : CompleteLattice α] [self : IsCompactlyGenerated α] (x : α),
∃ s, (∀ x ∈ s, CompleteLattice.IsCompactElement x) ∧ sSup s = x
This theorem states that in a compactly generated complete lattice, every element can be expressed as the supremum (`sSup`) of a set of compact elements. Specifically, for every element `x` in the lattice, there exists a set `s`, where every element in `s` is a compact element, and `x` is equal to the supremum of `s`. A compact element, in the context of a complete lattice, is an element `k` such that for any set with a supremum above `k`, there is a finite subset also with a supremum above `k`.
More concisely: In a compactly generated complete lattice, every element is the supremum of a set of compact elements.
|
WellFounded.isSupClosedCompact
theorem WellFounded.isSupClosedCompact :
∀ (α : Type u_2) [inst : CompleteLattice α],
(WellFounded fun x x_1 => x > x_1) → CompleteLattice.IsSupClosedCompact α
This theorem, which is an alias of the reverse direction of `CompleteLattice.isSupClosedCompact_iff_wellFounded`, states that for any type `α` that has a structure of a complete lattice, if there exists a well-founded relation where each element `x` is greater than the next element `x_1`, then `α` has the property of being sup-closed compact. In other words, if `α` is a complete lattice and has a descending chain condition (all strictly decreasing sequences are finite), then any non-empty subset of `α` that is closed under taking `sup` (supremum or least upper bound) contains its supremum.
More concisely: In a complete lattice with the descending chain condition, any non-empty sup-closed subset has a least upper bound (supremum).
|
complementedLattice_of_isAtomistic
theorem complementedLattice_of_isAtomistic :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsModularLattice α] [inst_2 : IsCompactlyGenerated α]
[inst_3 : IsAtomistic α], ComplementedLattice α
This theorem states that for any type `α` that has a structure of a complete lattice, a modular lattice, a compactly generated lattice, and an atomistic lattice, this type `α` also possesses a structure of a complemented lattice. This is a result known from Theorem 6.6 in the referenced document from Calugareanu. In other words, if a lattice is complete, modular, compactly generated, and atomistic, then it is guaranteed to have a complemented structure where every element has a complement.
More concisely: If a lattice is complete, modular, compactly generated, and atomistic, then it is complemented.
|
CompleteLattice.isSupFiniteCompact_iff_all_elements_compact
theorem CompleteLattice.isSupFiniteCompact_iff_all_elements_compact :
∀ (α : Type u_2) [inst : CompleteLattice α],
CompleteLattice.IsSupFiniteCompact α ↔ ∀ (k : α), CompleteLattice.IsCompactElement k
This theorem states that for any type `α` that forms a complete lattice, the property that the lattice is sup-finite-compact is equivalent to all elements `k` of type `α` being compact. In other words, a complete lattice has the compactness property (i.e., any subset has a finite subset with the same supremum) if and only if every element in the lattice is a compact element (i.e., for any set with supremum above this element, there exists a finite subset with the supremum also above this element).
More concisely: A complete lattice `α` is sup-finite-compact if and only if every element in `α` is compact.
|
DirectedOn.inf_sSup_eq
theorem DirectedOn.inf_sSup_eq :
∀ {α : Type u_2} [inst : CompleteLattice α] [inst_1 : IsCompactlyGenerated α] {a : α} {s : Set α},
DirectedOn (fun x x_1 => x ≤ x_1) s → a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
This theorem, referred to as `α` being upper continuous, states that for any type `α` that forms a Complete Lattice and is Compactly Generated, and for any element `a` of `α` and set `s` of `α`, if the set `s` is directed in the sense that for every pair of elements from `s`, there exists another element in `s` that is greater than or equal to both, then the infimum (greatest lower bound) of `a` and the supremum (least upper bound) of `s` is equal to the supremum of the set of all infimums of `a` and each element `b` in `s`. In LaTeX terms, if `s` is directed with respect to `≤`, then `a ∧ sup s = sup {a ∧ b | b ∈ s}`.
More concisely: For any complete lattice `α` that is compactly generated, if `s` is a directed set in `α` with respect to `≤`, then the infimum of any element `a` in `α` and the supremum of `s` are equal to the supremum of the set of all infimums of `a` and each element in `s`.
|