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

Equations

• EuclidGeom.wedge A B C = (EuclidGeom.Vec.det (EuclidGeom.Vec.mkPtPt A B)) (EuclidGeom.Vec.mkPtPt A C)

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

Equations

• EuclidGeom.oarea A B C = EuclidGeom.wedge A B C / 2

theorem EuclidGeom.wedge213 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.wedge B A C = -EuclidGeom.wedge A B C

theorem EuclidGeom.wedge132 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.wedge A C B = -EuclidGeom.wedge A B C

theorem EuclidGeom.wedge231 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.wedge C A B = EuclidGeom.wedge A B C

theorem EuclidGeom.wedge312 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.wedge B C A = EuclidGeom.wedge A B C

theorem EuclidGeom.wedge321 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.wedge C B A = -EuclidGeom.wedge A B C

theorem EuclidGeom.wedge_eq_length_mul_length_mul_sin {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [bnea : EuclidGeom.PtNe B A] [cnea : EuclidGeom.PtNe C A] : EuclidGeom.wedge A B C = { source := A, target := B }.length * { source := A, target := C }.length * EuclidGeom.AngValue.sin (ANG B A C).value

theorem EuclidGeom.collinear_iff_wedge_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.Collinear A B C ↔ EuclidGeom.wedge A B C = 0

theorem EuclidGeom.not_collinear_iff_wedge_ne_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : ¬EuclidGeom.Collinear A B C ↔ EuclidGeom.wedge A B C ≠ 0

theorem EuclidGeom.wedge_pos_iff_angle_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (nd : ¬EuclidGeom.Collinear A B C) : 0 < EuclidGeom.wedge A B C ↔ (ANG B A C (_ : B ≠ A) (_ : C ≠ A)).value.IsPos

def EuclidGeom.odist' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) : ℝ

Equations

• EuclidGeom.odist' A ray = (EuclidGeom.Vec.det ray.toDir.unitVec) (EuclidGeom.Vec.mkPtPt ray.source A)

theorem EuclidGeom.odist'_eq_zero_iff_exist_real_vec_eq_smul {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} : EuclidGeom.odist' A ray = 0 ↔ ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec

theorem EuclidGeom.odist'_eq_length_mul_sin {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) [h : EuclidGeom.PtNe A ray.source] : EuclidGeom.odist' A ray = { source := ray.source, target := A }.length * EuclidGeom.AngValue.sin (EuclidGeom.Angle.mk_ray_pt ray A (_ : A ≠ ray.source)).value

theorem EuclidGeom.wedge_eq_length_mul_odist' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [bnea : EuclidGeom.PtNe B A] : EuclidGeom.wedge A B C = { source := A, target := B }.length * EuclidGeom.odist' C (RAY A B)

theorem EuclidGeom.odist'_eq_odist'_of_to_dirline_eq_to_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) (ray' : EuclidGeom.Ray P) (h : EuclidGeom.same_dir_line ray ray') : EuclidGeom.odist' A ray = EuclidGeom.odist' A ray'

def EuclidGeom.odist {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (l : α) : ℝ

Equations

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

theorem EuclidGeom.odist_reverse_eq_neg_odist' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) : EuclidGeom.odist A ray.reverse = -EuclidGeom.odist A ray

theorem EuclidGeom.odist_reverse_eq_neg_odist'' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dl : EuclidGeom.DirLine P) : EuclidGeom.odist A dl.reverse = -EuclidGeom.odist A dl

theorem EuclidGeom.odist_reverse_eq_neg_odist {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) : EuclidGeom.odist A (EuclidGeom.DirFig.reverse df) = -EuclidGeom.odist A df

theorem EuclidGeom.wedge_eq_wedge_iff_odist_eq_odist_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] : EuclidGeom.odist C (SEG_nd A B) = EuclidGeom.odist D (SEG_nd A B) ↔ EuclidGeom.wedge A B C = EuclidGeom.wedge A B D

