Constructions of an angle #

This document discusses the construction of an angle, their properties, and the relationships between them.

source

def EuclidGeom.Angle.oppo {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) :

EuclidGeom.Angle P

Equations

ang.oppo = { source := ang.source, dir₁ := -ang.dir₁, dir₂ := -ang.dir₂ }

Instances For

source

@[simp]

theorem EuclidGeom.Angle.oppo_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.source = ang.source

source

@[simp]

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

ang.oppo.dir₁ = -ang.dir₁

source

@[simp]

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

ang.oppo.dir₂ = -ang.dir₂

source

@[simp]

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

ang.oppo.proj₁ = ang.proj₁

source

@[simp]

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

ang.oppo.proj₂ = ang.proj₂

source

@[simp]

theorem EuclidGeom.Angle.oppo_value_eq_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.value = ang.value

source

@[simp]

theorem EuclidGeom.Angle.oppo_dvalue_eq_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.dvalue = ang.dvalue

source

@[simp]

theorem EuclidGeom.Angle.oppo_isPos_iff_isPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsPos ↔ ang.IsPos

source

@[simp]

theorem EuclidGeom.Angle.oppo_isNeg_iff_isNeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsNeg ↔ ang.IsNeg

source

@[simp]

theorem EuclidGeom.Angle.oppo_isND_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsND ↔ ang.IsND

source

@[simp]

theorem EuclidGeom.Angle.oppo_isAcu_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsAcu ↔ ang.IsAcu

source

@[simp]

theorem EuclidGeom.Angle.oppo_isObt_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsObt ↔ ang.IsObt

source

@[simp]

theorem EuclidGeom.Angle.oppo_isRt_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.IsRt ↔ ang.IsRt

source

theorem EuclidGeom.Angle.oppo_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.start_ray = ang.start_ray.reverse

source

theorem EuclidGeom.Angle.oppo_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.end_ray = ang.end_ray.reverse

source

theorem EuclidGeom.Angle.oppo_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.start_dirLine = ang.start_dirLine.reverse

source

theorem EuclidGeom.Angle.oppo_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.end_dirLine = ang.end_dirLine.reverse

source

@[simp]

theorem EuclidGeom.Angle.oppo_oppo_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.oppo.oppo = ang

source

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

Prop

Equations

ang₁.IsOppo ang₂ = (ang₁ = ang₂.oppo)

Instances For

source

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

ang₂.IsOppo ang₁

source

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

ang₁.value = ang₂.value

source

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

ang₁.dvalue = ang₂.dvalue

source

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

ang₁.dir₁ = -ang₂.dir₁ ↔ ang₁.dir₂ = -ang₂.dir₂

source

theorem EuclidGeom.Angle.isOppo_of_value_eq_of_dir₁_eq_neg_dir₁_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = -ang₂.dir₁) (hv : ang₁.value = ang₂.value) :

ang₁.IsOppo ang₂

source

theorem EuclidGeom.Angle.isOppo_of_value_eq_of_dir₂_eq_neg_dir₂_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₂ = -ang₂.dir₂) (hv : ang₁.value = ang₂.value) :

ang₁.IsOppo ang₂

source

def EuclidGeom.Angle.suppl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) :

EuclidGeom.Angle P

Equations

ang.suppl = { source := ang.source, dir₁ := ang.dir₂, dir₂ := -ang.dir₁ }

Instances For

source

@[simp]

theorem EuclidGeom.Angle.suppl_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.source = ang.source

source

@[simp]

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

ang.suppl.dir₁ = ang.dir₂

source

@[simp]

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

ang.suppl.dir₂ = -ang.dir₁

source

@[simp]

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

ang.suppl.proj₁ = ang.proj₂

source

@[simp]

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

ang.suppl.proj₂ = ang.proj₁

source

@[simp]

theorem EuclidGeom.Angle.suppl_value_add_value_eq_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.value + ang.value = ∠[Real.pi]

source

@[simp]

theorem EuclidGeom.Angle.suppl_dvalue_eq_neg_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.dvalue = -ang.dvalue

source

@[simp]

theorem EuclidGeom.Angle.suppl_isPos_iff_isPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsPos ↔ ang.IsPos

source

@[simp]

