OAI/Analysis/CircleDomains/Topology/CrosscutPathSides.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Side membership is characterized by a path avoiding the crosscut to the corresponding explicit real-boundary point.

  1. def OAI.CircleDomainRigidity.DiskAvoidingPath line 15
  2. theorem OAI.CircleDomainRigidity.HalfPlaneRay.side_eq_iff_avoidingPath line 21
  3. theorem OAI.CircleDomainRigidity.HalfPlaneRay.right_iff_avoidingPath line 42
  4. theorem OAI.CircleDomainRigidity.HalfPlaneRay.left_iff_hit_or_avoidingPath line 70