OAI/Analysis/CircleDomains/Topology/ResidualOpenIntervals.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The coded residual-contact inequalities extend from rational closed intervals to every open time interval, by directed continuity from below.

  1. theorem OAI.CircleDomainRigidity.residualIncidence_time_mono line 18
  2. theorem OAI.CircleDomainRigidity.residualToll_time_mono line 26
  3. theorem OAI.CircleDomainRigidity.residualIncidence_time_iUnion line 38
  4. theorem OAI.CircleDomainRigidity.residualIncidenceBound_directed_union line 51
  5. theorem OAI.CircleDomainRigidity.residualIncidenceBound_open_of_rational line 65
  6. theorem OAI.CircleDomainRigidity.residualConstraintFamily_open line 74