Merge pull request #285 from Thmoas-Guan/master

add compatibility of seg and relative side
jjdishere · Jan 16, 2024 · d8a4609 · d8a4609
2 parents 9fcd9f7 + 6a25c27
commit d8a4609
Show file tree

Hide file tree

Showing 2 changed files with 491 additions and 16 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean
@@ -98,5 +98,24 @@ theorem eq_toDir_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A Lies
 
 theorem eq_toDirLine_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target h.ne_target.symm).toDirLine = seg_nd.toDirLine := by sorry
 
+--Guan Nailin
+theorem every_pt_onLine_exist_rep (A : P) (l : Line P) (ha : A LiesOn l) : ∃ ray : Ray P , (ray.source = A) ∧ (ray.toLine = l) := by
+  rcases (Quotient.exists_rep l.toProj) with ⟨Dir , h0⟩
+  let r : Ray P := ⟨A,Dir⟩
+  have s: r.source = A := by rfl
+  have l: r.toLine = l := by
+    have : r.toProj = l.toProj := by
+      calc
+        _= r.toDir.toProj := by rfl
+        _= ⟦Dir⟧ := by rfl
+        _=_ := h0
+    calc
+      _= Line.mk_pt_proj A r.toProj := by rfl
+      _= Line.mk_pt_proj A l.toProj := by congr
+      _= l := by
+        apply Line.mk_pt_proj_eq_of_eq_toProj
+        exact ha
+        rfl
+  use r
 
 end EuclidGeom