OAI/Analysis/CircleDomains/Modulus/ShrinkingWeightedCollars.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The chosen collar closures and all their joining levels shrink to the actual quotient point.

  1. theorem OAI.CircleDomainRigidity.exists_shrinking_weighted_collars line 18