OAI/Analysis/CircleDomains/Topology/JordanCrossingStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Crossing segments persist in converging finite models

Anchored convergence of the inner and outer Jordan contours retains a fixed compact subset of the inner fill and the strict nesting. Their prescribed zero/one boundary values then yield crossings over the same fixed projection set for all sufficiently late models.

  1. theorem OAI.CircleDomainRigidity.eventually_crossings_of_anchored_jordan_limits line 22