OAI/Geometry/RCD/Transport/PathReversal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Time reversal and final-interval agreement

  1. theorem OAI.RegularPointCoordinates.timeSegment_one_zero_coe line 12
  2. theorem OAI.RegularPointCoordinates.timeSegment_reverse_reverse line 15
  3. theorem OAI.RegularPointCoordinates.subpath_reverse_reverse line 20
  4. theorem OAI.RegularPointCoordinates.subpath_reverse_injective line 25
  5. theorem OAI.RegularPointCoordinates.reversed_pair_agreement line 30