def EuclidGeom.odist_sign {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (df : α) : ℝ

Equations

• EuclidGeom.odist_sign A df = ↑(SignType.sign (EuclidGeom.odist A df))

def EuclidGeom.IsOnLeftSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (df : α) : Prop

Equations

• EuclidGeom.IsOnLeftSide A df = (0 < EuclidGeom.odist A df)

def EuclidGeom.IsOnRightSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (df : α) : Prop

Equations

• EuclidGeom.IsOnRightSide A df = (EuclidGeom.odist A df < 0)

def EuclidGeom.OnLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (df : α) : Prop

Equations

• EuclidGeom.OnLine A df = (EuclidGeom.odist A df = 0)

def EuclidGeom.OffLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (df : α) : Prop

Equations

• EuclidGeom.OffLine A df = ¬EuclidGeom.odist A df = 0

theorem EuclidGeom.online_iff_online {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) : EuclidGeom.OnLine A ray ↔ EuclidGeom.Line.IsOn A ray.toLine

theorem EuclidGeom.online_iff_lies_on_line' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dl : EuclidGeom.DirLine P) : EuclidGeom.Line.IsOn A (EuclidGeom.toLine dl) ↔ EuclidGeom.odist A dl = 0

theorem EuclidGeom.online_iff_lies_on_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) : EuclidGeom.lies_on A (EuclidGeom.toLine df) ↔ EuclidGeom.odist A df = 0

theorem EuclidGeom.off_line_iff_not_online {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) : EuclidGeom.OffLine A df ↔ ¬EuclidGeom.OnLine A df

theorem EuclidGeom.LiesOn_or_LiesOnLeft_or_LiesOnRight {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) : EuclidGeom.lies_on A (EuclidGeom.toLine df) ∨ EuclidGeom.IsOnLeftSide A df ∨ EuclidGeom.IsOnRightSide A df

theorem EuclidGeom.not_LiesOnRight_and_not_LiesOn_Line_of_LiesOnLeft {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.IsOnLeftSide A df) : ¬EuclidGeom.IsOnRightSide A df ∧ ¬EuclidGeom.lies_on A (EuclidGeom.toLine df)

theorem EuclidGeom.not_LiesOnLeft_and_not_LiesOn_Line_of_LiesOnRight {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.IsOnRightSide A df) : ¬EuclidGeom.IsOnLeftSide A df ∧ ¬EuclidGeom.lies_on A (EuclidGeom.toLine df)

theorem EuclidGeom.not_LiesOnLeftt_and_not_LiesOnRight_of_LiesOn_Line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.lies_on A (EuclidGeom.toLine df)) : ¬EuclidGeom.IsOnLeftSide A df ∧ ¬EuclidGeom.IsOnRightSide A df

theorem EuclidGeom.lies_on_of_lies_on_toline {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) : EuclidGeom.lies_on A df → EuclidGeom.lies_on A (EuclidGeom.toLine df)

theorem EuclidGeom.not_LiesOnRight_and_not_LiesOn_of_LiesOnLeft {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.IsOnLeftSide A df) : ¬EuclidGeom.IsOnRightSide A df ∧ ¬EuclidGeom.lies_on A df

theorem EuclidGeom.not_LiesOnLeft_and_not_LiesOn_of_LiesOnRight {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.IsOnRightSide A df) : ¬EuclidGeom.IsOnLeftSide A df ∧ ¬EuclidGeom.lies_on A df

theorem EuclidGeom.not_LiesOnLeft_and_not_LiesOnRight_of_LiesOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.DirFig α P] (df : α) (h : EuclidGeom.lies_on A df) : ¬EuclidGeom.IsOnLeftSide A df ∧ ¬EuclidGeom.IsOnRightSide A df

