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