OAI/Analysis/CircleDomains/Topology/RationalTimeIntervals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Every open time interval is the directed union of the rational closed intervals contained in it. This passes the coded constraints to open pieces.

  1. theorem OAI.CircleDomainRigidity.rationalTime_toTime_monotone line 15
  2. theorem OAI.CircleDomainRigidity.rationalTime_toTime_min line 20
  3. theorem OAI.CircleDomainRigidity.rationalTime_toTime_max line 26
  4. def OAI.CircleDomainRigidity.InnerRationalInterval line 32
  5. def OAI.CircleDomainRigidity.innerRationalInterval line 35
  6. theorem OAI.CircleDomainRigidity.innerRationalInterval_directed line 38
  7. theorem OAI.CircleDomainRigidity.iUnion_innerRationalInterval line 51