OAI/Analysis/CircleDomains/Topology/RegularPieceOpenOrbit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Each orbit is open in its actual regular level, as witnessed by the nonzero derivative of its local level coordinate.

  1. def OAI.CircleDomainRigidity.CompactRegularPieceFlow.levelTrajectory line 12
  2. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.continuous_levelTrajectory line 16
  3. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.isOpenMap_levelTrajectory line 20
  4. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.isOpen_range_levelTrajectory line 49