OAI/Analysis/CircleDomains/Topology/JordanHoleSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Select exactly the finite round holes inside a retained Jordan curve. Its punctured closed side is therefore contained in the actual target domain, including its outer boundary.

  1. theorem OAI.CircleDomainRigidity.round_hole_jordan_side line 14
  2. theorem OAI.CircleDomainRigidity.exists_round_holes_inside_jordan line 30