OAI/Geometry/RCD/Transport/ReflectedMidpointDiameter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The elementary diameter bound in the isodiametric argument

  1. theorem OAI.RegularPointCoordinates.reflected_midpoints_subset_closedBall line 13

    Source documentation

    Midpoints of a set and its reflection lie in the ball whose radius is half the original diameter.

    theorem reflected_midpoints_subset_closedBall {n : ℕ} {A : Set (Euclidean n)}
    (hA : Bornology.IsBounded A) :
    midpointSet A (Neg.neg '' A) ⊆ closedBall 0 (diam A/2) := by
…

    Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.midpointSet