OAI/Analysis/CircleDomains/Topology/JordanFillLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Upper containment for limits of Jordan fills

Uniform convergence of boundary parametrizations traps the approximating closed fills in every neighborhood of the limiting closed fill. The proof uses Jordan nesting and radial enlargement.

  1. def OAI.CircleDomainRigidity.dilatedJordan line 22
  2. theorem OAI.CircleDomainRigidity.jordanInterior_dilated line 25
  3. theorem OAI.CircleDomainRigidity.eventually_jordan_fill_subset_open line 33
  4. theorem OAI.CircleDomainRigidity.mem_jordan_fill_of_tendsto line 69