OAI/Analysis/CircleDomains/Topology/ControlledComponentShrink.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quantitative shrinking stage for the actual component decomposition. The old component diameter is used only to keep the forward movement small. The quotient observation is constant on components and controls the inverse movement. The new component diameter is arbitrary.

  1. lemma OAI.CircleDomainRigidity.exists_controlled_component_shrink line 14