OAI/Geometry/RCD/Transport/LastPathAgreement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The last meeting of two paths before a fixed time

The last meeting time is measurable. After it, the paths remain distinct up to the fixed time. Adding time zero makes the definition total; on pairs with a common initial point it is an actual meeting time.

  1. def OAI.RegularPointCoordinates.pathMeetingTimes line 18
  2. def OAI.RegularPointCoordinates.lastPathAgreement line 21
  3. theorem OAI.RegularPointCoordinates.lastPathAgreement_isGreatest line 24
  4. theorem OAI.RegularPointCoordinates.lastPathAgreement_le line 30
  5. theorem OAI.RegularPointCoordinates.lastPathAgreement_eq line 38
  6. theorem OAI.RegularPointCoordinates.ne_after_lastPathAgreement line 45
  7. theorem OAI.RegularPointCoordinates.measurable_lastPathAgreement line 54