Results about compactness properties for intervals in complete lattices

theorem Set.Iic.isCompactElement {α : Type u_2} [CompleteLattice α] {a : α} {b : ↑(Set.Iic a)} (h : CompleteLattice.IsCompactElement ↑b) : CompleteLattice.IsCompactElement b

instance Set.Iic.instIsCompactlyGenerated {α : Type u_2} [CompleteLattice α] [IsCompactlyGenerated α] {a : α} : IsCompactlyGenerated ↑(Set.Iic a)

Equations

• ⋯ = ⋯

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 = ⊤) : ComplementedLattice α