OAI/Geometry/RCD/Transport/HyperbolicChord.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The hyperbolic comparison chord and its exact neighboring-point identity

  1. def OAI.RegularPointCoordinates.hyperbolicChord line 11
  2. theorem OAI.RegularPointCoordinates.hyperbolicChord_zero line 14
  3. theorem OAI.RegularPointCoordinates.hyperbolicChord_one line 18
  4. theorem OAI.RegularPointCoordinates.continuous_hyperbolicChord line 22
  5. theorem OAI.RegularPointCoordinates.hyperbolicChord_nonneg line 26
  6. theorem OAI.RegularPointCoordinates.hyperbolicChord_neighbor_sum line 32