OAI/Geometry/RCD/Transport/PointedMidpointSets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Midpoints of arbitrary compact target sets

  1. def OAI.RegularPointCoordinates.midpointSet line 13

    Source documentation

    The exact midpoint image, without a convexity assumption.

    def midpointSet {n : ℕ} (A B : Set (Euclidean n)) : Set (Euclidean n) :=
…

    Mentions: OAI.RegularPointCoordinates.Euclidean

  2. theorem OAI.RegularPointCoordinates.isCompact_midpointSet line 16
  3. theorem OAI.RegularPointCoordinates.pointed_midpoint_sets_within line 20