Baisc definitions of angle as a figure

def EuclidGeom.DirObj.AngDiff {α : Type u_1} {β : Type u_2} [EuclidGeom.DirObj α] [EuclidGeom.DirObj β] (F : α) (G : β) : EuclidGeom.AngValue

The angle value between two directed figures.

Equations

• EuclidGeom.AngDiff F G = EuclidGeom.toDir G -ᵥ EuclidGeom.toDir F

def EuclidGeom.ProjObj.DAngDiff {α : Type u_1} {β : Type u_2} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] (F : α) (G : β) : EuclidGeom.AngDValue

The AngDValue between two figures with projective directions.

Equations

• EuclidGeom.DAngDiff F G = EuclidGeom.toProj G -ᵥ EuclidGeom.toProj F

theorem EuclidGeom.Angle.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Angle P), x = y ↔ x.source = y.source ∧ x.dir₁ = y.dir₁ ∧ x.dir₂ = y.dir₂

theorem EuclidGeom.Angle.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Angle P), x.source = y.source → x.dir₁ = y.dir₁ → x.dir₂ = y.dir₂ → x = y

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

An Angle is a structure of a point $P$ and two directions, which is the angle consists of two rays start at $P$ along with the two specified directions.

• source : P
• dir₁ : EuclidGeom.Dir
• dir₂ : EuclidGeom.Dir

def EuclidGeom.Angle.mk_pt_dir_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (source : P) (dir₁ : EuclidGeom.Dir) (dir₂ : EuclidGeom.Dir) : EuclidGeom.Angle P

Alias of EuclidGeom.Angle.mk.

Equations

• @EuclidGeom.Angle.mk_pt_dir_dir = @EuclidGeom.Angle.mk

def EuclidGeom.Angle.mk_two_ray_of_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (_h : r.source = r'.source) : EuclidGeom.Angle P

Given two rays with the same source, this function returns the angle consists of these two rays.

Equations

• EuclidGeom.Angle.mk_two_ray_of_eq_source r r' _h = { source := r.source, dir₁ := r.toDir, dir₂ := r'.toDir }

def EuclidGeom.Angle.mk_pt_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : EuclidGeom.Angle P

Given vertex $O$ and two distinct points $A$ and $B$, this function returns the angle formed by rays $OA$ and $OB$. We use $\verb|ANG|$ to abbreviate $\verb|Angle.mk_pt_pt_pt|$.

Equations

• ANG A O B h₁ h₂ = { source := O, dir₁ := (VEC_nd O A h₁).toDir, dir₂ := (VEC_nd O B h₂).toDir }

def EuclidGeom.Angle.mk_ray_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : EuclidGeom.Angle P

Equations

• EuclidGeom.Angle.mk_ray_pt r A h = { source := r.source, dir₁ := r.toDir, dir₂ := (VEC_nd r.source A h).toDir }

def EuclidGeom.Angle.mk_pt_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : EuclidGeom.Angle P

Equations

• EuclidGeom.Angle.mk_pt_ray A r h = { source := r.source, dir₁ := (VEC_nd r.source A h).toDir, dir₂ := r.toDir }

def EuclidGeom.Angle.mk_dirline_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l₁ : EuclidGeom.DirLine P) (l₂ : EuclidGeom.DirLine P) (h : ¬EuclidGeom.Parallel l₁ l₂) : EuclidGeom.Angle P

Equations

• EuclidGeom.Angle.mk_dirline_dirline l₁ l₂ h = { source := EuclidGeom.Line.inx l₁.toLine l₂.toLine (_ : ¬EuclidGeom.Parallel l₁.toLine l₂.toLine), dir₁ := l₁.toDir, dir₂ := l₂.toDir }

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

Equations

• ang.value = ang.dir₂ -ᵥ ang.dir₁

@[inline, reducible]

abbrev EuclidGeom.Angle.dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.AngDValue

Equations

• ang.dvalue = ↑ang.value

@[inline, reducible]

abbrev EuclidGeom.Angle.proj₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Proj

Equations

• ang.proj₁ = ang.dir₁.toProj

@[inline, reducible]

