OAI/Analysis/CircleDomains/Selection/NarrowedResidualBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The countable image exposed by discarding constant tag pieces is paid by singleton bounds. This preserves all incidence constraints on the retained open interval, even if the new residual set has uncountably many times.

  1. theorem OAI.CircleDomainRigidity.timeIncidence_bound_of_countable_difference line 18
  2. theorem OAI.CircleDomainRigidity.residualIncidenceBound_narrow line 34
  3. theorem OAI.CircleDomainRigidity.residualImage_narrow_null line 51