OAI/Analysis/CircleDomains/Topology/ClosedJordanCore.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Closed cores bounded by a finite disjoint Jordan family

The closed common exterior is regular closed, its interior is the already constructed connected open completed region, and its boundary is exactly the union of the specified Jordan curves.

  1. def OAI.CircleDomainRigidity.closedJordanCore line 22
  2. theorem OAI.CircleDomainRigidity.interior_finite_disjoint_closed line 25
  3. theorem OAI.CircleDomainRigidity.interior_closedTerminalCap line 48
  4. theorem OAI.CircleDomainRigidity.interior_closedJordanCore line 65
  5. theorem OAI.CircleDomainRigidity.closure_interior_closedJordanCore line 71
  6. theorem OAI.CircleDomainRigidity.frontier_closedJordanCore line 80