OAI/Analysis/CircleDomains/Selection/PrescribedMarkedEnds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Marked disk limits lie in their prescribed complementary components

Local uniform convergence on the source gives uniform convergence on each retained circle. The finite terminal assignment and the nested target end description then place the entire limiting round disk in the prescribed component, including a zero-radius limit.

  1. theorem OAI.CircleDomainRigidity.marked_limit_subset_corresponding_component line 25