mathlib

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

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`