theorem IsoperimetricEuclidean.isoperimetric_euclidean {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n))) (hA : MeasurableSet A) (c : EuclideanSpace ℝ (Fin n)) (r : ℝ) (hvol : MeasureTheory.volume A = MeasureTheory.volume (Metric.closedBall c r)) (t : ℝ) (ht : 0 ≤ t) : MeasureTheory.volume (Metric.cthickening t (Metric.closedBall c r)) ≤ MeasureTheory.volume (Metric.cthickening t A)

Euclidean isoperimetric inequality (Theorem 9.4.1). Among all measurable subsets of $\mathbb{R}^n$ with a fixed Lebesgue volume, the closed ball minimizes the volume of the $t$-thickening: if $\operatorname{vol}(A) = \operatorname{vol}(B(c, r))$, then for every $t \ge 0$, $\operatorname{vol}(B(c, r)_t) \le \operatorname{vol}(A_t)$.