Merge pull request #223 from kfc2333/master

Team_D_changed_Parallelogram.lean&Quadrilateral.lean
jjdishere · Nov 26, 2023 · eef2aac · eef2aac
2 parents 5ac535d + a5fbc64
commit eef2aac
Show file tree

Hide file tree

Showing 5 changed files with 491 additions and 179 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
@@ -3,6 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray
 namespace EuclidGeom
 
 variable {P : Type _} [EuclideanPlane P]
+variable {P : Type _} [EuclideanPlane P] (seg_nd : Seg_nd P)
 
 theorem Seg_nd.not_lies_int_extn_and_rev_extn_of_lies_on {A : P} {seg_nd : Seg_nd P} (lieson : A LiesOn seg_nd.1) : ¬ A LiesInt seg_nd.extension ∧ ¬ A LiesInt seg_nd.reverse.extension := by
   constructor
@@ -15,4 +16,8 @@ theorem Seg_nd.not_lies_int_extn_and_rev_extn_of_lies_on {A : P} {seg_nd : Seg_n
   simp only [extn_eq_rev_toray_rev, Ray.rev_rev_eq_self, Seg_nd.rev_rev_eq_self]
   exact lies_on_toray_of_lies_on lieson
 
+theorem Seg_nd_midpoint_not_eq_source : seg_nd.1.midpoint ≠ seg_nd.source := by sorry
+
+theorem Seg_nd_midpoint_not_eq_target : seg_nd.1.midpoint ≠ seg_nd.target := by sorry
+
   end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean
@@ -12,4 +12,7 @@ theorem start_ray_todir_rev_todir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs :
 
 theorem angle_value_eq_angle (A : P) (ray : Ray P) (h : A ≠ ray.1) : (Angle.mk_ray_pt ray A h).value = Vec_nd.angle ray.2.toVec_nd (VEC_nd ray.source A h) := sorry
 
+theorem ang_eq_ang_of_todir_rev_todir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = - ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = - ang₂.end_ray.toDir) : ang₁.value = ang₂.value := sorry
+
+
 end EuclidGeom
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean
@@ -1,4 +1,4 @@
-import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence
+import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence'
 
 noncomputable section
 namespace EuclidGeom
Original file line number	Diff line number	Diff line change
Expand Up		@@ -12,4 +12,7 @@ theorem start_ray_todir_rev_todir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs :

		theorem angle_value_eq_angle (A : P) (ray : Ray P) (h : A ≠ ray.1) : (Angle.mk_ray_pt ray A h).value = Vec_nd.angle ray.2.toVec_nd (VEC_nd ray.source A h) := sorry

		theorem ang_eq_ang_of_todir_rev_todir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = - ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = - ang₂.end_ray.toDir) : ang₁.value = ang₂.value := sorry


		end EuclidGeom