OAI/Analysis/CircleDomains/Topology/SmallPerturbationJordan.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Small smooth ambient perturbations preserve regular Jordan curves.

  1. lemma OAI.CircleDomainRigidity.regularJordanParametrization_smallPerturbation line 13
  2. def OAI.CircleDomainRigidity.scaledPerturbationHomeomorph line 38
  3. lemma OAI.CircleDomainRigidity.scaledPerturbationHomeomorph_apply line 46
  4. lemma OAI.CircleDomainRigidity.scaledPerturbationHomeomorph_zero line 50
  5. lemma OAI.CircleDomainRigidity.positiveJordanParametrization_smallPerturbation line 56