theorem EuclidGeom.LiesOnLeft_or_LiesOnRight_of_not_LiesOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} {A : P} [EuclidGeom.DirFig α P] {df : α} (h : ¬EuclidGeom.lies_on A (EuclidGeom.toLine df)) : EuclidGeom.IsOnLeftSide A df ∨ EuclidGeom.IsOnRightSide A df

theorem EuclidGeom.not_collinear_of_LiesOnLeft_or_LiesOnRight {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [bnea : EuclidGeom.PtNe B A] (hlr : EuclidGeom.IsOnLeftSide C (RAY A B) ∨ EuclidGeom.IsOnRightSide C (RAY A B)) : ¬EuclidGeom.Collinear A B C

theorem EuclidGeom.oarea_eq_length_mul_odist_div_two {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [bnea : EuclidGeom.PtNe B A] : EuclidGeom.oarea A B C = { source := A, target := B }.length * EuclidGeom.odist C (SEG_nd A B) / 2

theorem EuclidGeom.oarea_eq_oarea_iff_odist_eq_odist_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] : EuclidGeom.odist C (SEG_nd A B) = EuclidGeom.odist D (SEG_nd A B) ↔ EuclidGeom.oarea A B C = EuclidGeom.oarea A B D

theorem EuclidGeom.oarea_eq_sin_mul_length_mul_length_div_two {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [bnea : EuclidGeom.PtNe B A] [cnea : EuclidGeom.PtNe C A] : EuclidGeom.oarea A B C = { source := A, target := B }.length * { source := A, target := C }.length * EuclidGeom.AngValue.sin (ANG B A C).value / 2

theorem EuclidGeom.oarea_eq_zero_iff_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.oarea A B C = 0 ↔ EuclidGeom.Collinear A B C

theorem EuclidGeom.oarea_tri_nd_ne_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (trind : ¬EuclidGeom.Collinear A B C) : EuclidGeom.oarea A B C ≠ 0

theorem EuclidGeom.odist_eq_odist_of_parallel' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) [bnea : EuclidGeom.PtNe B A] (para : EuclidGeom.Parallel (SEG_nd A B) ray) : EuclidGeom.odist A ray = EuclidGeom.odist B ray

theorem EuclidGeom.odist_eq_odist_iff_parallel_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.DirFig α P] (A : P) (B : P) (df : α) [bnea : EuclidGeom.PtNe B A] : EuclidGeom.Parallel (SEG_nd A B) df ↔ EuclidGeom.odist A df = EuclidGeom.odist B df

theorem EuclidGeom.wedge_eq_wedge_iff_parallel_of_ne_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] [dnec : EuclidGeom.PtNe D C] : EuclidGeom.Parallel (SEG_nd A B) (SEG_nd C D) ↔ EuclidGeom.wedge A B C = EuclidGeom.wedge A B D

theorem EuclidGeom.oarea_eq_oarea_iff_parallel_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] [dnec : EuclidGeom.PtNe D C] : EuclidGeom.Parallel (SEG_nd A B) (SEG_nd C D) ↔ EuclidGeom.oarea A B C = EuclidGeom.oarea A B D

def EuclidGeom.term_LiesOnLeft_ : Lean.TrailingParserDescr

Equations

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

def EuclidGeom.term_LiesOnRight_ : Lean.TrailingParserDescr

Equations

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

theorem EuclidGeom.same_sign_of_parallel {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) [bnea : EuclidGeom.PtNe B A] (para : EuclidGeom.Parallel (RAY A B) ray) : EuclidGeom.odist_sign A ray = EuclidGeom.odist_sign B ray

theorem EuclidGeom.same_odist_sign_of_same_odist_sign {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (l : EuclidGeom.DirLine P) (signeq : EuclidGeom.odist_sign A l = EuclidGeom.odist_sign B l) (C : P) : EuclidGeom.Seg.IsOn C { source := A, target := B } → EuclidGeom.odist_sign C l = EuclidGeom.odist_sign A l

theorem EuclidGeom.LiesOnLeft_of_ang_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) [ne : EuclidGeom.PtNe A ray.source] (h : { source := ray.source, dir₁ := ray.toDir, dir₂ := (RAY ray.source A).toDir }.IsPos) : EuclidGeom.IsOnLeftSide A ray

