OAI/Geometry/RCD/Transport/MeetingSpliceGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Splicing arbitrary contacting geodesics at an interior meeting

  1. theorem OAI.RegularPointCoordinates.splicePathAt_isGeodesic_of_cross_length line 14
  2. theorem OAI.RegularPointCoordinates.contacting_splice_isGeodesic line 51