Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-10-09 14:37
c8f30551
View on Github →
feat(topology/metric_space): diameter of pointwise zero and addition (
#19028
)
Estimated changes
Modified
src/analysis/normed/group/pointwise.lean
added
theorem
ediam_mul_le
added
theorem
metric.bounded.of_mul
Modified
src/topology/metric_space/antilipschitz.lean
added
theorem
antilipschitz_with.bounded_of_image2_left
added
theorem
antilipschitz_with.bounded_of_image2_right
Modified
src/topology/metric_space/basic.lean
added
theorem
metric.diam_one
added
theorem
metric.nonempty_of_unbounded
Modified
src/topology/metric_space/emetric_space.lean
added
theorem
emetric.diam_one
Modified
src/topology/metric_space/lipschitz.lean
added
theorem
lipschitz_on_with.bounded_image2
added
theorem
lipschitz_on_with.ediam_image2_le