OAI/Analysis/CircleDomains/Selection/MarkedEndTrapping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing marked finite disks to their prescribed ends

The finite-stage geometric containment and uniform convergence on each fixed boundary curve imply containment in the whole limiting end component. No winding-number or boundary-extension hypothesis is used.

  1. theorem OAI.CircleDomainRigidity.limit_disk_subset_jordan_fill line 24
  2. theorem OAI.CircleDomainRigidity.limit_disk_subset_prescribed_end line 45