theorem EuclidGeom.Angle.suppl_isNeg_iff_isNeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsNeg ↔ ang.IsNeg

source

@[simp]

theorem EuclidGeom.Angle.suppl_isND_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsND ↔ ang.IsND

source

@[simp]

theorem EuclidGeom.Angle.suppl_isAcu_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsAcu ↔ ang.IsObt

source

@[simp]

theorem EuclidGeom.Angle.suppl_isObt_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsObt ↔ ang.IsAcu

source

@[simp]

theorem EuclidGeom.Angle.suppl_isRt_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.IsRt ↔ ang.IsRt

source

theorem EuclidGeom.Angle.suppl_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.start_ray = ang.end_ray

source

theorem EuclidGeom.Angle.suppl_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.end_ray = ang.start_ray.reverse

source

theorem EuclidGeom.Angle.suppl_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.start_dirLine = ang.end_dirLine

source

theorem EuclidGeom.Angle.suppl_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.end_dirLine = ang.start_dirLine.reverse

source

theorem EuclidGeom.Angle.suppl_suppl_eq_oppo {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.suppl = ang.oppo

source

theorem EuclidGeom.Angle.suppl_oppo_eq_oppo_suppl {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.oppo = ang.oppo.suppl

source

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

Prop

Equations

ang₁.IsSuppl ang₂ = (ang₁ = ang₂.suppl)

Instances For

source

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

ang₁.value + ang₂.value = ∠[Real.pi]

source

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

ang₁.dvalue = -↑ang₂.value

source

theorem EuclidGeom.Angle.dir_eq_rev_dir_iff_of_value_add_eq_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : ang₁.value + ang₂.value = ∠[Real.pi]) :

ang₁.dir₁ = ang₂.dir₂ ↔ ang₁.dir₂ = -ang₂.dir₁

source

theorem EuclidGeom.Angle.isSuppl_of_value_add_eq_pi_of_dir_eq_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = ∠[Real.pi]) :

ang₁.IsSuppl ang₂

source

theorem EuclidGeom.Angle.isSuppl_of_value_add_eq_pi_of_dir_eq_neg_dir_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₂ = -ang₂.dir₁) (hv : ang₁.value + ang₂.value = ∠[Real.pi]) :

ang₁.IsSuppl ang₂

source

def EuclidGeom.Angle.reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) :

EuclidGeom.Angle P

Equations

ang.reverse = { source := ang.source, dir₁ := ang.dir₂, dir₂ := ang.dir₁ }

Instances For

source

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

InvolutiveNeg (EuclidGeom.Angle P)

Equations

EuclidGeom.Angle.instInvolutiveNeg = InvolutiveNeg.mk (_ : ∀ (x : EuclidGeom.Angle P), - -x = - -x)

source

@[simp]

theorem EuclidGeom.Angle.rev_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.source = ang.source

source

@[simp]

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

ang.reverse.dir₁ = ang.dir₂

source

@[simp]

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

ang.reverse.dir₂ = ang.dir₁

source

@[simp]

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

ang.reverse.proj₁ = ang.proj₂

source

@[simp]

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

ang.reverse.proj₂ = ang.proj₁

source

theorem EuclidGeom.Angle.rev_value_eq_neg_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.value = -ang.value

source

theorem EuclidGeom.Angle.rev_dvalue_eq_neg_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.dvalue = -ang.dvalue

source

@[simp]

theorem EuclidGeom.Angle.rev_isPos_iff_isNeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsPos ↔ ang.IsNeg

source

@[simp]

theorem EuclidGeom.Angle.rev_isNeg_iff_isPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsNeg ↔ ang.IsPos

source

@[simp]

theorem EuclidGeom.Angle.rev_isND_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsND ↔ ang.IsND

source

@[simp]

theorem EuclidGeom.Angle.rev_isAcu_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsAcu ↔ ang.IsAcu

source

@[simp]

theorem EuclidGeom.Angle.rev_isObt_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsObt ↔ ang.IsObt

source

@[simp]

theorem EuclidGeom.Angle.rev_isRt_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.IsRt ↔ ang.IsRt

source

theorem EuclidGeom.Angle.rev_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.start_ray = ang.end_ray

source

theorem EuclidGeom.Angle.rev_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.end_ray = ang.start_ray

source

