Documentation

Mathlib.Order.CompactlyGenerated.Basic

Compactness properties for complete lattices #

For complete lattices, there are numerous equivalent ways to express the fact that the relation > is well-founded. In this file we define three especially-useful characterisations and provide proofs that they are indeed equivalent to well-foundedness.

Main definitions #

Main results #

The main result is that the following four conditions are equivalent for a complete lattice:

well_founded (>)
CompleteLattice.IsSupClosedCompact
CompleteLattice.IsSupFiniteCompact
∀ k, CompleteLattice.IsCompactElement k

This is demonstrated by means of the following four lemmas:

We also show well-founded lattices are compactly generated (CompleteLattice.isCompactlyGenerated_of_wellFounded).

References #

[G. Călugăreanu, Lattice Concepts of Module Theory][calugareanu]

Tags #

complete lattice, well-founded, compact

def CompleteLattice.IsSupClosedCompact (α : Type u_2) [CompleteLattice α] :

A compactness property for a complete lattice is that any sup-closed non-empty subset contains its sSup.

Equations

CompleteLattice.IsSupClosedCompact α = ∀ (s : Set α), s.Nonempty → SupClosed s → sSup s ∈ s

def CompleteLattice.IsSupFiniteCompact (α : Type u_2) [CompleteLattice α] :

A compactness property for a complete lattice is that any subset has a finite subset with the same sSup.

Equations

CompleteLattice.IsSupFiniteCompact α = ∀ (s : Set α), ∃ (t : Finset α), ↑t ⊆ s ∧ sSup s = t.sup id

def CompleteLattice.IsCompactElement {α : Type u_3} [CompleteLattice α] (k : α) :

An element k of a complete lattice is said to be compact if any set with sSup above k has a finite subset with sSup above k. Such an element is also called "finite" or "S-compact".

Equations

CompleteLattice.IsCompactElement k = ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), ↑t ⊆ s ∧ k ≤ t.sup id

theorem CompleteLattice.isCompactElement_iff {α : Type u} [CompleteLattice α] (k : α) :

IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s

theorem CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le (α : Type u_2) [CompleteLattice α] (k : α) :

IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

An element k is compact if and only if any directed set with sSup above k already got above k at some point in the set.

theorem CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (α : Type u_2) [CompleteLattice α] {k : α} (hk : IsCompactElement k) {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i) :

∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

theorem CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt {α : Type u_3} [CompleteLattice α] {k : α} (hk : IsCompactElement k) {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hbelow : ∀ x ∈ s, x < k) :

sSup s < k

A compact element k has the property that any directed set lying strictly below k has its sSup strictly below k.

theorem CompleteLattice.isCompactElement_finsetSup {α : Type u_3} {β : Type u_4} [CompleteLattice α] {f : β → α} (s : Finset β) (h : ∀ x ∈ s, IsCompactElement (f x)) :

IsCompactElement (s.sup f)

theorem CompleteLattice.WellFoundedGT.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] [WellFoundedGT α] :

IsSupFiniteCompact α

theorem CompleteLattice.IsSupFiniteCompact.isSupClosedCompact (α : Type u_2) [CompleteLattice α] (h : IsSupFiniteCompact α) :

IsSupClosedCompact α

theorem CompleteLattice.IsSupClosedCompact.wellFoundedGT (α : Type u_2) [CompleteLattice α] (h : IsSupClosedCompact α) :

WellFoundedGT α

theorem CompleteLattice.isSupFiniteCompact_iff_all_elements_compact (α : Type u_2) [CompleteLattice α] :

IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

theorem CompleteLattice.wellFoundedGT_characterisations (α : Type u_2) [CompleteLattice α] :

[WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

theorem CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact (α : Type u_2) [CompleteLattice α] :

WellFoundedGT α ↔ IsSupFiniteCompact α

theorem CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact (α : Type u_2) [CompleteLattice α] :

IsSupFiniteCompact α ↔ IsSupClosedCompact α

theorem CompleteLattice.isSupClosedCompact_iff_wellFoundedGT (α : Type u_2) [CompleteLattice α] :

IsSupClosedCompact α ↔ WellFoundedGT α

theorem CompleteLattice.IsSupFiniteCompact.wellFoundedGT (α : Type u_2) [CompleteLattice α] :

IsSupFiniteCompact α → WellFoundedGT α

Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact.

theorem CompleteLattice.IsSupClosedCompact.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] :

IsSupClosedCompact α → IsSupFiniteCompact α

Alias of the reverse direction of CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact.

theorem CompleteLattice.WellFoundedGT.isSupClosedCompact (α : Type u_2) [CompleteLattice α] :

WellFoundedGT α → IsSupClosedCompact α

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT.

theorem WellFoundedGT.finite_of_sSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) :

@[deprecated WellFoundedGT.finite_of_sSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedGT.finite_of_setIndependent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) :

Alias of WellFoundedGT.finite_of_sSupIndep.

theorem WellFoundedGT.finite_ne_bot_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) :

{i : ι | t i ≠ ⊥}.Finite

@[deprecated WellFoundedGT.finite_ne_bot_of_iSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) :

{i : ι | t i ≠ ⊥}.Finite

Alias of WellFoundedGT.finite_ne_bot_of_iSupIndep.

theorem WellFoundedGT.finite_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

@[deprecated WellFoundedGT.finite_of_iSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedGT.finite_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

Alias of WellFoundedGT.finite_of_iSupIndep.

theorem WellFoundedLT.finite_of_sSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {s : Set α} (hs : sSupIndep s) :

@[deprecated WellFoundedLT.finite_of_sSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedLT.finite_of_setIndependent {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {s : Set α} (hs : sSupIndep s) :

Alias of WellFoundedLT.finite_of_sSupIndep.

theorem WellFoundedLT.finite_ne_bot_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) :

{i : ι | t i ≠ ⊥}.Finite

@[deprecated WellFoundedLT.finite_ne_bot_of_iSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedLT.finite_ne_bot_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) :

{i : ι | t i ≠ ⊥}.Finite

Alias of WellFoundedLT.finite_ne_bot_of_iSupIndep.

theorem WellFoundedLT.finite_of_iSupIndep {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

@[deprecated WellFoundedLT.finite_of_iSupIndep (since := "2024-11-24")]

theorem CompleteLattice.WellFoundedLT.finite_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedLT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

Alias of WellFoundedLT.finite_of_iSupIndep.

class IsCompactlyGenerated (α : Type u_3) [CompleteLattice α] :

A complete lattice is said to be compactly generated if any element is the sSup of compact elements.

exists_sSup_eq (x : α) : ∃ (s : Set α), (∀ x ∈ s, CompleteLattice.IsCompactElement x) ∧ sSup s = x
In a compactly generated complete lattice, every element is the sSup of some set of compact elements.

Instances

@[simp]

theorem sSup_compact_le_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] (b : α) :

sSup {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b

@[simp]

theorem sSup_compact_eq_top {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] :

sSup {a : α | CompleteLattice.IsCompactElement a} = ⊤

theorem le_iff_compact_le_imp {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a b : α} :

a ≤ b ↔ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b

theorem DirectedOn.inf_sSup_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) :

a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

This property is sometimes referred to as α being upper continuous.

theorem DirectedOn.sSup_inf_eq {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) :

sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

This property is sometimes referred to as α being upper continuous.

theorem Directed.inf_iSup_eq {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) :

a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i

theorem Directed.iSup_inf_eq {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) :

(⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a

theorem DirectedOn.disjoint_sSup_right {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) :

Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b

theorem DirectedOn.disjoint_sSup_left {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) :

Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a

theorem Directed.disjoint_iSup_right {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) :

Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)

theorem Directed.disjoint_iSup_left {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α} (h : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) :

Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a

theorem inf_sSup_eq_iSup_inf_sup_finset {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α} :

a ⊓ sSup s = ⨆ (t : Finset α), ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

This property is equivalent to α being upper continuous.

theorem sSupIndep_iff_finite {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set α} :

sSupIndep s ↔ ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t

@[deprecated sSupIndep_iff_finite (since := "2024-11-24")]

theorem CompleteLattice.setIndependent_iff_finite {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set α} :

sSupIndep s ↔ ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t

Alias of sSupIndep_iff_finite.

theorem iSupIndep_iff_supIndep_of_injOn {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α} (hf : Set.InjOn f {i : ι | f i ≠ ⊥}) :

iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

@[deprecated iSupIndep_iff_supIndep_of_injOn (since := "2024-11-24")]

theorem CompleteLattice.independent_iff_supIndep_of_injOn {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} {f : ι → α} (hf : Set.InjOn f {i : ι | f i ≠ ⊥}) :

iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Alias of iSupIndep_iff_supIndep_of_injOn.

theorem sSupIndep_iUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : η → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ (i : η), sSupIndep (s i)) :

sSupIndep (⋃ (i : η), s i)

@[deprecated sSupIndep_iUnion_of_directed (since := "2024-11-24")]

theorem CompleteLattice.setIndependent_iUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : η → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ (i : η), sSupIndep (s i)) :

