Commit 2026-01-06 17:14 f53fc46f

View on Github →

refactor(EMetricSpace): rename EMetric.diam -> Metric.ediam (#33558) Also review names of the lemmas in this file, see deprecation warning for all the renames. Zulip thread: #mathlib4 > eball vs emetricBall vs EMetric.ball @ 💬

Estimated changes

modified theorem AffineIsometry.ediam_image
modified theorem AffineIsometry.ediam_range
modified theorem ediam_mul_le
modified theorem ediam_smul_le
modified theorem ediam_smul₀
modified theorem convexHull_ediam
modified theorem LinearIsometry.ediam_image
modified theorem LinearIsometry.ediam_range
modified theorem Real.volume_le_diam
modified theorem Real.volume_pi_le_diam_pow
deleted theorem EMetric.diam_ball
deleted theorem EMetric.diam_closedBall
deleted theorem EMetric.diam_empty
deleted theorem EMetric.diam_eq_sSup
deleted theorem EMetric.diam_eq_zero_iff
deleted theorem EMetric.diam_image_le_iff
deleted theorem EMetric.diam_insert
deleted theorem EMetric.diam_le
deleted theorem EMetric.diam_le_iff
deleted theorem EMetric.diam_mono
deleted theorem EMetric.diam_one
deleted theorem EMetric.diam_pair
deleted theorem EMetric.diam_pi_le_of_le
deleted theorem EMetric.diam_pos_iff'
deleted theorem EMetric.diam_pos_iff
deleted theorem EMetric.diam_singleton
deleted theorem EMetric.diam_subsingleton
deleted theorem EMetric.diam_triple
deleted theorem EMetric.diam_union'
deleted theorem EMetric.diam_union
added theorem Metric.ediam_eball_le
added theorem Metric.ediam_empty
added theorem Metric.ediam_eq_sSup
added theorem Metric.ediam_insert
added theorem Metric.ediam_le
added theorem Metric.ediam_le_iff
added theorem Metric.ediam_mono
added theorem Metric.ediam_one
added theorem Metric.ediam_pair
added theorem Metric.ediam_pos_iff'
added theorem Metric.ediam_pos_iff
added theorem Metric.ediam_singleton
added theorem Metric.ediam_triple
added theorem Metric.ediam_union_le
deleted theorem EMetric.diam_closure
added theorem Metric.ediam_closure
modified theorem Real.ediam_Icc
modified theorem Real.ediam_Ico
modified theorem Real.ediam_Ioc
modified theorem Real.ediam_Ioo
modified theorem Metric.dist_le_diam_of_mem'
modified theorem Metric.ediam_of_unbounded
modified theorem Dilation.diam_image
modified theorem Dilation.diam_range
modified theorem Dilation.ediam_image
modified theorem Dilation.ediam_range
modified theorem Isometry.ediam_image
modified theorem Isometry.ediam_range
modified theorem IsometryClass.ediam_image
modified theorem IsometryClass.ediam_range
modified theorem IsometryEquiv.ediam_image
modified theorem IsometryEquiv.ediam_univ
modified theorem Metric.ediam_thickening_le