Theorem complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact
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) …
Modified complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compactView on Github →