Mathlib Changelog
v4
Changelog
About
Github
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