abbrev EuclidGeom.Angle.proj₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Proj

Equations

• ang.proj₂ = ang.dir₂.toProj

@[inline, reducible]

abbrev EuclidGeom.Angle.IsPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsPos = ang.value.IsPos

@[inline, reducible]

abbrev EuclidGeom.Angle.IsNeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsNeg = ang.value.IsNeg

@[inline, reducible]

abbrev EuclidGeom.Angle.IsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsND = ang.value.IsND

@[inline, reducible]

abbrev EuclidGeom.Angle.IsAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsAcu = ang.value.IsAcu

@[inline, reducible]

abbrev EuclidGeom.Angle.IsObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsObt = ang.value.IsObt

@[inline, reducible]

abbrev EuclidGeom.Angle.IsRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : Prop

Equations

• ang.IsRt = ang.value.IsRt

@[inline, reducible]

abbrev EuclidGeom.value_of_angle_of_three_point_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : EuclidGeom.AngValue

The value of $\verb|Angle.mk_pt_pt_pt| A O B$. We use ∠ to abbreviate $\verb|Angle.value_of_angle_of_three_point_nd|$.

Equations

• ∠ A O B h₁ h₂ = (ANG A O B h₁ h₂).value

@[inline, reducible]

abbrev EuclidGeom.value_of_angle_of_two_ray_of_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (start_ray : EuclidGeom.Ray P) (end_ray : EuclidGeom.Ray P) (h : start_ray.source = end_ray.source) : EuclidGeom.AngValue

Equations

• EuclidGeom.value_of_angle_of_two_ray_of_eq_source start_ray end_ray h = (EuclidGeom.Angle.mk_two_ray_of_eq_source start_ray end_ray h).value

theorem EuclidGeom.value_of_angle_of_two_ray_of_eq_source_eq_angDiff {P : Type u_1} [EuclidGeom.EuclideanPlane P] (start_ray : EuclidGeom.Ray P) (end_ray : EuclidGeom.Ray P) (h : start_ray.source = end_ray.source) : EuclidGeom.value_of_angle_of_two_ray_of_eq_source start_ray end_ray h = EuclidGeom.AngDiff start_ray end_ray

@[inline, reducible]

abbrev EuclidGeom.value_of_angle_of_pt_dir_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (r : EuclidGeom.Dir) (r' : EuclidGeom.Dir) : EuclidGeom.AngValue

Equations

• EuclidGeom.value_of_angle_of_pt_dir_dir O r r' = { source := O, dir₁ := r, dir₂ := r' }.value