theorem EuclidGeom.SB_class {a : ℝ} {b : ℝ} (apos : a > 0) (bneg : b < 0) : a * b < 0

theorem EuclidGeom.LiesOnRight_of_ang_neg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (ray : EuclidGeom.Ray P) [ne : EuclidGeom.PtNe A ray.source] (h : { source := ray.source, dir₁ := ray.toDir, dir₂ := (RAY ray.source A).toDir }.IsNeg) : EuclidGeom.IsOnRightSide A ray

def EuclidGeom.IsOnSameSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) : Prop

Equations

• EuclidGeom.IsOnSameSide' A B ray = (EuclidGeom.IsOnLeftSide A ray ∧ EuclidGeom.IsOnLeftSide B ray ∨ EuclidGeom.IsOnRightSide A ray ∧ EuclidGeom.IsOnRightSide B ray)

def EuclidGeom.IsOnOppositeSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) : Prop

Equations

• EuclidGeom.IsOnOppositeSide' A B ray = (EuclidGeom.IsOnLeftSide A ray ∧ EuclidGeom.IsOnRightSide B ray ∨ EuclidGeom.IsOnRightSide A ray ∧ EuclidGeom.IsOnLeftSide B ray)

theorem EuclidGeom.LiesOnSameSide'_of_toLine_eq_toLine' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) (ray' : EuclidGeom.Ray P) (h : ray.toLine = ray'.toLine) : EuclidGeom.IsOnSameSide' A B ray → EuclidGeom.IsOnSameSide' A B ray'

theorem EuclidGeom.LiesOnSameSide'_of_toLine_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) (ray' : EuclidGeom.Ray P) (h : ray.toLine = ray'.toLine) : EuclidGeom.IsOnSameSide' A B ray = EuclidGeom.IsOnSameSide' A B ray'

theorem EuclidGeom.LiesOnOppositeSide'_of_toLine_eq_toLine' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) (ray' : EuclidGeom.Ray P) (h : ray.toLine = ray'.toLine) : EuclidGeom.IsOnOppositeSide' A B ray → EuclidGeom.IsOnOppositeSide' A B ray'

theorem EuclidGeom.LiesOnOppositeSide'_of_toLine_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) (ray' : EuclidGeom.Ray P) (h : ray.toLine = ray'.toLine) : EuclidGeom.IsOnOppositeSide' A B ray = EuclidGeom.IsOnOppositeSide' A B ray'

def EuclidGeom.IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) : Prop

Equations

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

def EuclidGeom.IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) : Prop

Equations

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

theorem EuclidGeom.IsOnSameSide_symm' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) : EuclidGeom.IsOnSameSide A B ray → EuclidGeom.IsOnSameSide B A ray

theorem EuclidGeom.IsOnSameSide_symm'' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (l : EuclidGeom.Line P) : EuclidGeom.IsOnSameSide A B l → EuclidGeom.IsOnSameSide B A l

theorem EuclidGeom.IsOnSameSide_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) : EuclidGeom.IsOnSameSide A B l = EuclidGeom.IsOnSameSide B A l

theorem EuclidGeom.IsOnOppositeSide_symm' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (ray : EuclidGeom.Ray P) : EuclidGeom.IsOnOppositeSide A B ray → EuclidGeom.IsOnOppositeSide B A ray

theorem EuclidGeom.IsOnOppositeSide_symm'' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (l : EuclidGeom.Line P) : EuclidGeom.IsOnOppositeSide A B l → EuclidGeom.IsOnOppositeSide B A l

theorem EuclidGeom.IsOnOppositeSide_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) : EuclidGeom.IsOnOppositeSide A B l = EuclidGeom.IsOnOppositeSide B A l