theorem EuclidGeom.Angle.rev_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.start_dirLine = ang.end_dirLine

source

theorem EuclidGeom.Angle.rev_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.end_dirLine = ang.start_dirLine

source

@[simp]

theorem EuclidGeom.Angle.rev_rev_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.reverse = ang

source

theorem EuclidGeom.Angle.rev_suppl_oppo_eq_suppl_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.suppl.oppo = ang.suppl.reverse

source

theorem EuclidGeom.Angle.suppl_rev_oppo_eq_rev_suppl {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.suppl.reverse.oppo = ang.reverse.suppl

source

theorem EuclidGeom.Angle.rev_oppo_eq_oppo_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} :

ang.reverse.oppo = ang.oppo.reverse

source

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

Prop

Equations

ang₁.IsReverse ang₂ = (ang₁ = ang₂.reverse)

Instances For

source

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

ang₁.value = -ang₂.value

source

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

ang₁.dvalue = -ang₂.dvalue

source

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

ang₁.dir₁ = ang₂.dir₂ ↔ ang₁.dir₂ = ang₂.dir₁

source

theorem EuclidGeom.Angle.isReverse_of_value_eq_neg_value_of_dir₁_eq_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value = -ang₂.value) :

ang₁.IsReverse ang₂

source

theorem EuclidGeom.Angle.isReverse_of_value_eq_neg_value_of_dir₂_eq_of_source_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₂ = ang₂.dir₁) (hv : ang₁.value = -ang₂.value) :

ang₁.IsReverse ang₂

source

structure EuclidGeom.IsCorrespondingAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] (ang₁ : EuclidGeom.Angle P) (ang₂ : EuclidGeom.Angle P) :

Prop

start_ray : ang₁.dir₁ = ang₂.dir₁
end_ray : ang₁.end_dirLine = ang₂.end_dirLine

Instances For

source

structure EuclidGeom.IsConsecutiveIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] (ang₁ : EuclidGeom.Angle P) (ang₂ : EuclidGeom.Angle P) :

Prop

start_ray : ang₁.dir₁ = ang₂.dir₁
end_ray : ang₁.end_dirLine = ang₂.end_dirLine.reverse

Instances For

source

structure EuclidGeom.IsAlternateIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] (ang₁ : EuclidGeom.Angle P) (ang₂ : EuclidGeom.Angle P) :

Prop

start_ray : ang₁.dir₁ = -ang₂.dir₁
end_ray : ang₁.end_dirLine = ang₂.end_dirLine.reverse

Instances For

source

theorem EuclidGeom.IsCorrespondingAng.symm {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsCorrespondingAng ang₁ ang₂) :

EuclidGeom.IsCorrespondingAng ang₂ ang₁

source

theorem EuclidGeom.IsConsecutiveIntAng.symm {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsConsecutiveIntAng ang₁ ang₂) :

EuclidGeom.IsConsecutiveIntAng ang₂ ang₁

source

theorem EuclidGeom.IsAlternateIntAng.symm {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsAlternateIntAng ang₁ ang₂) :

EuclidGeom.IsAlternateIntAng ang₂ ang₁

source

theorem EuclidGeom.value_eq_of_isCorrespondingAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsCorrespondingAng ang₁ ang₂) :

ang₁.value = ang₂.value

source

theorem EuclidGeom.dvalue_eq_of_isCorrespondingAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsCorrespondingAng ang₁ ang₂) :

ang₁.dvalue = ang₂.dvalue

source

theorem EuclidGeom.value_eq_value_add_pi_of_isConsecutiveIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsConsecutiveIntAng ang₁ ang₂) :

ang₁.value = ang₂.value + ∠[Real.pi]

source

theorem EuclidGeom.dvalue_eq_of_isConsecutiveIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsConsecutiveIntAng ang₁ ang₂) :

ang₁.dvalue = ang₂.dvalue

source

theorem EuclidGeom.value_eq_of_isAlternateIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsAlternateIntAng ang₁ ang₂) :

ang₁.value = ang₂.value

source

theorem EuclidGeom.dvalue_eq_of_isAlternateIntAng {P : Type u_2} [EuclidGeom.EuclideanPlane P] {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h : EuclidGeom.IsAlternateIntAng ang₁ ang₂) :

ang₁.dvalue = ang₂.dvalue