theorem EuclidGeom.value_of_angle_of_pt_dir_dir_eq_angDiff {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (r : EuclidGeom.Dir) (r' : EuclidGeom.Dir) : EuclidGeom.value_of_angle_of_pt_dir_dir O r r' = EuclidGeom.AngDiff r r'

def EuclidGeom.termANG__________ : Lean.ParserDescr

Given vertex $O$ and two distinct points $A$ and $B$, this function returns the angle formed by rays $OA$ and $OB$. We use $\verb|ANG|$ to abbreviate $\verb|Angle.mk_pt_pt_pt|$.

Equations

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

def EuclidGeom.delabAngleMkPtPtPt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Angle.mk_pt_pt_pt

Equations

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

def EuclidGeom.«term∠__________» : Lean.ParserDescr

The value of $\verb|Angle.mk_pt_pt_pt| A O B$. We use ∠ to abbreviate $\verb|Angle.value_of_angle_of_three_point_nd|$.

Equations

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

def EuclidGeom.delabValueOfAngleOfThreePointND : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for value_of_angle_of_three_point_nd

Equations

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

@[inline, reducible]

abbrev EuclidGeom.dvalue_of_angle_of_three_point_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : EuclidGeom.AngDValue

The dvalue of $\verb|Angle.mk_pt_pt_pt| A O B$. We use ∡ to abbreviate $\verb|Angle.dvalue_of_angle_of_three_point_nd|$.

Equations

• ∡ A O B h₁ h₂ = (ANG A O B h₁ h₂).dvalue

def EuclidGeom.«term∡__________» : Lean.ParserDescr

The dvalue of $\verb|Angle.mk_pt_pt_pt| A O B$. We use ∡ to abbreviate $\verb|Angle.dvalue_of_angle_of_three_point_nd|$.

Equations

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

def EuclidGeom.delabDValueOfAngleOfThreePointND : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for value_of_angle_of_three_point_nd

Equations

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

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

Equations

• ang.start_ray = { source := ang.source, toDir := ang.dir₁ }

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

Equations

• ang.end_ray = { source := ang.source, toDir := ang.dir₂ }

theorem EuclidGeom.Angle.start_ray_source_eq_end_ray_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.start_ray.source = ang.end_ray.source

@[simp]

theorem EuclidGeom.Angle.start_ray_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.start_ray.toDir = ang.dir₁

@[simp]

theorem EuclidGeom.Angle.end_ray_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.end_ray.toDir = ang.dir₂

@[simp]

theorem EuclidGeom.Angle.source_eq_start_ray_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.start_ray.source = ang.source

@[simp]

theorem EuclidGeom.Angle.source_eq_end_ray_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.end_ray.source = ang.source

theorem EuclidGeom.Angle.source_lies_on_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.lies_on ang.source ang.start_ray

theorem EuclidGeom.Angle.source_lies_on_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.lies_on ang.source ang.end_ray

theorem EuclidGeom.Angle.start_ray_not_para_end_ray_of_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.IsND) : ¬EuclidGeom.Parallel ang.start_ray ang.end_ray

theorem EuclidGeom.Angle.start_ray_eq_end_ray_of_value_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.value = 0) : ang.start_ray = ang.end_ray

theorem EuclidGeom.Angle.start_ray_eq_end_ray_reverse_of_value_eq_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.value = ∠[Real.pi]) : ang.start_ray = ang.end_ray.reverse

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

Equations

• ang.start_dirLine = EuclidGeom.DirLine.mk_pt_dir ang.source ang.dir₁

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

Equations

• ang.end_dirLine = EuclidGeom.DirLine.mk_pt_dir ang.source ang.dir₂

@[simp]

theorem EuclidGeom.Angle.start_dirLine_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.start_dirLine.toDir = ang.dir₁

@[simp]

theorem EuclidGeom.Angle.end_dirLine_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.end_dirLine.toDir = ang.dir₂

@[simp]

theorem EuclidGeom.Angle.start_ray_toDirLine_eq_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.start_ray.toDirLine = ang.start_dirLine

@[simp]

theorem EuclidGeom.Angle.end_ray_toDirLine_eq_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.end_ray.toDirLine = ang.end_dirLine

theorem EuclidGeom.Angle.source_lies_on_start_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.lies_on ang.source ang.start_dirLine

theorem EuclidGeom.Angle.source_lies_on_end_dirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.lies_on ang.source ang.end_dirLine

theorem EuclidGeom.Angle.start_dirLine_not_para_end_dirLine_of_value_ne_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.value.IsND) : ¬EuclidGeom.Parallel ang.start_dirLine ang.end_dirLine

theorem EuclidGeom.Angle.start_dirLine_eq_end_dirLine_of_value_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.value = 0) : ang.start_dirLine = ang.end_dirLine

theorem EuclidGeom.Angle.start_dirLine_eq_end_dirLine_reverse_of_value_eq_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.value = ∠[Real.pi]) : ang.start_dirLine = ang.end_dirLine.reverse

theorem EuclidGeom.Angle.source_eq_fst_source_of_mk_two_ray_of_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).source = r.source

theorem EuclidGeom.Angle.source_eq_snd_source_of_mk_two_ray_of_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).source = r'.source

@[simp]

theorem EuclidGeom.Angle.mk_two_ray_of_eq_source_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).dir₁ = r.toDir

@[simp]

theorem EuclidGeom.Angle.mk_two_ray_of_eq_source_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).dir₂ = r'.toDir

@[simp]

theorem EuclidGeom.Angle.mk_two_ray_of_eq_source_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).start_ray = r

@[simp]

theorem EuclidGeom.Angle.mk_two_ray_of_eq_source_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).end_ray = r'