theorem EuclidGeom.IsOnSameSide_trans' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (l : EuclidGeom.Line P) (h₁ : EuclidGeom.IsOnSameSide A B l) (h₂ : EuclidGeom.IsOnSameSide B C l) : EuclidGeom.IsOnSameSide A C l

theorem EuclidGeom.IsOnSameSide_trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (C : P) (l : α) (h₁ : EuclidGeom.IsOnSameSide A B l) (h₂ : EuclidGeom.IsOnSameSide B C l) : EuclidGeom.IsOnSameSide A C l

theorem EuclidGeom.IsOnOppositeSide_of_IsOnOppositeSide_and_IsOnSameSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (l : EuclidGeom.Line P) (h₁ : EuclidGeom.IsOnSameSide A B l) (h₂ : EuclidGeom.IsOnOppositeSide B C l) : EuclidGeom.IsOnOppositeSide A C l

theorem EuclidGeom.IsOnOppositeSide_of_IsOnOppositeSide_and_IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (C : P) (l : α) (h₁ : EuclidGeom.IsOnSameSide A B l) (h₂ : EuclidGeom.IsOnOppositeSide B C l) : EuclidGeom.IsOnOppositeSide A C l

theorem EuclidGeom.IsOnOppositeSide_of_IsOnSameSide_and_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (C : P) (l : α) (h₁ : EuclidGeom.IsOnOppositeSide A B l) (h₂ : EuclidGeom.IsOnSameSide B C l) : EuclidGeom.IsOnOppositeSide A C l

theorem EuclidGeom.IsOnSameSide_of_IsOnOppositeSide_and_IsOnOppositeSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (l : EuclidGeom.Line P) (h₁ : EuclidGeom.IsOnOppositeSide A B l) (h₂ : EuclidGeom.IsOnOppositeSide B C l) : EuclidGeom.IsOnSameSide A C l

theorem EuclidGeom.IsOnSameSide_of_IsOnOppositeSide_and_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (C : P) (l : α) (h₁ : EuclidGeom.IsOnOppositeSide A B l) (h₂ : EuclidGeom.IsOnOppositeSide B C l) : EuclidGeom.IsOnSameSide A C l

theorem EuclidGeom.LiesOnLeft_iff_LiesOnLeft_of_IsOnSameSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (dl : EuclidGeom.DirLine P) (h : EuclidGeom.IsOnSameSide A B dl) : EuclidGeom.IsOnLeftSide A dl → EuclidGeom.IsOnLeftSide B dl

theorem EuclidGeom.LiesOnLeft_iff_LiesOnLeft_of_IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (dl : EuclidGeom.DirLine P) (h : EuclidGeom.IsOnSameSide A B dl) : EuclidGeom.IsOnLeftSide A dl = EuclidGeom.IsOnLeftSide B dl

theorem EuclidGeom.LiesOnLeft_iff_LiesOnLeft_rev_of_IsOnOppositeSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (dl : EuclidGeom.DirLine P) (h : EuclidGeom.IsOnOppositeSide A B dl) : EuclidGeom.IsOnLeftSide A dl → EuclidGeom.IsOnLeftSide B dl.reverse

theorem EuclidGeom.LiesOnLeft_iff_LiesOnLeft_rev_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (dl : EuclidGeom.DirLine P) (h : EuclidGeom.IsOnOppositeSide A B dl) : EuclidGeom.IsOnLeftSide A dl = EuclidGeom.IsOnLeftSide B dl.reverse

theorem EuclidGeom.not_collinear_of_IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnSameSide C D (RAY A B)) : ¬EuclidGeom.Collinear A B C ∧ ¬EuclidGeom.Collinear A B D

theorem EuclidGeom.not_collinear_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) [bnea : EuclidGeom.PtNe B A] (h : EuclidGeom.IsOnOppositeSide C D (RAY A B)) : ¬EuclidGeom.Collinear A B C ∧ ¬EuclidGeom.Collinear A B D

