OAI/Analysis/CircleDomains/Selection/RegularPieceLeastPeriod.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.CompactRegularPieceFlow.returnSubgroup line 13
  2. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.returnSubgroup_closed line 25
  3. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.returnSubgroup_not_dense line 30
  4. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.exists_least_positive_period line 42
  5. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.injOn_fundamental_interval line 58
  6. lemma OAI.CircleDomainRigidity.CompactRegularPieceFlow.range_levelTrajectory_eq_component line 72