Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-21 18:29 3efd324a

View on Github →

feat(topology/algebra/order/compact): remove conditional completeness assumption in is_compact.exists_forall_le (#18991)

Estimated changes

Modified src/order/directed.lean

added theorem is_total.directed

Modified src/topology/algebra/order/compact.lean

added theorem continuous.bdd_above_range_of_has_compact_mul_support

added theorem continuous.bdd_below_range_of_has_compact_mul_support

added theorem is_compact.bdd_above

added theorem is_compact.bdd_above_image

added theorem is_compact.bdd_below

added theorem is_compact.bdd_below_image

Modified src/topology/order/basic.lean

deleted theorem continuous.bdd_above_range_of_has_compact_mul_support

deleted theorem continuous.bdd_below_range_of_has_compact_mul_support

deleted theorem is_compact.bdd_above

deleted theorem is_compact.bdd_above_image

deleted theorem is_compact.bdd_below

deleted theorem is_compact.bdd_below_image

Modified src/topology/subset_properties.lean

added theorem is_compact.elim_directed_family_closed