theorem EuclidGeom.Angle.mk_two_ray_of_eq_source_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : r.source = r'.source) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r' h).value = r'.toDir -ᵥ r.toDir

@[simp]

theorem EuclidGeom.Angle.same_ray_value_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) : (EuclidGeom.Angle.mk_two_ray_of_eq_source r r (_ : r.source = r.source)).value = 0

@[simp]

theorem EuclidGeom.Angle.mk_pt_pt_pt_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : (ANG A O B ha hb).source = O

@[simp]

theorem EuclidGeom.Angle.mk_pt_pt_pt_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : (ANG A O B ha hb).dir₁ = (VEC_nd O A ha).toDir

@[simp]

theorem EuclidGeom.Angle.mk_pt_pt_pt_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : (ANG A O B ha hb).dir₂ = (VEC_nd O B hb).toDir

@[simp]

theorem EuclidGeom.Angle.mk_pt_pt_pt_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : (ANG A O B ha hb).start_ray = RAY O A ha

@[simp]

theorem EuclidGeom.Angle.mk_pt_pt_pt_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : (ANG A O B ha hb).end_ray = RAY O B hb

@[simp]

theorem EuclidGeom.Angle.neg_value_eq_rev_ang {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} (ha : A ≠ O) (hb : B ≠ O) : -∠ A O B ha hb = ∠ B O A hb ha

theorem EuclidGeom.Angle.neg_value_of_rev_ang {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [h₁ : EuclidGeom.PtNe A O] [h₂ : EuclidGeom.PtNe B O] : ∠ A O B = -∠ B O A

@[simp]

theorem EuclidGeom.Angle.mk_ray_pt_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_ray_pt r A h).source = r.source

@[simp]

theorem EuclidGeom.Angle.mk_ray_pt_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_ray_pt r A h).dir₁ = r.toDir

@[simp]

theorem EuclidGeom.Angle.mk_ray_pt_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_ray_pt r A h).dir₂ = (VEC_nd r.source A h).toDir

@[simp]

theorem EuclidGeom.Angle.mk_ray_pt_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_ray_pt r A h).start_ray = r

@[simp]

theorem EuclidGeom.Angle.mk_ray_pt_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (A : P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_ray_pt r A h).end_ray = RAY r.source A h

@[simp]

theorem EuclidGeom.Angle.mk_pt_ray_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_pt_ray A r h).source = r.source

@[simp]

theorem EuclidGeom.Angle.mk_pt_ray_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_pt_ray A r h).dir₁ = (VEC_nd r.source A h).toDir

@[simp]

theorem EuclidGeom.Angle.mk_pt_ray_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_pt_ray A r h).dir₂ = r.toDir

@[simp]

theorem EuclidGeom.Angle.mk_pt_ray_start_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_pt_ray A r h).start_ray = RAY r.source A h

@[simp]

theorem EuclidGeom.Angle.mk_pt_ray_end_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (r : EuclidGeom.Ray P) (h : A ≠ r.source) : (EuclidGeom.Angle.mk_pt_ray A r h).end_ray = r

def EuclidGeom.Angle.mk_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) (d : EuclidGeom.Dir) : EuclidGeom.Angle P

Equations

• EuclidGeom.Angle.mk_dir₁ ang d = { source := ang.source, dir₁ := ang.dir₁, dir₂ := d }

def EuclidGeom.Angle.mk_dir₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) (d : EuclidGeom.Dir) : EuclidGeom.Angle P

Equations

• EuclidGeom.Angle.mk_dir₂ ang d = { source := ang.source, dir₁ := d, dir₂ := ang.dir₂ }

@[simp]

theorem EuclidGeom.Angle.mk_dir₁_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (d : EuclidGeom.Dir) : (EuclidGeom.Angle.mk_dir₁ ang d).source = ang.source

@[simp]

theorem EuclidGeom.Angle.mk_dir₂_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (d : EuclidGeom.Dir) : (EuclidGeom.Angle.mk_dir₂ ang d).source = ang.source

