Theorem AffineIsometry.ediam_range

Modification history

2026-01-06 17:14
Mathlib/Analysis/Normed/Affine/Isometry.lean
refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558) …
Modified AffineIsometry.ediam_rangeView on Github →
2023-05-19 18:00
Mathlib/Analysis/NormedSpace/AffineIsometry.lean
feat: port Analysis.NormedSpace.AffineIsometry (#3651)
Added AffineIsometry.ediam_rangeView on Github →