OAI/Analysis/CircleDomains/Topology/IsolatedDiskComponent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A closed disk with an exterior collar contained in the domain is an entire complementary component.

  1. lemma OAI.CircleDomainRigidity.connectedComponentIn_eq_of_relative_clopen line 12
  2. lemma OAI.CircleDomainRigidity.closedBall_complementary_component line 21