Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 13:45 3fde0827

View on Github →

refactor(topology/algebra/order): reorganize, simplify proofs (#13716)

  • Prove has_compact_mul_support.is_compact_range
  • Simplify the proof of continuous.exists_forall_le_of_has_compact_mul_support and continuous.bdd_below_range_of_has_compact_mul_support using has_compact_mul_support.is_compact_range.
  • Reorder topology.algebra.order.basic so that is_compact.bdd_below and friends are together with all results about order_closed_topology.
  • Move continuous.bdd_below_range_of_has_compact_mul_support (and dual) to topology.algebra.order.basic

Estimated changes

modified theorem is_compact.bdd_above
modified theorem is_compact.bdd_above_image
modified theorem is_compact.bdd_below
modified theorem is_compact.bdd_below_image