OAI/Analysis/CircleDomains/Topology/ConnectedDiskIntersection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A connected open plane set whose available unit-circle part is connected has connected intersection with the open unit disk.

  1. lemma OAI.CircleDomainRigidity.disk_component_closure_contains_circle line 12
  2. lemma OAI.CircleDomainRigidity.isPreconnected_inter_disk_of_circle line 38