OAI/Analysis/CircleDomains/Topology/RayJordanSides.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Side functions for all integer translates of a lifted ray. Boundary order is the ordinary order on the real boundary of the half-plane.

  1. def OAI.CircleDomainRigidity.HalfPlaneRay.IsJordan line 18
  2. theorem OAI.CircleDomainRigidity.HalfPlaneRay.exists_jordan line 21
  3. theorem OAI.CircleDomainRigidity.HalfPlaneRay.crosscut_norm_le line 36
  4. theorem OAI.CircleDomainRigidity.HalfPlaneRay.filling_subset line 46
  5. abbrev OAI.CircleDomainRigidity.HalfPlaneRay.CutDomain line 60
  6. def OAI.CircleDomainRigidity.HalfPlaneRay.side line 62
  7. theorem OAI.CircleDomainRigidity.HalfPlaneRay.isLocallyConstant_side line 65
  8. theorem OAI.CircleDomainRigidity.HalfPlaneRay.start_eq_real line 97
  9. theorem OAI.CircleDomainRigidity.HalfPlaneRay.side_boundary line 106