OAI/Analysis/CircleDomains/Topology/RegularLevelCompactOrbit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Orbits form clopen components of a compact regular level. Their compactness forces a return for the complete nonstationary flow.

  1. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.mem_range_levelTrajectory line 13
  2. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.level_orbits_eq_or_disjoint line 22
  3. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.isClopen_range_levelTrajectory line 36
  4. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.compact_range_levelTrajectory line 50
  5. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.not_injective_trajectory line 57