OAI/Analysis/CircleDomains/Selection/RegularLevelLeastPeriod.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The closed return subgroup of a nonstationary compact regular-level trajectory has a least positive element. This is its fundamental period.

  1. def OAI.CircleDomainRigidity.CompactRegularLevelFlow.returnSubgroup line 13
  2. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.returnSubgroup_closed line 25
  3. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.returnSubgroup_not_dense line 30
  4. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.exists_least_positive_period line 42
  5. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.injOn_fundamental_interval line 58
  6. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.range_levelTrajectory_eq_component line 72