OAI/Analysis/CircleDomains/Selection/AffineResidualExposure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Under affine restriction, old residual times remain residual. Discarded constant tags expose only countably many image points in the open piece.

  1. theorem OAI.CircleDomainRigidity.affine_old_residual_subset line 17
  2. theorem OAI.CircleDomainRigidity.affine_discarded_image_countable line 37
  3. theorem OAI.CircleDomainRigidity.affine_exposed_image_countable line 47