OAI/Analysis/CircleDomains/Modulus/ModulusFiniteBallCut.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite collection of small closed balls retains a prescribed strict modulus threshold in a separable metric presentation.

  1. lemma OAI.CircleDomainRigidity.exists_modulus_finite_closedBall_cut line 13