EuclideanGeometry.Foundation.Axiom.Triangle.Basic

source

theorem EuclidGeom.Triangle.lie_on_snd_and_trd_edge_of_fst_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr.point₁ tr.edge₂ ∧ EuclidGeom.lies_on tr.point₁ tr.edge₃

source

theorem EuclidGeom.Triangle.lie_on_trd_and_fst_edge_of_snd_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr.point₁ tr.edge₂ ∧ EuclidGeom.lies_on tr.point₁ tr.edge₃

source

theorem EuclidGeom.Triangle.lie_on_fst_and_snd_edge_of_trd_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr.point₁ tr.edge₂ ∧ EuclidGeom.lies_on tr.point₁ tr.edge₃

source

theorem EuclidGeom.TriangleND.ne_vertex_of_lies_int_fst_edge {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A tr_nd.edge₁) :

A ≠ tr_nd.point₁ ∧ A ≠ tr_nd.point₂ ∧ A ≠ tr_nd.point₃

source

theorem EuclidGeom.TriangleND.ne_vertex_of_lies_int_snd_edge {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A tr_nd.edge₂) :

A ≠ tr_nd.point₁ ∧ A ≠ tr_nd.point₂ ∧ A ≠ tr_nd.point₃

source

theorem EuclidGeom.TriangleND.ne_vertex_of_lies_int_trd_edge {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A tr_nd.edge₃) :

A ≠ tr_nd.point₁ ∧ A ≠ tr_nd.point₂ ∧ A ≠ tr_nd.point₃

source

theorem EuclidGeom.TriangleND.lie_on_snd_and_trd_edge_of_fst_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₂ ∧ EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₃

source

theorem EuclidGeom.TriangleND.lie_on_trd_and_fst_edge_of_snd_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₂ ∧ EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₃

source

theorem EuclidGeom.TriangleND.lie_on_fst_and_snd_edge_of_trd_vertex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) :

EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₂ ∧ EuclidGeom.lies_on tr_nd.point₁ tr_nd.edge₃

source

theorem EuclidGeom.TriangleND.not_lie_on_snd_and_trd_of_int_fst {P : Type u_1} [EuclidGeom.EuclideanPlane P] (trind : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A (↑trind).edge₁) :

¬EuclidGeom.lies_on A (↑trind).edge₂ ∧ ¬EuclidGeom.lies_on A (↑trind).edge₃

source

theorem EuclidGeom.TriangleND.not_lie_on_trd_and_fst_of_int_snd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (trind : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A (↑trind).edge₂) :

¬EuclidGeom.lies_on A (↑trind).edge₃ ∧ ¬EuclidGeom.lies_on A (↑trind).edge₁

source

theorem EuclidGeom.TriangleND.not_lie_on_fst_and_snd_of_int_trd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (trind : EuclidGeom.TriangleND P) {A : P} (h : EuclidGeom.lies_int A (↑trind).edge₃) :

¬EuclidGeom.lies_on A (↑trind).edge₁ ∧ ¬EuclidGeom.lies_on A (↑trind).edge₂

source

theorem EuclidGeom.Triangle.edge_eq_edge_of_flip_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

tr.edge₁.length = tr.flip_vertices.edge₁.length ∧ tr.edge₂.length = tr.flip_vertices.edge₃.length ∧ tr.edge₃.length = tr.flip_vertices.edge₂.length

source

theorem EuclidGeom.Triangle.edge_eq_edge_of_perm_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

tr.edge₁.length = tr.perm_vertices.edge₂.length ∧ tr.edge₂.length = tr.perm_vertices.edge₃.length ∧ tr.edge₃.length = tr.perm_vertices.edge₁.length

source

theorem EuclidGeom.Triangle.nd_iff_nd_of_perm_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) :

tr.IsND ↔ tr.perm_vertices.IsND

source

