OAI/Analysis/CircleDomains/Topology/DiskComponentBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Components of an open planar set cut by a disk are relatively closed, and a component approaching an available circle point occupies its whole small inner neighborhood.

  1. lemma OAI.CircleDomainRigidity.closure_component_inter_subset line 14
  2. lemma OAI.CircleDomainRigidity.disk_component_boundary_neighborhood line 22
  3. lemma OAI.CircleDomainRigidity.disk_component_touches_available_circle line 43