def EuclidGeom.Shan_Problem_1_5.tri {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} : EuclidGeom.Triangle P

Equations

• EuclidGeom.Shan_Problem_1_5.tri = { point₁ := A, point₂ := B, point₃ := C }

theorem EuclidGeom.Shan_Problem_1_5.A_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} : A ≠ C

theorem EuclidGeom.Shan_Problem_1_5.B_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} : B ≠ C

def EuclidGeom.Shan_Problem_1_5.SegND_ac {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} : EuclidGeom.SegND P

Equations

• EuclidGeom.Shan_Problem_1_5.SegND_ac = SEG_nd A C (_ : C ≠ A)

def EuclidGeom.Shan_Problem_1_5.SegND_bc {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} : EuclidGeom.SegND P

Equations

• EuclidGeom.Shan_Problem_1_5.SegND_bc = { val := { source := B, target := C }, property := (_ : { source := B, target := C }.target ≠ { source := B, target := C }.source) }

theorem EuclidGeom.Shan_Problem_1_5.d_int_bc {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} {D : P} {d_mid : D = { source := B, target := C }.midpoint} : EuclidGeom.lies_int D { source := B, target := C }

theorem EuclidGeom.Shan_Problem_1_5.a_ne_d {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} {D : P} {d_mid : D = { source := B, target := C }.midpoint} : A ≠ D

def EuclidGeom.Shan_Problem_1_5.line_ad {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} {D : P} {d_mid : D = { source := B, target := C }.midpoint} : EuclidGeom.Line P

Equations

• EuclidGeom.Shan_Problem_1_5.line_ad = LIN A D (_ : D ≠ A)

theorem EuclidGeom.Shan_Problem_1_5.B_ne_E {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} {E : P} {be_eq_ac : { source := B, target := E }.length = { source := A, target := C }.length} : B ≠ E

def EuclidGeom.Shan_Problem_1_5.SegND_be {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {hnd : ¬EuclidGeom.Collinear A B C} {E : P} {be_eq_ac : { source := B, target := E }.length = { source := A, target := C }.length} : EuclidGeom.SegND P

Equations

• EuclidGeom.Shan_Problem_1_5.SegND_be = { val := { source := B, target := E }, property := (_ : { source := B, target := E }.target ≠ { source := B, target := E }.source) }

theorem EuclidGeom.Shan_Problem_1_5.Shan_Problem_1_5 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {E : P} {F : P} : { source := A, target := F }.length = { source := E, target := F }.length

theorem EuclidGeom.Shan_Problem_1_6.A_ne_B {P : Type u_1} {A : P} {B : P} : A ≠ B

theorem EuclidGeom.Shan_Problem_1_6.B_ne_C {P : Type u_1} {B : P} {C : P} : B ≠ C

theorem EuclidGeom.Shan_Problem_1_6.c_ne_a {P : Type u_1} {A : P} {C : P} : C ≠ A

def EuclidGeom.Shan_Problem_1_6.htsum {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (D : P) : ℝ

Equations

• EuclidGeom.Shan_Problem_1_6.htsum D = EuclidGeom.dist_pt_line D (LIN A B (_ : B ≠ A)) + EuclidGeom.dist_pt_line D (LIN A C (_ : C ≠ A))

theorem EuclidGeom.Shan_Problem_1_6.Shan_Problem_1_6 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D₁ : P} {D₂ : P} : EuclidGeom.Shan_Problem_1_6.htsum D₁ = EuclidGeom.Shan_Problem_1_6.htsum D₂