OAI/Analysis/CircleDomains/Topology/RationalIntervalControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounds on rational intervals extend to all compact interior intervals by continuity from above. No pointwise continuity of a density is required.

  1. theorem OAI.CircleDomainRigidity.le_measure_Icc_of_rational_enclosures line 16