OAI/Analysis/CircleDomains/Topology/ClosedDiskCutSides.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two sides remain separated at the boundary of the closed disk. Membership in the filled side is locally constant away from the crosscut.

  1. abbrev OAI.CircleDomainRigidity.DiskCutDomain line 14
  2. def OAI.CircleDomainRigidity.diskCutSide line 17
  3. theorem OAI.CircleDomainRigidity.isLocallyConstant_diskCutSide line 21
  4. theorem OAI.CircleDomainRigidity.diskCutSide_eq_on_connected line 50
  5. theorem OAI.CircleDomainRigidity.diskCutSide_path_intersection line 59