theorem EuclidGeom.TriangleND.value_abs_add_value_abs_lt_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} : EuclidGeom.AngValue.abs tr_nd.angle₁.value + EuclidGeom.AngValue.abs tr_nd.angle₂.value < Real.pi

structure EuclidGeom.TriangleND.IsAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : Prop

• angle₁ : tr_nd.angle₁.IsAcu
• angle₂ : tr_nd.angle₂.IsAcu
• angle₃ : tr_nd.angle₃.IsAcu

theorem EuclidGeom.TriangleND.perm_isAcu_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} : (EuclidGeom.TriangleND.perm_vertices tr_nd).IsAcu ↔ tr_nd.IsAcu

theorem EuclidGeom.TriangleND.flip_isAcu_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} : (EuclidGeom.TriangleND.flip_vertices tr_nd).IsAcu ↔ tr_nd.IsAcu

def EuclidGeom.TriangleND.IsRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : Prop

Equations

• tr_nd.IsRt = tr_nd.angle₁.IsRt

theorem EuclidGeom.TriangleND.flip_isRt_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} : (EuclidGeom.TriangleND.flip_vertices tr_nd).IsAcu ↔ tr_nd.IsAcu

theorem EuclidGeom.TriangleND.angle₂_isAcu_of_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} (h : tr_nd.IsRt) : tr_nd.angle₂.IsAcu

theorem EuclidGeom.TriangleND.angle₃_isAcu_of_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} (h : tr_nd.IsRt) : tr_nd.angle₃.IsAcu

def EuclidGeom.TriangleND.IsObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : Prop

Equations

• tr_nd.IsObt = tr_nd.angle₁.IsObt

theorem EuclidGeom.TriangleND.flip_isObt_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} : (EuclidGeom.TriangleND.flip_vertices tr_nd).IsAcu ↔ tr_nd.IsAcu

theorem EuclidGeom.TriangleND.angle₂_isAcu_of_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} (h : tr_nd.IsObt) : tr_nd.angle₂.IsAcu

theorem EuclidGeom.TriangleND.angle₃_isAcu_of_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd : EuclidGeom.TriangleND P} (h : tr_nd.IsObt) : tr_nd.angle₃.IsAcu

theorem EuclidGeom.edge_toLine_not_para_of_not_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : ¬EuclidGeom.Collinear A B C) : ¬EuclidGeom.Parallel (SEG_nd A B (_ : B ≠ A)) (SEG_nd B C (_ : C ≠ B)) ∧ ¬EuclidGeom.Parallel (SEG_nd B C (_ : C ≠ B)) (SEG_nd C A (_ : A ≠ C)) ∧ ¬EuclidGeom.Parallel (SEG_nd C A (_ : A ≠ C)) (SEG_nd A B (_ : B ≠ A))

theorem EuclidGeom.angle_eq_of_cosine_eq_of_cclock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (cclock : tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock) (cosine : EuclidGeom.AngValue.cos tr_nd₁.angle₁.value = EuclidGeom.AngValue.cos tr_nd₂.angle₁.value) : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value

theorem EuclidGeom.angle_eq_neg_of_cosine_eq_of_clock {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (clock : tr_nd₁.is_cclock ↔ ¬tr_nd₂.is_cclock) (cosine : EuclidGeom.AngValue.cos tr_nd₁.angle₁.value = EuclidGeom.AngValue.cos tr_nd₂.angle₁.value) : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value

theorem EuclidGeom.sine_ne_zero_of_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.AngValue.sin tr_nd.angle₁.value ≠ 0

theorem EuclidGeom.TriangleND.edge_eq_edge_of_perm_vertices_two_times {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : (↑tr_nd).edge₁.length = (↑(EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd))).edge₃.length ∧ (↑tr_nd).edge₂.length = (↑(EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd))).edge₁.length ∧ (↑tr_nd).edge₃.length = (↑(EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd))).edge₂.length

theorem EuclidGeom.TriangleND.angle_eq_angle_of_perm_vertices_two_times {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.angle₁.value = (EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd)).angle₃.value ∧ tr_nd.angle₂.value = (EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd)).angle₁.value ∧ tr_nd.angle₃.value = (EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd)).angle₂.value

theorem EuclidGeom.TriangleND.points_ne_of_collinear_of_not_collinear1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (ncolin : ¬EuclidGeom.Collinear A B C) (colin : EuclidGeom.Collinear D B C) : D ≠ A

theorem EuclidGeom.TriangleND.points_ne_of_collinear_of_not_collinear2 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (ncolin : ¬EuclidGeom.Collinear A B C) (colin : EuclidGeom.Collinear D C A) : D ≠ B

theorem EuclidGeom.TriangleND.points_ne_of_collinear_of_not_collinear3 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (ncolin : ¬EuclidGeom.Collinear A B C) (colin : EuclidGeom.Collinear D A B) : D ≠ C

theorem EuclidGeom.TriangleND.not_parallel_of_not_collinear_of_collinear_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {E : P} (nd : ¬EuclidGeom.Collinear A B C) (colindbc : EuclidGeom.Collinear D B C) (colineca : EuclidGeom.Collinear E C A) : ¬EuclidGeom.Parallel (LIN A D (_ : D ≠ A)) (LIN B E (_ : E ≠ B))

theorem EuclidGeom.TriangleND.intersection_not_collinear_of_nondegenerate {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {E : P} (nd : ¬EuclidGeom.Collinear A B C) (colindbc : EuclidGeom.Collinear D B C) (colineca : EuclidGeom.Collinear E C A) (dneb : D ≠ B) (dnec : D ≠ C) (enea : E ≠ A) (enec : E ≠ C) (F : P) (fdef : F = EuclidGeom.Line.inx (LIN A D (_ : D ≠ A)) (LIN B E (_ : E ≠ B)) (_ : ¬EuclidGeom.Parallel (LIN A D (_ : D ≠ A)) (LIN B E (_ : E ≠ B)))) : ¬EuclidGeom.Collinear A B F ∧ ¬EuclidGeom.Collinear B C F ∧ ¬EuclidGeom.Collinear C A F

theorem EuclidGeom.TriangleND.cclock_of_eq_angle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) (a : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) : tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock

theorem EuclidGeom.TriangleND.clock_of_eq_neg_angle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) (a : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value) : tr_nd₁.is_cclock ↔ ¬tr_nd₂.is_cclock

theorem EuclidGeom.angle_sum_eq_pi_of_tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri : EuclidGeom.Triangle P) (h₁ : tri.point₂ ≠ tri.point₃) (h₂ : tri.point₃ ≠ tri.point₁) (h₃ : tri.point₁ ≠ tri.point₂) : ∠ tri.point₂ tri.point₁ tri.point₃ (_ : tri.point₂ ≠ tri.point₁) h₂ + ∠ tri.point₃ tri.point₂ tri.point₁ (_ : tri.point₃ ≠ tri.point₂) h₃ + ∠ tri.point₁ tri.point₃ tri.point₂ (_ : tri.point₁ ≠ tri.point₃) h₁ = ∠[Real.pi]