Theorem convexHull_ediam

Modification history

2026-01-06 17:14

Mathlib/Analysis/Normed/Module/Convex.lean

refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558) …

Modified convexHull_ediam View on Github →

2023-04-24 22:52

Mathlib/Analysis/Convex/Normed.lean

feat: port Analysis.Convex.Normed (#3626)

Added convexHull_ediam View on Github →