theorem EuclidGeom.Angle.mk_dir₁_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (d : EuclidGeom.Dir) : (EuclidGeom.Angle.mk_dir₁ ang d).value = d -ᵥ ang.dir₁

theorem EuclidGeom.Angle.mk_dir₂_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (d : EuclidGeom.Dir) : (EuclidGeom.Angle.mk_dir₂ ang d).value = ang.dir₂ -ᵥ d

theorem EuclidGeom.Angle.mk_dir₁_dir₂_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Angle.mk_dir₁ ang ang.dir₂ = ang

theorem EuclidGeom.Angle.mk_dir₂_dir₁_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Angle.mk_dir₂ ang ang.dir₁ = ang

@[simp]

theorem EuclidGeom.Angle.mk_start_ray_end_ray_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Angle.mk_two_ray_of_eq_source ang.start_ray ang.end_ray (_ : ang.start_ray.source = ang.start_ray.source) = ang

theorem EuclidGeom.Angle.eq_of_lies_int_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} {B : P} (ha : EuclidGeom.lies_int A ang.start_ray) (hb : EuclidGeom.lies_int B ang.end_ray) : ANG A ang.source B (_ : A ≠ ang.start_ray.source) (_ : B ≠ ang.end_ray.source) = ang

theorem EuclidGeom.Angle.value_eq_of_lies_int_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} {B : P} (ha : EuclidGeom.lies_int A ang.start_ray) (hb : EuclidGeom.lies_int B ang.end_ray) : ∠ A ang.source B (_ : A ≠ ang.start_ray.source) (_ : B ≠ ang.end_ray.source) = ang.value

theorem EuclidGeom.Angle.eq_of_lies_on_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} {B : P} [_ha : EuclidGeom.PtNe A ang.source] [_hb : EuclidGeom.PtNe B ang.source] (ha : EuclidGeom.lies_on A ang.start_ray) (hb : EuclidGeom.lies_on B ang.end_ray) : ANG A ang.source B = ang

theorem EuclidGeom.Angle.value_eq_of_lies_on_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} {B : P} [EuclidGeom.PtNe A ang.source] [EuclidGeom.PtNe B ang.source] (ha : EuclidGeom.lies_on A ang.start_ray) (hb : EuclidGeom.lies_on B ang.end_ray) : ∠ A ang.source B = ang.value

theorem EuclidGeom.Angle.eq_of_lies_on_ray_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {O : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [_hc : EuclidGeom.PtNe C O] [_hd : EuclidGeom.PtNe D O] (hc : EuclidGeom.lies_on C (RAY O A)) (hd : EuclidGeom.lies_on D (RAY O B)) : ANG C O D = ANG A O B

theorem EuclidGeom.Angle.value_eq_of_lies_on_ray_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {O : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] [EuclidGeom.PtNe C O] [EuclidGeom.PtNe D O] (hc : EuclidGeom.lies_on C (RAY O A)) (hd : EuclidGeom.lies_on D (RAY O B)) : ∠ C O D = ∠ A O B

theorem EuclidGeom.Angle.mk_ray_pt_eq_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} (h : EuclidGeom.lies_int A ang.end_ray) : EuclidGeom.Angle.mk_ray_pt ang.start_ray A (_ : A ≠ ang.end_ray.source) = ang

theorem EuclidGeom.Angle.mk_ray_pt_eq_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} [_h : EuclidGeom.PtNe A ang.source] (h : EuclidGeom.lies_on A ang.end_ray) : EuclidGeom.Angle.mk_ray_pt ang.start_ray A (_ : A ≠ ang.source) = ang

theorem EuclidGeom.Angle.mk_pt_ray_eq_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} (h : EuclidGeom.lies_int A ang.start_ray) : EuclidGeom.Angle.mk_pt_ray A ang.end_ray (_ : A ≠ ang.start_ray.source) = ang

theorem EuclidGeom.Angle.mk_pt_ray_eq_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} [_h : EuclidGeom.PtNe A ang.source] (h : EuclidGeom.lies_on A ang.start_ray) : EuclidGeom.Angle.mk_pt_ray A ang.end_ray (_ : A ≠ ang.source) = ang

