Commit 2024-06-10 10:01 8ecf3628

View on Github →

chore: move totallyBounded_Ixx lemmas up a bit (#13631)

Estimated changes

Modified Mathlib/Analysis/Convex/Extrema.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

added theorem totallyBounded_Icc

added theorem totallyBounded_Ico

added theorem totallyBounded_Ioc

added theorem totallyBounded_Ioo

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

deleted theorem totallyBounded_Icc

deleted theorem totallyBounded_Ico

deleted theorem totallyBounded_Ioc

deleted theorem totallyBounded_Ioo