OAI/Analysis/CircleDomains/Topology/FiniteJordanShrink.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One actual finite shrinking step. A disjoint Jordan cover with boundaries avoiding the compact obstacle can be compressed so that all its connected components have arbitrarily small image diameter.

  1. lemma OAI.CircleDomainRigidity.exists_finite_jordan_shrink line 13
  2. lemma OAI.CircleDomainRigidity.supported_displacement_bound line 73