theorem EuclidGeom.Angle.mk_start_dirLine_end_dirLine_eq_self_of_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} (h : ang.IsND) : EuclidGeom.Angle.mk_dirline_dirline ang.start_dirLine ang.end_dirLine (_ : ¬EuclidGeom.Parallel ang.start_dirLine ang.end_dirLine) = ang

theorem EuclidGeom.Angle.dvalue_eq_of_lies_on_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {A : P} {B : P} [EuclidGeom.PtNe A ang.source] [EuclidGeom.PtNe B ang.source] (ha : EuclidGeom.lies_on A ang.start_ray.toLine) (hb : EuclidGeom.lies_on B ang.end_ray.toLine) : ∡ A ang.source B = ang.dvalue

theorem EuclidGeom.Angle.dvalue_eq_of_lies_on_line_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {O : P} [_ha : EuclidGeom.PtNe A O] [_hb : EuclidGeom.PtNe B O] [_hc : EuclidGeom.PtNe C O] [_hd : EuclidGeom.PtNe D O] (hc : EuclidGeom.lies_on C (LIN O A)) (hd : EuclidGeom.lies_on D (LIN O B)) : ∡ C O D = ∡ A O B

theorem EuclidGeom.Angle.dir_eq_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₂

theorem EuclidGeom.Angle.eq_of_value_eq_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) (hr : ang₁.dir₁ = ang₂.dir₁) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂

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

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

theorem EuclidGeom.Angle.eq_of_value_eq_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) (hr : ang₁.dir₂ = ang₂.dir₂) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂

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

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

theorem EuclidGeom.Angle.angDiff_eq_zero_of_same_dir {dir₁ : EuclidGeom.Dir} {dir₂ : EuclidGeom.Dir} (h : dir₁ = dir₂) : EuclidGeom.AngDiff dir₁ dir₂ = 0

theorem EuclidGeom.Angle.same_dir_iff_value_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.dir₁ = ang.dir₂ ↔ ang.value = 0

@[simp]

theorem EuclidGeom.Angle.pt_pt_pt_value_eq_zero_of_same_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) [EuclidGeom.PtNe A O] : ∠ A O A = 0

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

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

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

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

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

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₁.dir₁ = ang₂.dir₂) (h₂ : ang₁.dir₂ = -ang₂.dir₁) : ang₁.value + ang₂.value = ∠[Real.pi]

theorem EuclidGeom.Angle.value_toReal_le_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.value.toReal ≤ Real.pi

theorem EuclidGeom.Angle.neg_pi_lt_value_toReal {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : -Real.pi < ang.value.toReal

theorem EuclidGeom.Angle.dir₂_eq_value_vadd_dir₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.dir₂ = ang.value +ᵥ ang.dir₁

theorem EuclidGeom.Angle.dvalue_eq_dAngDiff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.dvalue = EuclidGeom.DAngDiff ang.proj₁ ang.proj₂

theorem EuclidGeom.Angle.dvalue_eq_vsub {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.dvalue = ang.proj₂ -ᵥ ang.proj₁

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

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

theorem EuclidGeom.Angle.dAngDiff_eq_zero_of_same_proj {proj₁ : EuclidGeom.Proj} {proj₂ : EuclidGeom.Proj} (h : proj₁ = proj₂) : EuclidGeom.DAngDiff proj₁ proj₂ = 0

theorem EuclidGeom.Angle.same_proj_iff_dvalue_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.proj₁ = ang.proj₂ ↔ ang.dvalue = 0

theorem EuclidGeom.Angle.same_proj_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.proj₁ = ang.proj₂ ↔ ¬ang.IsND

@[simp]

theorem EuclidGeom.Angle.pt_pt_pt_dvalue_eq_zero_of_same_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) [EuclidGeom.PtNe A O] : ∡ A O A = 0

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

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

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

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

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

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

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₁.dir₁ = ang₂.dir₂) (h₂ : ang₁.dir₂ = -ang₂.dir₁) : ang₁.dvalue = -ang₂.dvalue

