OAI/Geometry/RCD/Sobolev/WeightedMatchedJoin.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Matched paths joined at an arbitrary interior time

  1. def OAI.RegularPointCoordinates.weightedLeftTime line 13
  2. def OAI.RegularPointCoordinates.weightedRightTime line 16
  3. theorem OAI.RegularPointCoordinates.weightedLeftTime_coe line 19
  4. theorem OAI.RegularPointCoordinates.weightedRightTime_coe line 24
  5. theorem OAI.RegularPointCoordinates.continuous_weightedLeftTime line 30
  6. theorem OAI.RegularPointCoordinates.continuous_weightedRightTime line 33
  7. def OAI.RegularPointCoordinates.weightedJoin line 36
  8. theorem OAI.RegularPointCoordinates.weightedJoin_continuous line 54
  9. theorem OAI.RegularPointCoordinates.weightedJoin_left line 78
  10. theorem OAI.RegularPointCoordinates.weightedJoin_right line 82
  11. theorem OAI.RegularPointCoordinates.weightedJoin_zero line 97
  12. theorem OAI.RegularPointCoordinates.weightedJoin_one line 105
  13. theorem OAI.RegularPointCoordinates.weightedJoin_split line 114
  14. theorem OAI.RegularPointCoordinates.weightedJoin_isGeodesic line 122
  15. theorem OAI.RegularPointCoordinates.weightedJoin_law_left line 172
  16. theorem OAI.RegularPointCoordinates.weightedJoin_law_right line 182
  17. theorem OAI.RegularPointCoordinates.weightedJoin_law_zero line 192
  18. theorem OAI.RegularPointCoordinates.weightedJoin_law_one line 199
  19. theorem OAI.RegularPointCoordinates.weightedJoin_law_split line 206