Theorem complete_lattice.compactly_generated_of_well_founded
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.compactly_generated_of_well_foundedView on Github →