OAI/Analysis/CircleDomains/Modulus/WeightedIntermediateCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An actual weighted collar between an inner physical Jordan disk and an outer quotient disk. Its entire joining level stays in the intervening annulus.

  1. theorem OAI.CircleDomainRigidity.exists_weighted_intermediate_collar line 16