Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_compact.elim_directed_family_closed

Modification history

2023-06-21 18:29
src/topology/subset_properties.lean
feat(topology/algebra/order/compact): remove conditional completeness assumption in `is_compact.exists_forall_le` (#18991)
Added is_compact.elim_directed_family_closedView on Github →