Commit 2023-11-01 15:16 5a2b014d

View on Github →

chore: forward-port leanprover-community/mathlib#19028 (#8083) This was "feat(topology/metric_space): diameter of pointwise zero and addition"

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

added theorem Bornology.IsBounded.of_mul

added theorem ediam_mul_le

Modified Mathlib/Topology/Bornology/Basic.lean

added theorem Bornology.nonempty_of_not_isBounded

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem EMetric.diam_one

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

added theorem AntilipschitzWith.isBounded_of_image2_left

added theorem AntilipschitzWith.isBounded_of_image2_right

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

added theorem Metric.diam_one

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

added theorem LipschitzOnWith.ediam_image2_le

added theorem LipschitzOnWith.isBounded_image2