OAI/Analysis/CircleDomains/Topology/JordanEndComponents.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

End components of a strict Jordan-core exhaustion

The selected target disk at each level is determined by the omitted point. Strict core inclusion forces these disks to nest strictly. Their intersection is exactly the full complementary component of the exhausted image.

  1. theorem OAI.CircleDomainRigidity.component_eq_nested_jordan_end line 23