OAI/Analysis/CircleDomains/Topology/RegularLevelOpenOrbit.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.CompactRegularLevelFlow.levelTrajectory line 12
  2. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.continuous_levelTrajectory line 16
  3. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.isOpenMap_levelTrajectory line 20
  4. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.isOpen_range_levelTrajectory line 48