OAI/Geometry/RCD/Transport/ClosedMidpointConvex.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Closed midpoint sets and the local distance-coordinate image

  1. theorem OAI.RegularPointCoordinates.closed_midpoints_fill_interval line 14
  2. theorem OAI.RegularPointCoordinates.isClosed_convex_of_midpoints line 35