Merge pull request #106 from Liang-Xiao-pku/master

add some thing to prove A \neq B when one on line the other not on line
jjdishere · Sep 24, 2023 · 87d8282 · 87d8282
2 parents 473c850 + 55cc23a
commit 87d8282
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 0 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Class.lean
@@ -29,6 +29,19 @@ scoped infix : 50 "LiesInt" => lies_int
 -- scoped infix : 50 "LiesIn" => lies_in
 -- scoped notation A "IsInx" F G => (is_inx A F G) -- this notation doesn't work as imagined
 
+section compatibility
+
+theorem ne_of_lieson_and_not_lieson {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] {F : α} {X Y : P} (hx : X LiesOn F) (hy : ¬ Y LiesOn F) : X ≠ Y := by 
+  by_contra h
+  rw [h] at hx
+  tauto
+
+theorem ne_of_liesint_and_not_liesint {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] {F : α} {X Y : P} (hx : X LiesInt F) (hy : ¬ Y LiesInt F) : X ≠ Y := by 
+  by_contra h
+  rw [h] at hx
+  tauto
+end compatibility
+
 /- Three figures concurrent at a point -/
 def concurrent {P : Type _} [EuclideanPlane P] {α β γ: Type _} [Carrier P α] [Carrier P β] [Carrier P γ] (A : P) (F : α) (G : β) (H : γ) : Prop := A LiesOn F ∧ A LiesOn G ∧ A LiesOn H
 

diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean
@@ -192,4 +192,11 @@ theorem Line.exist_pt_beyond_pt {A B : P} {l : Line P} (hA : A LiesOn l) (hB : B
 
 end Archimedean_property
 
+
+section NewTheorems
+
+theorem Seg_nd.lies_on_toline_of_lies_on_extn {X : P} {segnd : Seg_nd P} (lieson : X LiesOn segnd.extension) : X LiesOn segnd.toLine := by sorry
+
+end NewTheorems
+
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -46,6 +46,12 @@ def nontriv₂ := (ne_of_not_colinear tr_nd.2).2.1
 
 def nontriv₃ := (ne_of_not_colinear tr_nd.2).2.2
 
+def edge_nd₁ : Seg_nd P := ⟨tr_nd.1.edge₁, tr_nd.nontriv₁⟩
+
+def edge_nd₂ : Seg_nd P := ⟨tr_nd.1.edge₂, tr_nd.nontriv₂⟩
+
+def edge_nd₃ : Seg_nd P := ⟨tr_nd.1.edge₃, tr_nd.nontriv₃⟩
+
 /- Only nondegenerate triangles can talk about orientation -/
 def is_cclock : Prop := tr_nd.1.3 LiesOnLeft (Ray.mk_pt_pt tr_nd.1.1 tr_nd.1.2 (tr_nd.nontriv₃))
 
@@ -55,6 +61,8 @@ def angle₂ : Angle P := Angle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₁) (tr_nd.nont
 
 def angle₃ : Angle P := Angle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₂) (tr_nd.nontriv₁).symm
 
+
+
 end Triangle_nd
 
 end nondeg