theorem EuclidGeom.TriangleND.edge_eq_edge_of_flip_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.edge₁.length = (EuclidGeom.TriangleND.flip_vertices tr_nd).edge₁.length ∧ tr_nd.edge₂.length = (EuclidGeom.TriangleND.flip_vertices tr_nd).edge₃.length ∧ tr_nd.edge₃.length = (EuclidGeom.TriangleND.flip_vertices tr_nd).edge₂.length

source

theorem EuclidGeom.TriangleND.edge_eq_edge_of_perm_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.edge₁.length = (EuclidGeom.TriangleND.perm_vertices tr_nd).edge₂.length ∧ tr_nd.edge₂.length = (EuclidGeom.TriangleND.perm_vertices tr_nd).edge₃.length ∧ tr_nd.edge₃.length = (EuclidGeom.TriangleND.perm_vertices tr_nd).edge₁.length

source

theorem EuclidGeom.TriangleND.angle_eq_neg_angle_of_flip_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.angle₁.value = -(EuclidGeom.TriangleND.flip_vertices tr_nd).angle₁.value ∧ tr_nd.angle₂.value = -(EuclidGeom.TriangleND.flip_vertices tr_nd).angle₃.value ∧ tr_nd.angle₃.value = -(EuclidGeom.TriangleND.flip_vertices tr_nd).angle₂.value

source

theorem EuclidGeom.TriangleND.angle_eq_angle_of_perm_vertices {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.angle₁.value = (EuclidGeom.TriangleND.perm_vertices tr_nd).angle₂.value ∧ tr_nd.angle₂.value = (EuclidGeom.TriangleND.perm_vertices tr_nd).angle₃.value ∧ tr_nd.angle₃.value = (EuclidGeom.TriangleND.perm_vertices tr_nd).angle₁.value

source

theorem EuclidGeom.TriangleND.iscclock_iff_liesonleft₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.is_cclock = EuclidGeom.IsOnLeftSide (↑tr_nd).point₃ tr_nd.edgeND₃

source

theorem EuclidGeom.TriangleND.iscclock_iff_liesonleft₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.is_cclock = EuclidGeom.IsOnLeftSide (↑tr_nd).point₁ tr_nd.edgeND₁

source

theorem EuclidGeom.TriangleND.iscclock_iff_liesonleft₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :

tr_nd.is_cclock = EuclidGeom.IsOnLeftSide (↑tr_nd).point₂ tr_nd.edgeND₂

source

theorem EuclidGeom.TriangleND.eq_cclock_of_IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnSameSide C D (RAY A B)) :

(EuclidGeom.TriangleND.mk A B C (_ : ¬EuclidGeom.Collinear A B C)).is_cclock = (EuclidGeom.TriangleND.mk A B D (_ : ¬EuclidGeom.Collinear A B D)).is_cclock

source

theorem EuclidGeom.TriangleND.anti_cclock_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnOppositeSide C D (SEG_nd A B)) :

(EuclidGeom.TriangleND.mk A B C (_ : ¬EuclidGeom.Collinear A B C)).is_cclock → ¬(EuclidGeom.TriangleND.mk A B D (_ : ¬EuclidGeom.Collinear A B D)).is_cclock

source

theorem EuclidGeom.TriangleND.liesonleft_ne_pts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnLeftSide C (DLIN A B)) :

C ≠ A ∧ C ≠ B

source

theorem EuclidGeom.TriangleND.liesonleft_angle_ispos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnLeftSide C (DLIN A B)) :

(∠ A C B (_ : A ≠ C) (_ : B ≠ C)).IsPos

source

theorem EuclidGeom.TriangleND.liesonright_ne_pts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnRightSide C (DLIN A B)) :

C ≠ A ∧ C ≠ B

source

theorem EuclidGeom.TriangleND.liesonright_angle_isneg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnRightSide C (DLIN A B)) :

(∠ A C B (_ : A ≠ C) (_ : B ≠ C)).IsNeg