EuclideanGeometry.Foundation.Axiom.Position.Angle

instance EuclidGeom.Angle.instAddSemigroup {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

Equations

EuclidGeom.Angle.instAddSemigroup = AddSemigroup.mk (_ : ∀ (x x_1 x_2 : EuclidGeom.Angle P), x + x_1 + x_2 = x + x_1 + x_2)

theorem EuclidGeom.Angle.add_source_eq_source_left {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).source = ang₁.source

source

theorem EuclidGeom.Angle.add_source_eq_source_right {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ + ang₂).source = ang₂.source

source

@[simp]

theorem EuclidGeom.Angle.add_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).dir₁ = ang₁.dir₁

source

@[simp]

theorem EuclidGeom.Angle.add_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).dir₂ = ang₂.dir₂

source

@[simp]

theorem EuclidGeom.Angle.add_proj₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).proj₁ = ang₁.proj₁

source

@[simp]

theorem EuclidGeom.Angle.add_proj₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).proj₂ = ang₂.proj₂

source

@[simp]

theorem EuclidGeom.Angle.add_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).start_ray = ang₁.start_ray

source

theorem EuclidGeom.Angle.add_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ + ang₂).end_ray = ang₂.end_ray

source

@[simp]

theorem EuclidGeom.Angle.add_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ + ang₂).start_dirLine = ang₁.start_dirLine

source

theorem EuclidGeom.Angle.add_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ + ang₂).end_dirLine = ang₂.end_dirLine

source

theorem EuclidGeom.Angle.add_value_eq_value_add_of_dir_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.dir₂ = ang₂.dir₁) :

(ang₁ + ang₂).value = ang₁.value + ang₂.value

source

theorem EuclidGeom.Angle.add_dvalue_eq_dvalue_add_of_proj_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.proj₂ = ang₂.proj₁) :

(ang₁ + ang₂).dvalue = ang₁.dvalue + ang₂.dvalue

source

theorem EuclidGeom.Angle.value_add_eq_add_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∠ A O C + ∠ C O B = ∠ A O B

source

theorem EuclidGeom.Angle.dvalue_add_eq_add_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∡ A O C + ∡ C O B = ∡ A O B

source

theorem EuclidGeom.Angle.value_sub_right_eq_sub_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∠ A O C - ∠ B O C = ∠ A O B

source

theorem EuclidGeom.Angle.dvalue_sub_right_eq_sub_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∡ A O C - ∡ B O C = ∡ A O B

source

theorem EuclidGeom.Angle.value_sub_left_eq_sub_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∠ C O B - ∠ C O A = ∠ A O B

source

theorem EuclidGeom.Angle.dvalue_sub_left_eq_sub_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) (C : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] :

∡ C O B - ∡ C O A = ∡ A O B

source

instance EuclidGeom.Angle.instSub {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

Sub (EuclidGeom.Angle P)

Equations

EuclidGeom.Angle.instSub = { sub := fun (ang₁ ang₂ : EuclidGeom.Angle P) => { source := ang₁.source, dir₁ := ang₁.dir₁, dir₂ := ang₂.dir₁ } }

source

theorem EuclidGeom.Angle.sub_eq_add_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang₁ : EuclidGeom.Angle P) (ang₂ : EuclidGeom.Angle P) :

ang₁ - ang₂ = ang₁ + ang₂.reverse

source

theorem EuclidGeom.Angle.sub_source_eq_source_left {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).source = ang₁.source

source

theorem EuclidGeom.Angle.sub_source_eq_source_right {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ - ang₂).source = ang₂.source

source

@[simp]

theorem EuclidGeom.Angle.sub_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).dir₁ = ang₁.dir₁

source

@[simp]

theorem EuclidGeom.Angle.sub_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).dir₂ = ang₂.dir₁

source

@[simp]

theorem EuclidGeom.Angle.sub_proj₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).proj₁ = ang₁.proj₁

source

@[simp]

theorem EuclidGeom.Angle.sub_proj₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).proj₂ = ang₂.proj₁

source

@[simp]

theorem EuclidGeom.Angle.sub_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).start_ray = ang₁.start_ray

source

theorem EuclidGeom.Angle.sub_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ - ang₂).end_ray = ang₂.start_ray

source

@[simp]

theorem EuclidGeom.Angle.sub_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} :

(ang₁ - ang₂).start_dirLine = ang₁.start_dirLine

source

theorem EuclidGeom.Angle.sub_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.source = ang₂.source) :

(ang₁ - ang₂).end_dirLine = ang₂.start_dirLine

source

theorem EuclidGeom.Angle.sub_value_eq_value_sub_of_dir_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.dir₂ = ang₂.dir₂) :

(ang₁ - ang₂).value = ang₁.value - ang₂.value

source

theorem EuclidGeom.Angle.sub_dvalue_eq_dvalue_sub_of_proj_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.proj₂ = ang₂.proj₂) :

(ang₁ - ang₂).dvalue = ang₁.dvalue - ang₂.dvalue

source

theorem EuclidGeom.Angle.dvalue_eq_pi_div_two_at_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [_h : EuclidGeom.PtNe A O] {l : EuclidGeom.Line P} (ha : EuclidGeom.lies_on A l) (ho : O = EuclidGeom.perp_foot B l) (hb : ¬EuclidGeom.lies_on B l) :

∡ A O B = ↑∠[Real.pi / 2]

source

theorem EuclidGeom.Angle.isRt_at_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [_h : EuclidGeom.PtNe A O] {l : EuclidGeom.Line P} (ha : EuclidGeom.lies_on A l) (ho : O = EuclidGeom.perp_foot B l) (hb : ¬EuclidGeom.lies_on B l) :

(ANG A O B).IsRt

source

theorem EuclidGeom.Angle.perp_foot_lies_int_start_ray_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] :

EuclidGeom.lies_int (EuclidGeom.perp_foot B (LIN O A)) (RAY O A) ↔ (ANG A O B).IsAcu

source

theorem EuclidGeom.Angle.perp_foot_eq_source_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] :

EuclidGeom.perp_foot B (LIN O A) = O ↔ (ANG A O B).IsRt

source

theorem EuclidGeom.Angle.perp_foot_lies_int_start_ray_reverse_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] :

EuclidGeom.lies_int (EuclidGeom.perp_foot B (LIN O A)) (RAY O A).reverse ↔ (ANG A O B).IsObt