theorem EuclidGeom.lies_on_of_lies_on_toline' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} (A : P) [EuclidGeom.ProjFig α P] (df : α) : EuclidGeom.lies_on A df → EuclidGeom.lies_on A (EuclidGeom.toLine df)

theorem EuclidGeom.not_LiesOn_of_IsOnSameSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) (h : EuclidGeom.IsOnSameSide A B l) : ¬EuclidGeom.lies_on A l

theorem EuclidGeom.not_LiesOn_of_IsOnSameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) (h : EuclidGeom.IsOnSameSide A B l) : ¬EuclidGeom.lies_on A l ∧ ¬EuclidGeom.lies_on B l

theorem EuclidGeom.not_LiesOn_of_IsOnOppositeSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) (h : EuclidGeom.IsOnOppositeSide A B l) : ¬EuclidGeom.lies_on A l

theorem EuclidGeom.not_LiesOn_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] (A : P) (B : P) (l : α) (h : EuclidGeom.IsOnOppositeSide A B l) : ¬EuclidGeom.lies_on A l ∧ ¬EuclidGeom.lies_on B l

theorem EuclidGeom.IsOnSameSide_or_IsOnOppositeSide_of_not_LiesOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (l : EuclidGeom.Line P) (a : ¬EuclidGeom.lies_on A l) (b : ¬EuclidGeom.lies_on B l) : EuclidGeom.IsOnSameSide A B l ∨ EuclidGeom.IsOnOppositeSide A B l

theorem EuclidGeom.ne_of_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] {A : P} {B : P} (l : α) (ha : EuclidGeom.lies_on A l) (hb : ¬EuclidGeom.lies_on B l) : B ≠ A

theorem EuclidGeom.same_side_of_line_passing_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (l : EuclidGeom.Line P) (ha : EuclidGeom.lies_on A l) (hb : ¬EuclidGeom.lies_on B l) (hc : EuclidGeom.lies_int C (RAY A B (_ : B ≠ A))) : EuclidGeom.IsOnSameSide B C l

theorem EuclidGeom.linear_comb_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) {t : ℝ} (h : EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B) : EuclidGeom.Vec.mkPtPt D C = (1 - t) • EuclidGeom.Vec.mkPtPt D A + t • EuclidGeom.Vec.mkPtPt D B

theorem EuclidGeom.L_of_vertices_LL {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} {B : P} {C : P} (al : EuclidGeom.IsOnLeftSide A ray) (bl : EuclidGeom.IsOnLeftSide B ray) (c_on : EuclidGeom.lies_on C { source := A, target := B }) : EuclidGeom.IsOnLeftSide C ray

theorem EuclidGeom.IsOnSameSide_of_vertices_SameSide' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {l : EuclidGeom.Line P} (h : EuclidGeom.IsOnSameSide A B l) (c_on : EuclidGeom.lies_on C { source := A, target := B }) : EuclidGeom.IsOnSameSide C A l

theorem EuclidGeom.IsOnSameSide_of_vertices_SameSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {α : Type u_2} [EuclidGeom.ProjFig α P] {A : P} {B : P} {C : P} {l : α} (h : EuclidGeom.IsOnSameSide A B l) (c_on : EuclidGeom.lies_on C { source := A, target := B }) : EuclidGeom.IsOnSameSide C A l

theorem EuclidGeom.not_IsOnSameSide_of_exist_inx {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (l : EuclidGeom.Line P) (h : EuclidGeom.is_inx C { source := A, target := B } l) : ¬EuclidGeom.IsOnSameSide A B l

theorem EuclidGeom.ne_odist_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ray : EuclidGeom.Ray P} (h : EuclidGeom.IsOnOppositeSide A B ray) : EuclidGeom.odist A ray ≠ EuclidGeom.odist B ray

