OAI/Geometry/RCD/Transport/LocalMidpointFeatures.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Squared-distance coordinates of the local midpoint geometry

  1. abbrev OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature line 13
  2. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.in_large line 16
  3. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature_injective line 20
  4. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature_continuous line 34
  5. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature_mid line 41
  6. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature_center line 52
  7. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.feature_half line 56
  8. theorem OAI.RegularPointCoordinates.LocalQuadraticMidpointGeometry.mid_medial line 60