OAI/Analysis/CircleDomains/Topology/RetainedJordanConvergence.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Anchors for the Jordan curves of actual finite models
A point of the physical domain on the inside of a retained contour gives an interior anchor in every sufficiently late model. The proved side correspondence identifies that side, and local uniform convergence gives the anchor and boundary convergence needed for the crossing argument.
- theorem
OAI.CircleDomainRigidity.exists_domain_point_inside_jordanline 24 - theorem
OAI.CircleDomainRigidity.exists_anchored_retained_jordan_modelsline 33