OAI/Analysis/CircleDomains/Topology/AnchoredJordanLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Interior stability of Jordan fills with an interior anchor

Uniformly converging Jordan contours retain every compact part of the limiting interior if one convergent sequence of interior points is known. A smaller connected Jordan disk joins that anchor to the compact set, and avoids all approximating boundaries. This uses no winding-number assumption.

  1. theorem OAI.CircleDomainRigidity.eventually_compact_subset_jordanInterior_of_anchor line 22