OAI/Analysis/CircleDomains/Topology/ClosedTimeCounts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable multiplicity in a closed time relation. This allows visits to be restricted to a tagged path's residual times and to a closed test interval.

  1. def OAI.CircleDomainRigidity.timeCount line 17
  2. def OAI.CircleDomainRigidity.timeWitnessSet line 20
  3. def OAI.CircleDomainRigidity.separatedTimeWitnessSet line 23
  4. theorem OAI.CircleDomainRigidity.timeCount_eq_iSup line 26
  5. theorem OAI.CircleDomainRigidity.timeWitnessSet_eq_iUnion line 56
  6. theorem OAI.CircleDomainRigidity.isClosed_separatedTimeWitnessSet line 75
  7. theorem OAI.CircleDomainRigidity.measurable_timeCount line 95