OAI/Analysis/CircleDomains/Topology/AnchoredMeanCollars.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual nested collars for a finite marked point can simultaneously avoid the closed source anchor and the quotient point at infinity.

  1. theorem OAI.CircleDomainRigidity.exists_anchored_shrinking_weighted_collars line 13