OAI/Analysis/CircleDomains/Modulus/NestedWeightedCollars.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strictly nested actual weighted collars, chosen inside any prescribed sequence of quotient neighborhoods.

  1. theorem OAI.CircleDomainRigidity.exists_nested_weighted_collars line 15