theorem EuclidGeom.Angle.dir_perp_iff_dvalue_eq_pi_div_two {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Perpendicular ang.dir₁ ang.dir₂ ↔ ang.dvalue = ↑∠[Real.pi / 2]

theorem EuclidGeom.Angle.line_pt_pt_perp_iff_dvalue_eq_pi_div_two {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : EuclidGeom.Perpendicular (LIN O A) (LIN O B) ↔ ∡ A O B = ↑∠[Real.pi / 2]

theorem EuclidGeom.Angle.dir_perp_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Perpendicular ang.dir₁ ang.dir₂ ↔ ang.IsRt

theorem EuclidGeom.Angle.line_pt_pt_perp_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : EuclidGeom.Perpendicular (LIN O A) (LIN O B) ↔ (ANG A O B).IsRt

theorem EuclidGeom.Angle.value_eq_pi_of_lies_int_seg_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [EuclidGeom.PtNe C A] (h : EuclidGeom.lies_int B (SEG_nd A C)) : ∠ A B C (_ : (↑(SEG_nd A C)).source ≠ B) (_ : (↑(SEG_nd A C)).target ≠ B) = ∠[Real.pi]

theorem EuclidGeom.Angle.collinear_iff_dvalue_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : EuclidGeom.Collinear O A B ↔ ∡ A O B = 0

theorem EuclidGeom.Angle.collinear_iff_not_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : EuclidGeom.Collinear O A B ↔ ¬(ANG A O B).IsND

theorem EuclidGeom.Angle.not_collinear_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : ¬EuclidGeom.Collinear O A B ↔ (ANG A O B).IsND

theorem EuclidGeom.Angle.collinear_of_angle_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] (h : ∠ A O B = 0) : EuclidGeom.Collinear O A B

theorem EuclidGeom.Angle.collinear_of_angle_eq_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {O : P} {B : P} [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] (h : ∠ A O B = ∠[Real.pi]) : EuclidGeom.Collinear O A B

theorem EuclidGeom.Angle.sin_pos_iff_isPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : 0 < EuclidGeom.AngValue.sin ang.value ↔ ang.IsPos

theorem EuclidGeom.Angle.sin_neg_iff_isNeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.sin ang.value < 0 ↔ ang.IsNeg

theorem EuclidGeom.Angle.sin_ne_zero_iff_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.sin ang.value ≠ 0 ↔ ang.IsND

theorem EuclidGeom.Angle.sin_eq_zero_iff_not_isND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.sin ang.value = 0 ↔ ¬ang.IsND

theorem EuclidGeom.Angle.cos_pos_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : 0 < EuclidGeom.AngValue.cos ang.value ↔ ang.IsAcu

theorem EuclidGeom.Angle.cos_neg_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.cos ang.value < 0 ↔ ang.IsObt

theorem EuclidGeom.Angle.cos_ne_zero_iff_not_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.cos ang.value ≠ 0 ↔ ¬ang.IsRt

theorem EuclidGeom.Angle.cos_eq_zero_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.AngValue.cos ang.value = 0 ↔ ang.IsRt

theorem EuclidGeom.Angle.inner_eq_dist_mul_cos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : inner (EuclidGeom.Vec.mkPtPt O A) (EuclidGeom.Vec.mkPtPt O B) = dist O A * dist O B * EuclidGeom.AngValue.cos (∠ A O B)

theorem EuclidGeom.Angle.inner_pos_iff_isAcu {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : 0 < inner (EuclidGeom.Vec.mkPtPt O A) (EuclidGeom.Vec.mkPtPt O B) ↔ (∠ A O B).IsAcu

theorem EuclidGeom.Angle.inner_eq_zero_iff_isRt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : inner (EuclidGeom.Vec.mkPtPt O A) (EuclidGeom.Vec.mkPtPt O B) = 0 ↔ (∠ A O B).IsRt

theorem EuclidGeom.Angle.inner_neg_iff_isObt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) (B : P) [EuclidGeom.PtNe A O] [EuclidGeom.PtNe B O] : inner (EuclidGeom.Vec.mkPtPt O A) (EuclidGeom.Vec.mkPtPt O B) < 0 ↔ (∠ A O B).IsObt