sSupIndep (⋃ (i : η), s i)

Alias of sSupIndep_iUnion_of_directed.

theorem iSupIndep_sUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set (Set α)} (hs : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ a ∈ s, sSupIndep a) :

sSupIndep (⋃₀ s)

@[deprecated iSupIndep_sUnion_of_directed (since := "2024-11-24")]

theorem CompleteLattice.independent_sUnion_of_directed {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {s : Set (Set α)} (hs : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (h : ∀ a ∈ s, sSupIndep a) :

sSupIndep (⋃₀ s)

Alias of iSupIndep_sUnion_of_directed.

theorem CompleteLattice.isCompactlyGenerated_of_wellFoundedGT {α : Type u_2} [CompleteLattice α] [h : WellFoundedGT α] :

IsCompactlyGenerated α

@[deprecated CompleteLattice.WellFoundedGT.isSupFiniteCompact (since := "2024-10-07")]

theorem CompleteLattice.WellFounded.isSupFiniteCompact (α : Type u_2) [CompleteLattice α] [WellFoundedGT α] :

IsSupFiniteCompact α

Alias of CompleteLattice.WellFoundedGT.isSupFiniteCompact.

@[deprecated CompleteLattice.IsSupClosedCompact.wellFoundedGT (since := "2024-10-07")]

theorem CompleteLattice.IsSupClosedCompact.wellFounded (α : Type u_2) [CompleteLattice α] (h : IsSupClosedCompact α) :

WellFoundedGT α

Alias of CompleteLattice.IsSupClosedCompact.wellFoundedGT.

@[deprecated CompleteLattice.wellFoundedGT_characterisations (since := "2024-10-07")]

theorem CompleteLattice.wellFounded_characterisations (α : Type u_2) [CompleteLattice α] :

[WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Alias of CompleteLattice.wellFoundedGT_characterisations.

@[deprecated CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact (since := "2024-10-07")]

theorem CompleteLattice.wellFounded_iff_isSupFiniteCompact (α : Type u_2) [CompleteLattice α] :

WellFoundedGT α ↔ IsSupFiniteCompact α

Alias of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact.

@[deprecated CompleteLattice.isSupClosedCompact_iff_wellFoundedGT (since := "2024-10-07")]

theorem CompleteLattice.isSupClosedCompact_iff_wellFounded (α : Type u_2) [CompleteLattice α] :

IsSupClosedCompact α ↔ WellFoundedGT α

Alias of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT.

@[deprecated CompleteLattice.IsSupFiniteCompact.wellFoundedGT (since := "2024-10-07")]

theorem CompleteLattice.IsSupFiniteCompact.wellFounded (α : Type u_2) [CompleteLattice α] :

IsSupFiniteCompact α → WellFoundedGT α

Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact.

Alias of the reverse direction of CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact.

@[deprecated CompleteLattice.WellFoundedGT.isSupClosedCompact (since := "2024-10-07")]

theorem WellFounded.isSupClosedCompact (α : Type u_2) [CompleteLattice α] :

WellFoundedGT α → CompleteLattice.IsSupClosedCompact α

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT.

Alias of the reverse direction of CompleteLattice.isSupClosedCompact_iff_wellFoundedGT.

@[deprecated WellFoundedGT.finite_of_sSupIndep (since := "2024-10-07")]

theorem CompleteLattice.WellFounded.finite_of_setIndependent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {s : Set α} (hs : sSupIndep s) :

Alias of WellFoundedGT.finite_of_sSupIndep.

@[deprecated WellFoundedGT.finite_ne_bot_of_iSupIndep (since := "2024-10-07")]

theorem CompleteLattice.WellFounded.finite_ne_bot_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) :

{i : ι | t i ≠ ⊥}.Finite

Alias of WellFoundedGT.finite_ne_bot_of_iSupIndep.

@[deprecated WellFoundedGT.finite_of_iSupIndep (since := "2024-10-07")]

theorem CompleteLattice.WellFounded.finite_of_independent {α : Type u_2} [CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

Alias of WellFoundedGT.finite_of_iSupIndep.

@[deprecated CompleteLattice.isCompactlyGenerated_of_wellFoundedGT (since := "2024-10-07")]

theorem CompleteLattice.isCompactlyGenerated_of_wellFounded {α : Type u_2} [CompleteLattice α] [h : WellFoundedGT α] :

IsCompactlyGenerated α

Alias of CompleteLattice.isCompactlyGenerated_of_wellFoundedGT.

theorem CompleteLattice.Iic_coatomic_of_compact_element {α : Type u_2} [CompleteLattice α] {k : α} (h : IsCompactElement k) :

IsCoatomic ↑(Set.Iic k)

A compact element k has the property that any b < k lies below a "maximal element below k", which is to say [⊥, k] is coatomic.

theorem CompleteLattice.coatomic_of_top_compact {α : Type u_2} [CompleteLattice α] (h : IsCompactElement ⊤) :

@[instance 100]

instance isAtomic_of_complementedLattice {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α] :

@[instance 100]

instance isAtomistic_of_complementedLattice {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α] :

See [Lemma 5.1][calugareanu].

Now we will prove that a compactly generated modular atomistic lattice is a complemented lattice. Most explicitly, every element is the complement of a supremum of indepedendent atoms.

theorem exists_sSupIndep_isCompl_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) (b : α) :

∃ (s : Set α), sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

In an atomic lattice, every element b has a complement of the form sSup s, where each element of s is an atom. See also complementedLattice_of_sSup_atoms_eq_top.

@[deprecated exists_sSupIndep_isCompl_sSup_atoms (since := "2024-11-24")]

theorem exists_setIndependent_isCompl_sSup_atoms {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) (b : α) :

∃ (s : Set α), sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Alias of exists_sSupIndep_isCompl_sSup_atoms.

In an atomic lattice, every element b has a complement of the form sSup s, where each element of s is an atom. See also complementedLattice_of_sSup_atoms_eq_top.

theorem exists_sSupIndep_of_sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) :

∃ (s : Set α), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

@[deprecated exists_sSupIndep_of_sSup_atoms_eq_top (since := "2024-11-24")]

theorem exists_setIndependent_of_sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) :

∃ (s : Set α), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Alias of exists_sSupIndep_of_sSup_atoms_eq_top.

theorem complementedLattice_of_sSup_atoms_eq_top {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (h : sSup {a : α | IsAtom a} = ⊤) :

ComplementedLattice α

See [Theorem 6.6][calugareanu].

theorem complementedLattice_of_isAtomistic {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [IsAtomistic α] :

ComplementedLattice α

See [Theorem 6.6][calugareanu].

theorem complementedLattice_iff_isAtomistic {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] :

ComplementedLattice α ↔ IsAtomistic α