OAI/Analysis/CircleDomains/Modulus/CompactContinuousImageModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A continuous presentation inside a compact family avoiding zero has a compact subfamily retaining every prescribed strict modulus threshold.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_zero_of_isEmpty line 13
  2. lemma OAI.CircleDomainRigidity.exists_compact_subfamily_of_continuous_image line 22