OAI/Analysis/CircleDomains/Topology/HalfPlanePathSides.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The side path test in the original half-plane coordinates.

  1. def OAI.CircleDomainRigidity.HalfPlaneAvoidingPath line 15
  2. theorem OAI.CircleDomainRigidity.HalfPlaneRay.diskAvoiding_iff_halfPlaneAvoiding line 19
  3. theorem OAI.CircleDomainRigidity.HalfPlaneRay.right_iff_halfPlanePath line 56
  4. theorem OAI.CircleDomainRigidity.HalfPlaneRay.translated_right line 64