OAI/Analysis/CircleDomains/Topology/CrosscutAvoidingContinuum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A connected compact set in the closed disk can be replaced by a simple crosscut with the same two boundary endpoints while avoiding a disjoint closed set.

  1. lemma OAI.CircleDomainRigidity.radial_segment_in_thickened_disk line 15
  2. lemma OAI.CircleDomainRigidity.exists_disk_crosscut_avoiding line 37