Theorem complete_lattice.is_compact_element_iff_le_of_directed_Sup_le
Modification history
2021-01-24 20:25
src/order/compactly_generated.lean
feat(order/complete_well_founded, data/finset/lattice): introduce compact elements of a complete lattice and characterize compact lattices as those with all elements compact (#5825) …
Added complete_lattice.is_compact_element_iff_le_of_directed_Sup_leView on Github →