OAI/Geometry/RCD/Coordinates/CenteredBoundedFrame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded global representatives of centered local harmonic frames

  1. theorem OAI.RegularPointCoordinates.localGamma_pair_constant_shift line 16
  2. theorem OAI.RegularPointCoordinates.centered_bounded_frame line 29