theorem EuclidGeom.exist_inx_int_of_IsOnOppositeSide {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (l : EuclidGeom.Line P) (h : EuclidGeom.IsOnOppositeSide A B l) : ∃ (C : P), EuclidGeom.is_inx C { source := A, target := B } l ∧ EuclidGeom.lies_int C { source := A, target := B }

def EuclidGeom.term_And_LiesOnSameSide_ : Lean.TrailingParserDescr

Equations

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

def EuclidGeom.term_And_LiesOnOppositeSide_ : Lean.TrailingParserDescr

Equations

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

theorem EuclidGeom.intersect_of_ray_on_left_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray₁ : EuclidGeom.Ray P) (ray₂ : EuclidGeom.Ray P) (h : ray₂.source ≠ ray₁.source) : let ray₀ := RAY ray₁.source ray₂.source h; 0 < (EuclidGeom.Angle.mk_two_ray_of_eq_source ray₀ ray₁ (_ : ray₀.source = ray₀.source)).value.toReal ∧ (EuclidGeom.Angle.mk_two_ray_of_eq_source ray₀ ray₁ (_ : ray₀.source = ray₀.source)).value.toReal < (EuclidGeom.Angle.mk_two_ray_of_eq_source ray₀ ray₂ (_ : ray₀.source = ray₂.source)).value.toReal ∧ (EuclidGeom.Angle.mk_two_ray_of_eq_source ray₀ ray₂ (_ : ray₀.source = ray₂.source)).value.toReal < Real.pi ↔ ∃ (A : P), EuclidGeom.lies_on A ray₁ ∧ EuclidGeom.lies_on A ray₂ ∧ EuclidGeom.IsOnLeftSide A ray₀

theorem EuclidGeom.SB_simp (a : ℝ) (b : ℝ) (h : b ≠ 0) : a + -a / b * b = 0

theorem EuclidGeom.exist_inx_DirLine_Ray_of_source_LiesOnLeft_and_included_ang_neg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) (dl : EuclidGeom.DirLine P) (left : EuclidGeom.IsOnLeftSide ray.source dl) (h : (ray.toDir -ᵥ dl.toDir).IsNeg) : ∃ (C : P), EuclidGeom.is_inx C ray dl ∧ EuclidGeom.lies_int C ray

theorem EuclidGeom.exist_inx_DirLine_Ray_of_source_LiesOnRight_and_included_ang_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) (dl : EuclidGeom.DirLine P) (right : EuclidGeom.IsOnRightSide ray.source dl) (h : (ray.toDir -ᵥ dl.toDir).IsPos) : ∃ (C : P), EuclidGeom.is_inx C ray dl ∧ EuclidGeom.lies_int C ray

theorem EuclidGeom.exist_inx_ray_ray_of_ang_pos_pos_gt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray₁ : EuclidGeom.Ray P) (ray₂ : EuclidGeom.Ray P) [ne : EuclidGeom.PtNe ray₁.source ray₂.source] (h₁ : { source := ray₁.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₁.toDir }.IsPos) (h₂ : { source := ray₂.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₂.toDir }.IsPos) (gt : ({ source := ray₂.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₂.toDir }.value - { source := ray₁.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₁.toDir }.value).IsPos) : ∃ (C : P), EuclidGeom.is_inx C ray₁ ray₂

theorem EuclidGeom.exist_inx_ray_ray_of_ang_neg_neg_lt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray₁ : EuclidGeom.Ray P) (ray₂ : EuclidGeom.Ray P) [ne : EuclidGeom.PtNe ray₁.source ray₂.source] (h₁ : { source := ray₁.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₁.toDir }.IsNeg) (h₂ : { source := ray₂.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₂.toDir }.IsNeg) (lt : ({ source := ray₂.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₂.toDir }.value - { source := ray₁.source, dir₁ := (SEG_nd ray₁.source ray₂.source).toDir, dir₂ := ray₁.toDir }.value).IsNeg) : ∃ (C : P), EuclidGeom.is_inx C ray₁ ray₂