Results about compactness properties for intervals in complete lattices #
theorem
Set.Iic.isCompactElement
{α : Type u_2}
[CompleteLattice α]
{a : α}
{b : ↑(Iic a)}
(h : IsCompactElement ↑b)
:
instance
Set.Iic.instIsCompactlyGenerated
{α : Type u_2}
[CompleteLattice α]
[IsCompactlyGenerated α]
{a : α}
:
IsCompactlyGenerated ↑(Iic a)
theorem
complementedLattice_of_complementedLattice_Iic
{ι : Type u_1}
{α : Type u_2}
[CompleteLattice α]
[IsModularLattice α]
[IsCompactlyGenerated α]
{s : Set ι}
{f : ι → α}
(h : ∀ i ∈ s, ComplementedLattice ↑(Set.Iic (f i)))
(h' : ⨆ i ∈ s, f i = ⊤)
: