theorem EuclidGeom.Triangle.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Triangle P), x.point₁ = y.point₁ → x.point₂ = y.point₂ → x.point₃ = y.point₃ → x = y

theorem EuclidGeom.Triangle.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Triangle P), x = y ↔ x.point₁ = y.point₁ ∧ x.point₂ = y.point₂ ∧ x.point₃ = y.point₃

structure EuclidGeom.Triangle (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

• point₁ : P
• point₂ : P
• point₃ : P

def EuclidGeom.Triangle.edge₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Seg P

Equations

• tr.edge₁ = { source := tr.point₂, target := tr.point₃ }

def EuclidGeom.Triangle.edge₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Seg P

Equations

• tr.edge₂ = { source := tr.point₃, target := tr.point₁ }

def EuclidGeom.Triangle.edge₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Seg P

Equations

• tr.edge₃ = { source := tr.point₁, target := tr.point₂ }

def EuclidGeom.Triangle.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : ℝ

Equations

• tr.oarea = EuclidGeom.oarea tr.point₁ tr.point₂ tr.point₃

def EuclidGeom.Triangle.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : ℝ

Equations

• tr.area = |tr.oarea|

def EuclidGeom.Triangle.IsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : Prop

Equations

• tr.IsND = ¬EuclidGeom.Collinear tr.point₁ tr.point₂ tr.point₃

def EuclidGeom.TriangleND (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

Equations

• EuclidGeom.TriangleND P = { tr : EuclidGeom.Triangle P // tr.IsND }

@[inline, reducible]

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

Equations

• tr_nd.point₁ = (↑tr_nd).point₁

@[inline, reducible]

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

Equations

• tr_nd.point₂ = (↑tr_nd).point₂

@[inline, reducible]

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

Equations

• tr_nd.point₃ = (↑tr_nd).point₃

instance EuclidGeom.TriangleND.nontriv₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.PtNe tr_nd.point₃ tr_nd.point₂

Equations

• (_ : EuclidGeom.PtNe tr_nd.point₃ tr_nd.point₂) = (_ : Fact (tr_nd.point₃ ≠ tr_nd.point₂))

instance EuclidGeom.TriangleND.nontriv₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.PtNe tr_nd.point₁ tr_nd.point₃

Equations

• (_ : EuclidGeom.PtNe tr_nd.point₁ tr_nd.point₃) = (_ : Fact (tr_nd.point₁ ≠ tr_nd.point₃))

instance EuclidGeom.TriangleND.nontriv₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.PtNe tr_nd.point₂ tr_nd.point₁

Equations

• (_ : EuclidGeom.PtNe tr_nd.point₂ tr_nd.point₁) = (_ : Fact (tr_nd.point₂ ≠ tr_nd.point₁))

@[inline, reducible]

abbrev EuclidGeom.TriangleND.edge₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Seg P

Equations

• tr_nd.edge₁ = (↑tr_nd).edge₁

@[inline, reducible]

abbrev EuclidGeom.TriangleND.edge₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Seg P

Equations

• tr_nd.edge₂ = (↑tr_nd).edge₂

@[inline, reducible]

abbrev EuclidGeom.TriangleND.edge₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Seg P

Equations

• tr_nd.edge₃ = (↑tr_nd).edge₃

def EuclidGeom.TriangleND.edgeND₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.SegND P

Equations

• tr_nd.edgeND₁ = { val := (↑tr_nd).edge₁, property := (_ : tr_nd.point₃ ≠ tr_nd.point₂) }

def EuclidGeom.TriangleND.edgeND₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.SegND P

Equations

• tr_nd.edgeND₂ = { val := (↑tr_nd).edge₂, property := (_ : tr_nd.point₁ ≠ tr_nd.point₃) }

def EuclidGeom.TriangleND.edgeND₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.SegND P

Equations

• tr_nd.edgeND₃ = { val := (↑tr_nd).edge₃, property := (_ : tr_nd.point₂ ≠ tr_nd.point₁) }

@[inline, reducible]

abbrev EuclidGeom.TriangleND.oarea {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : ℝ

Equations

• tr_nd.oarea = (↑tr_nd).oarea

@[inline, reducible]

abbrev EuclidGeom.TriangleND.area {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : ℝ

Equations

• tr_nd.area = (↑tr_nd).area

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

Equations

• tr_nd.is_cclock = (0 < tr_nd.oarea)

def EuclidGeom.TriangleND.angle₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Angle P

Equations

• tr_nd.angle₁ = ANG tr_nd.point₂ tr_nd.point₁ tr_nd.point₃ (_ : tr_nd.point₂ ≠ tr_nd.point₁) (_ : tr_nd.point₃ ≠ tr_nd.point₁)

def EuclidGeom.TriangleND.angle₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Angle P

Equations

• tr_nd.angle₂ = ANG tr_nd.point₃ tr_nd.point₂ tr_nd.point₁ (_ : tr_nd.point₃ ≠ tr_nd.point₂) (_ : tr_nd.point₁ ≠ tr_nd.point₂)

def EuclidGeom.TriangleND.angle₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.Angle P

Equations

• tr_nd.angle₃ = ANG tr_nd.point₁ tr_nd.point₃ tr_nd.point₂ (_ : tr_nd.point₁ ≠ tr_nd.point₃) (_ : tr_nd.point₂ ≠ tr_nd.point₃)

def EuclidGeom.Triangle.IsInt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (tr : EuclidGeom.Triangle P) : Prop

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.Triangle.IsOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (tr : EuclidGeom.Triangle P) : Prop

Equations

• EuclidGeom.Triangle.IsOn A tr = (EuclidGeom.Triangle.IsInt A tr ∨ EuclidGeom.lies_on A tr.edge₁ ∨ EuclidGeom.lies_on A tr.edge₂ ∨ EuclidGeom.lies_on A tr.edge₃)

def EuclidGeom.Triangle.carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : Set P

Equations

• EuclidGeom.Triangle.carrier tr = {p : P | EuclidGeom.Triangle.IsOn p tr}

def EuclidGeom.Triangle.interior {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : Set P

Equations

• EuclidGeom.Triangle.interior tr = {p : P | EuclidGeom.Triangle.IsInt p tr}

instance EuclidGeom.Triangle.instInteriorTriangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.Interior (EuclidGeom.Triangle P) P

Equations

• EuclidGeom.Triangle.instInteriorTriangle = { interior := EuclidGeom.Triangle.interior }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• EuclidGeom.TriangleND.IsOn A tr_nd = (EuclidGeom.TriangleND.IsInt A tr_nd ∨ EuclidGeom.lies_on A tr_nd.edge₁ ∨ EuclidGeom.lies_on A tr_nd.edge₂ ∨ EuclidGeom.lies_on A tr_nd.edge₃)

def EuclidGeom.TriangleND.carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) : Set P

Equations

• EuclidGeom.TriangleND.carrier tr_nd = {p : P | EuclidGeom.Triangle.IsOn p tr_nd}

def EuclidGeom.TriangleND.interior {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) : Set P

Equations

• EuclidGeom.TriangleND.interior tr_nd = {p : P | EuclidGeom.Triangle.IsInt p tr_nd}

def EuclidGeom.Triangle.perm_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Triangle P

Equations

• tr.perm_vertices = { point₁ := tr.point₂, point₂ := tr.point₃, point₃ := tr.point₁ }

theorem EuclidGeom.Triangle.eq_self_of_perm_vertices_three_times {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : tr.perm_vertices.perm_vertices.perm_vertices = tr

def EuclidGeom.Triangle.flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Triangle P

Equations

• tr.flip_vertices = { point₁ := tr.point₁, point₂ := tr.point₃, point₃ := tr.point₂ }

theorem EuclidGeom.Triangle.eq_self_of_flip_vertices_twice {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : tr.flip_vertices.flip_vertices = tr

theorem EuclidGeom.Triangle.eq_flip_of_perm_twice_of_perm_flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : tr.flip_vertices.perm_vertices.perm_vertices = tr.perm_vertices.flip_vertices

theorem EuclidGeom.Triangle.is_inside_of_is_inside_perm_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) (p : P) (inside : EuclidGeom.lies_int p tr) : EuclidGeom.lies_int p tr.perm_vertices

theorem EuclidGeom.Triangle.is_inside_of_is_inside_flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) (p : P) (inside : EuclidGeom.lies_int p tr) : EuclidGeom.lies_int p tr.flip_vertices

def EuclidGeom.TriangleND.perm_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND P

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.TriangleND.flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND P

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.TriangleND.eq_self_of_perm_vertices_three_times {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd)) = tr_nd

theorem EuclidGeom.TriangleND.eq_self_of_flip_vertices_twice {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND.flip_vertices (EuclidGeom.TriangleND.flip_vertices tr_nd) = tr_nd

theorem EuclidGeom.TriangleND.eq_flip_of_perm_twice_of_perm_flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.perm_vertices (EuclidGeom.TriangleND.flip_vertices tr_nd)) = EuclidGeom.TriangleND.flip_vertices (EuclidGeom.TriangleND.perm_vertices tr_nd)

theorem EuclidGeom.TriangleND.same_orient_of_perm_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.is_cclock = (EuclidGeom.TriangleND.perm_vertices tr_nd).is_cclock

theorem EuclidGeom.TriangleND.reverse_orient_of_flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.is_cclock = ¬(EuclidGeom.TriangleND.flip_vertices tr_nd).is_cclock

theorem EuclidGeom.TriangleND.is_inside_of_is_inside_perm_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) (p : P) (inside : EuclidGeom.lies_int p tr_nd) : EuclidGeom.lies_int p tr_nd.perm_vertices

theorem EuclidGeom.TriangleND.is_inside_of_is_inside_flip_vertices {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.Triangle P) (p : P) (inside : EuclidGeom.lies_int p tr_nd) : EuclidGeom.lies_int p tr_nd.flip_vertices

def EuclidGeom.TriangleND.mk {P : Type u_2} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (h : ¬EuclidGeom.Collinear A B C) : EuclidGeom.TriangleND P

Equations

• EuclidGeom.TriangleND.mk A B C h = { val := { point₁ := A, point₂ := B, point₃ := C }, property := h }

def EuclidGeom.termTRI : Lean.ParserDescr

Equations

• EuclidGeom.termTRI = Lean.ParserDescr.node `EuclidGeom.termTRI 1024 (Lean.ParserDescr.symbol "TRI")

def EuclidGeom.«term▵» : Lean.ParserDescr

Equations

• EuclidGeom.«term▵» = Lean.ParserDescr.node `EuclidGeom.term▵ 1024 (Lean.ParserDescr.symbol "▵")

def EuclidGeom.termTRI_nd____ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem EuclidGeom.Triangle.triangle_ineq {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : tr.edge₃.length ≤ tr.edge₁.length + tr.edge₂.length

theorem EuclidGeom.Triangle.trivial_of_edge_sum_eq_edge {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬tr.IsND

theorem EuclidGeom.Triangle.triangle_ineq' {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) (nontriv : tr.IsND) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length

theorem EuclidGeom.Triangle.edge_sum_eq_edge_iff_collinear {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.Triangle P) : EuclidGeom.Collinear tr.point₁ tr.point₂ tr.point₃ ↔ tr.edge₁.length + tr.edge₂.length = tr.edge₃.length ∨ tr.edge₂.length + tr.edge₃.length = tr.edge₁.length ∨ tr.edge₃.length + tr.edge₁.length = tr.edge₂.length

theorem EuclidGeom.TriangleND.angle₁_pos_iff_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsPos

theorem EuclidGeom.TriangleND.angle₂_pos_iff_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.is_cclock ↔ tr_nd.angle₂.value.IsPos

theorem EuclidGeom.TriangleND.angle₃_pos_iff_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.is_cclock ↔ tr_nd.angle₃.value.IsPos

theorem EuclidGeom.TriangleND.angle₁_neg_iff_not_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : ¬tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsNeg

theorem EuclidGeom.TriangleND.angle₂_neg_iff_not_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : ¬tr_nd.is_cclock ↔ tr_nd.angle₂.value.IsNeg

theorem EuclidGeom.TriangleND.angle₃_neg_iff_not_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : ¬tr_nd.is_cclock ↔ tr_nd.angle₃.value.IsNeg

theorem EuclidGeom.TriangleND.pos_pos_or_neg_neg_of_iff_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} : (tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock) ↔ tr_nd₁.angle₁.value.IsPos ∧ tr_nd₂.angle₁.value.IsPos ∨ tr_nd₁.angle₁.value.IsNeg ∧ tr_nd₂.angle₁.value.IsNeg

theorem EuclidGeom.TriangleND.angle_sum_eq_pi_of_cclock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (cclock : tr_nd.is_cclock) : tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = ∠[Real.pi]

theorem EuclidGeom.TriangleND.angle_sum_eq_neg_pi_of_clock {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (clock : ¬tr_nd.is_cclock) : tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = -∠[Real.pi]

theorem EuclidGeom.TriangleND.triangle_ineq' {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.edge₁.length + tr_nd.edge₂.length > tr_nd.edge₃.length

theorem EuclidGeom.TriangleND.sum_of_other_angle_same_if_one_angle_same {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (a : tr₁.angle₁.value = tr₂.angle₁.value) : tr₁.angle₂.value + tr₁.angle₃.value = tr₂.angle₂.value + tr₂.angle₃.value

theorem EuclidGeom.TriangleND.sum_of_other_angle_same_neg_if_one_angle_same_neg {P : Type u_2} [EuclidGeom.EuclideanPlane P] (tr₁ : EuclidGeom.TriangleND P) (tr₂ : EuclidGeom.TriangleND P) (a : tr₁.angle₁.value = -tr₂.angle₁.value) : tr₁.angle₂.value + tr₁.angle₃.value = -(tr₂.angle₂.value + tr₂.angle₃.value)