OAI/Analysis/CircleDomains/Selection/FiniteMarkedTrapping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Marked-disk trapping for the actual finite terminal assignment

The assignment is constructed from a finite model. Once a fixed source core is retained, a terminal inside one of its holes has its target disk inside the corresponding image contour. Uniform convergence on that contour passes this containment to the limiting closed disk.

  1. structure OAI.CircleDomainRigidity.TerminalComponentAssignment line 24
  2. theorem OAI.CircleDomainRigidity.exists_terminal_component_assignment line 40
  3. def OAI.CircleDomainRigidity.SmoothJordanCore.inDomain line 52
  4. theorem OAI.CircleDomainRigidity.range_finite_image_boundary line 63
  5. theorem OAI.CircleDomainRigidity.marked_limit_subset_retained_fill line 76