Documentation

Mathlib.Order.CompactlyGenerated.Intervals

Results about compactness properties for intervals in complete lattices #

theorem complementedLattice_of_complementedLattice_Iic {ι : Type u_1} {α : Type u_2} [CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] {s : Set ι} {f : ια} (h : is, ComplementedLattice (Set.Iic (f i))) (h' : ⨆ i ∈ s, f i = ) :