Documentation

EuclideanGeometry.Foundation.Axiom.Basic.Angle

Angle Conversions #

Recall in Euclidean Geometry, the measure of angle is subtle. The measure of an angle can be treated as a number in ℝ⧸2π, (- π, π], [0, 2π), ℝ⧸π, or even [0, π] (after taking abs). Each of them has their own suitable applications.

ℝ⧸2π : add and sub of angles, angle between dirrcted object;
(- π, π] : measure of oriented angle, angles of a triangle, positions;
[0, 2π) : length of arc, central angle;
ℝ⧸π : measure of directed angle when discussing four points concyclic, angle between lines
[0, π] : cosine theorem, undirected angles.

In this file, we define suitable coversion function between ℝ⧸2π,ℝ⧸π and (- π, π]. Starting from Dir.toAngValue, we convert Dir to AngValue. We shall primarily use ℝ/2π, and gives coercion and compatibility theorems with respect to ℝ⧸π and (- π, π].

def EuclidGeom.AngDValue :

Equations

EuclidGeom.AngDValue = AddCircle Real.pi

Instances For

instance EuclidGeom.AngDValue.instNormedAddCommGroupAngDValue :

NormedAddCommGroup EuclidGeom.AngDValue

Equations

EuclidGeom.AngDValue.instNormedAddCommGroupAngDValue = inferInstanceAs (NormedAddCommGroup (AddCircle Real.pi))

instance EuclidGeom.AngDValue.instInhabitedAngDValue :

Inhabited EuclidGeom.AngDValue

Equations

EuclidGeom.AngDValue.instInhabitedAngDValue = inferInstanceAs (Inhabited (AddCircle Real.pi))

instance EuclidGeom.AngDValue.instCircularOrderedAddCommGroup :

CircularOrderedAddCommGroup EuclidGeom.AngDValue

Equations

EuclidGeom.AngDValue.instCircularOrderedAddCommGroup = QuotientAddGroup.instCircularOrderedAddCommGroup ℝ

def EuclidGeom.AngValue.toAngDValue :

EuclidGeom.AngValue → EuclidGeom.AngDValue

Equations

EuclidGeom.AngValue.toAngDValue = Quotient.map' id EuclidGeom.AngValue.toAngDValue.proof_1

Instances For

instance EuclidGeom.AngDValue.instCoeAngValueAngDValue :

Coe EuclidGeom.AngValue EuclidGeom.AngDValue

Equations

EuclidGeom.AngDValue.instCoeAngValueAngDValue = { coe := EuclidGeom.AngValue.toAngDValue }

def EuclidGeom.AngValue.toAngDValueHom :

EuclidGeom.AngValue →+ EuclidGeom.AngDValue

Equations

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

Instances For

instance EuclidGeom.AngDValue.instCircularOrderAngDValue :

CircularOrder EuclidGeom.AngDValue

Equations

EuclidGeom.AngDValue.instCircularOrderAngDValue = QuotientAddGroup.circularOrder

theorem EuclidGeom.AngDValue.coe_def (x : ℝ) :

↑∠[x] = ↑x

theorem EuclidGeom.AngDValue.continuous_coe :

Continuous fun (x : ℝ) => ↑∠[x]

def Real.toAngDValueHom :

ℝ →+ EuclidGeom.AngDValue

Coercion ℝ → AngDValue as an additive homomorphism.

Equations

Real.toAngDValueHom = AddMonoidHom.comp EuclidGeom.AngValue.toAngDValueHom EuclidGeom.AngValue.coeHom

Instances For

@[simp]

theorem EuclidGeom.AngDValue.coe_toAngDValueHom :

⇑Real.toAngDValueHom = fun (x : ℝ) => ↑∠[x]

theorem EuclidGeom.AngDValue.induction_on {p : EuclidGeom.AngDValue → Prop} (θ : EuclidGeom.AngDValue) (h : ∀ (x : EuclidGeom.AngValue), p ↑x) :

p θ

An induction principle to deduce results for AngDValue from those for ℝ, used with induction θ using AngDValue.induction_on.

@[simp]

theorem EuclidGeom.AngDValue.coe_zero :

↑0 = 0

@[simp]

theorem EuclidGeom.AngDValue.coe_add_coe (x : ℝ) (y : ℝ) :

↑(∠[x] + ∠[y]) = ↑∠[x] + ↑∠[y]

@[simp]

theorem EuclidGeom.AngDValue.coe_neg_coe (x : ℝ) :

↑(-∠[x]) = -↑∠[x]

@[simp]

theorem EuclidGeom.AngDValue.coe_sub_coe (x : ℝ) (y : ℝ) :

↑(∠[x] - ∠[y]) = ↑∠[x] - ↑∠[y]

@[simp]

theorem EuclidGeom.AngDValue.coe_nsmul_coe (n : ℕ) (x : ℝ) :

↑(n • ∠[x]) = n • ↑∠[x]

@[simp]

theorem EuclidGeom.AngDValue.coe_zsmul_coe (z : ℤ) (x : ℝ) :

↑(z • ∠[x]) = z • ↑∠[x]

@[simp]

theorem EuclidGeom.AngDValue.coe_add (x : EuclidGeom.AngValue) (y : EuclidGeom.AngValue) :

↑(x + y) = ↑x + ↑y

@[simp]

theorem EuclidGeom.AngDValue.coe_neg (x : EuclidGeom.AngValue) :

↑(-x) = -↑x

@[simp]

theorem EuclidGeom.AngDValue.coe_sub (x : EuclidGeom.AngValue) (y : EuclidGeom.AngValue) :

↑(x - y) = ↑x - ↑y

@[simp]

theorem EuclidGeom.AngDValue.coe_nsmul (n : ℕ) (x : EuclidGeom.AngValue) :

↑(n • x) = n • ↑x

@[simp]

theorem EuclidGeom.AngDValue.coe_zsmul (z : ℤ) (x : EuclidGeom.AngValue) :

↑(z • x) = z • ↑x

theorem EuclidGeom.AngDValue.eq_iff_pi_dvd_sub {ψ : ℝ} {θ : ℝ} :

↑∠[θ] = ↑∠[ψ] ↔ ∃ (k : ℤ), θ - ψ = Real.pi * ↑k

@[simp]

theorem EuclidGeom.AngDValue.coe_pi :

↑∠[Real.pi] = 0

@[simp]

theorem EuclidGeom.AngDValue.coe_neg_pi_div_two :

↑∠[-Real.pi / 2] = ↑∠[Real.pi / 2]

@[simp]

theorem EuclidGeom.AngDValue.neg_coe_pi_div_two :

-↑∠[Real.pi / 2] = ↑∠[Real.pi / 2]

@[simp]

theorem EuclidGeom.AngDValue.two_nsmul_coe_div_two (θ : ℝ) :

2 • ↑∠[θ / 2] = ↑∠[θ]

@[simp]

theorem EuclidGeom.AngDValue.two_zsmul_coe_div_two (θ : ℝ) :

2 • ↑∠[θ / 2] = ↑∠[θ]

theorem EuclidGeom.AngValue.coe_eq_coe_iff {θ₁ : EuclidGeom.AngValue} {θ₂ : EuclidGeom.AngValue} :

↑θ₁ = ↑θ₂ ↔ θ₁ = θ₂ ∨ θ₁ = θ₂ + ∠[Real.pi]

theorem EuclidGeom.AngValue.coe_eq_coe_iff_two_nsmul_eq {θ₁ : EuclidGeom.AngValue} {θ₂ : EuclidGeom.AngValue} :

↑θ₁ = ↑θ₂ ↔ 2 • θ₁ = 2 • θ₂

@[simp]

theorem EuclidGeom.AngValue.coe_add_pi {θ : EuclidGeom.AngValue} :

↑(θ + ∠[Real.pi]) = ↑θ

theorem EuclidGeom.AngValue.coe_eq_zero_iff {θ : EuclidGeom.AngValue} :

↑θ = 0 ↔ θ = 0 ∨ θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.coe_eq_pi_div_two_iff {θ : EuclidGeom.AngValue} :

↑θ = ↑∠[Real.pi / 2] ↔ θ = ∠[Real.pi / 2] ∨ θ = ∠[-Real.pi / 2]

@[inline, reducible]

abbrev EuclidGeom.AngDValue.lift {α : Sort u_1} (f : EuclidGeom.AngValue → α) (hf : ∀ (θ : EuclidGeom.AngValue), f (θ + ∠[Real.pi]) = f θ) :

EuclidGeom.AngDValue → α

Equations

EuclidGeom.AngDValue.lift f hf = Quotient.lift (fun (v : ℝ) => f ∠[v]) (_ : ∀ (v₁ v₂ : ℝ), v₁ ≈ v₂ → (fun (v : ℝ) => f ∠[v]) v₁ = (fun (v : ℝ) => f ∠[v]) v₂)

Instances For

def EuclidGeom.piNotation :

Lean.ParserDescr

Equations

EuclidGeom.piNotation = Lean.ParserDescr.node `EuclidGeom.piNotation 1024 (Lean.ParserDescr.symbol "π")

Instances For

def EuclidGeom.piNotationImpl :

Equations

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

Instances For

def EuclidGeom.«term∠[_]» :

Lean.ParserDescr

The canonical map from ℝ to the quotient AngValue.

Equations

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

Instances For

def EuclidGeom.delabAngValueCoe :

Lean.PrettyPrinter.Delaborator.Delab

Delaborator for AngValue.coe

Equations

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

Instances For

def EuclidGeom.«term∡[_]» :

Lean.ParserDescr

Equations

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

Instances For

theorem EuclidGeom.AngValue.toReal_lt_pi_of_ne_pi {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

θ.toReal < Real.pi

theorem EuclidGeom.AngValue.neg_pi_lt_toReal_le_pi {θ : EuclidGeom.AngValue} :

-Real.pi < θ.toReal ∧ θ.toReal ≤ Real.pi

theorem EuclidGeom.AngValue.eq_coe_of_toReal_eq {θ : EuclidGeom.AngValue} {x : ℝ} (h : θ.toReal = x) :

θ = ∠[x]

theorem EuclidGeom.AngValue.neg_pi_le_toReal {θ : EuclidGeom.AngValue} :

-Real.pi ≤ θ.toReal

instance EuclidGeom.AngValue.instCircularOrderedAddCommGroup :

CircularOrderedAddCommGroup EuclidGeom.AngValue

Equations

EuclidGeom.AngValue.instCircularOrderedAddCommGroup = QuotientAddGroup.instCircularOrderedAddCommGroup ℝ

@[simp]

theorem EuclidGeom.AngValue.toReal_coe_eq_self {r : ℝ} (h₁ : -Real.pi < r) (h₂ : r ≤ Real.pi) :

∠[r].toReal = r

theorem EuclidGeom.AngValue.coe_eq_iff {r : ℝ} {s : ℝ} :

∠[r] = ∠[s] ↔ ∃ (k : ℤ), r - s = ↑k * (2 * Real.pi)

theorem EuclidGeom.AngValue.toReal_coe_eq_self_add_two_mul_int_mul_pi (r : ℝ) :

∃ (k : ℤ), ∠[r].toReal = r + ↑k * (2 * Real.pi)

theorem EuclidGeom.AngValue.coe_eq_of_add_two_mul_int_mul_pi {r₁ : ℝ} {r₂ : ℝ} (k : ℤ) (h : r₁ = r₂ + ↑k * (2 * Real.pi)) :

∠[r₁] = ∠[r₂]

@[simp]

theorem EuclidGeom.AngValue.add_two_pi (x : ℝ) :

∠[x + 2 * Real.pi] = ∠[x]

@[simp]

theorem EuclidGeom.AngValue.sub_two_pi (x : ℝ) :

∠[x - 2 * Real.pi] = ∠[x]

@[simp]

theorem EuclidGeom.AngValue.neg_toReal {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

(-θ).toReal = -θ.toReal

theorem EuclidGeom.AngValue.pi_div_two_ne_neg_pi_div_two :

∠[Real.pi / 2] ≠ ∠[-Real.pi / 2]

theorem EuclidGeom.AngValue.pi_div_two_ne_pi :

∠[Real.pi / 2] ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.neg_pi_div_two_ne_pi :

∠[-Real.pi / 2] ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.neg_coe_pi_div_two :

-∠[Real.pi / 2] = ∠[-Real.pi / 2]

@[simp]

theorem EuclidGeom.AngValue.two_nsmul_toReal_div_two {θ : EuclidGeom.AngValue} :

2 • ∠[θ.toReal / 2] = θ

@[simp]

theorem EuclidGeom.AngValue.two_zsmul_toReal_div_two {θ : EuclidGeom.AngValue} :

2 • ∠[θ.toReal / 2] = θ

def EuclidGeom.AngValue.IsPos (θ : EuclidGeom.AngValue) :

An angle is positive if it is strictly between 0 and π.

Equations

θ.IsPos = sbtw 0 θ ∠[Real.pi]

Instances For

def EuclidGeom.AngValue.IsNeg (θ : EuclidGeom.AngValue) :

An angle is negative if it is strictly between - π and 0.

Equations

θ.IsNeg = sbtw ∠[Real.pi] θ 0

Instances For

structure EuclidGeom.AngValue.IsND (θ : EuclidGeom.AngValue) :

An angle is non-degenerate if it is not 0 or π.

ne_zero : θ ≠ 0
ne_pi : θ ≠ ∠[Real.pi]

Instances For

theorem EuclidGeom.AngValue.not_zero_isPos :

¬∠[0].IsPos

theorem EuclidGeom.AngValue.not_zero_isNeg :

¬∠[0].IsNeg

theorem EuclidGeom.AngValue.not_zero_isND :

¬∠[0].IsND

theorem EuclidGeom.AngValue.not_isPos_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

¬θ.IsPos

theorem EuclidGeom.AngValue.ne_zero_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

θ ≠ 0

theorem EuclidGeom.AngValue.not_isNeg_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.ne_zero_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

θ ≠ 0

theorem EuclidGeom.AngValue.not_isND_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

¬θ.IsND

theorem EuclidGeom.AngValue.not_pi_isPos :

¬∠[Real.pi].IsPos

theorem EuclidGeom.AngValue.not_pi_isNeg :

¬∠[Real.pi].IsNeg

theorem EuclidGeom.AngValue.not_pi_isND :

¬∠[Real.pi].IsND

theorem EuclidGeom.AngValue.not_isPos_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

¬θ.IsPos

theorem EuclidGeom.AngValue.ne_pi_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

θ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.not_isNeg_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.ne_pi_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

θ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.not_isND_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

¬θ.IsND

theorem EuclidGeom.AngValue.isND_iff {θ : EuclidGeom.AngValue} :

θ.IsND ↔ θ ≠ 0 ∧ θ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.not_isND_iff {θ : EuclidGeom.AngValue} :

¬θ.IsND ↔ θ = 0 ∨ θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.two_nsmul_ne_zero_iff_isND {θ : EuclidGeom.AngValue} :

2 • θ ≠ 0 ↔ θ.IsND

theorem EuclidGeom.AngValue.two_nsmul_eq_zero_iff_not_isND {θ : EuclidGeom.AngValue} :

2 • θ = 0 ↔ ¬θ.IsND

theorem EuclidGeom.AngValue.ne_neg_self_iff_isND {θ : EuclidGeom.AngValue} :

θ ≠ -θ ↔ θ.IsND

theorem EuclidGeom.AngValue.eq_neg_self_iff_not_isND {θ : EuclidGeom.AngValue} :

θ = -θ ↔ ¬θ.IsND

theorem EuclidGeom.AngValue.not_isND_iff_coe {θ : EuclidGeom.AngValue} :

¬θ.IsND ↔ ↑θ = 0

theorem EuclidGeom.AngValue.isND_iff_coe {θ : EuclidGeom.AngValue} :

θ.IsND ↔ ↑θ ≠ 0

theorem EuclidGeom.AngValue.not_isNeg_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.isND_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

θ.IsND

theorem EuclidGeom.AngValue.not_isPos_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

¬θ.IsPos

theorem EuclidGeom.AngValue.isND_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

θ.IsND

theorem EuclidGeom.AngValue.not_isPos_of_not_isND {θ : EuclidGeom.AngValue} (h : ¬θ.IsND) :

¬θ.IsPos

theorem EuclidGeom.AngValue.not_isNeg_of_not_isND {θ : EuclidGeom.AngValue} (h : ¬θ.IsND) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.isND_iff_isPos_or_isNeg {θ : EuclidGeom.AngValue} :

θ.IsND ↔ θ.IsPos ∨ θ.IsNeg

theorem EuclidGeom.AngValue.not_isND_or_isPos_or_isNeg {θ : EuclidGeom.AngValue} :

¬θ.IsND ∨ θ.IsPos ∨ θ.IsNeg

theorem EuclidGeom.AngValue.not_isPos_iff_not_isND_or_isNeg {θ : EuclidGeom.AngValue} :

¬θ.IsPos ↔ ¬θ.IsND ∨ θ.IsNeg

theorem EuclidGeom.AngValue.not_isNeg_iff_not_isND_or_isPos {θ : EuclidGeom.AngValue} :

¬θ.IsNeg ↔ ¬θ.IsND ∨ θ.IsPos

theorem EuclidGeom.AngValue.toReal_nonneg_iff {θ : EuclidGeom.AngValue} :

0 ≤ θ.toReal ↔ btw 0 θ ∠[Real.pi]

theorem EuclidGeom.AngValue.toReal_nonneg_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

0 ≤ θ.toReal

theorem EuclidGeom.AngValue.toReal_pos_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

0 < θ.toReal

theorem EuclidGeom.AngValue.toReal_lt_pi_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

θ.toReal < Real.pi

theorem EuclidGeom.AngValue.toReal_neg_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

θ.toReal < 0

theorem EuclidGeom.AngValue.toReal_nonpos_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

θ.toReal ≤ 0

theorem EuclidGeom.AngValue.isPos_of_toReal_pos_of_ne_pi {θ : EuclidGeom.AngValue} (h : 0 < θ.toReal) (hn : θ ≠ ∠[Real.pi]) :

θ.IsPos

theorem EuclidGeom.AngValue.isNeg_of_toReal_pos {θ : EuclidGeom.AngValue} (h : θ.toReal < 0) :

θ.IsNeg

theorem EuclidGeom.AngValue.isPos_iff {θ : EuclidGeom.AngValue} :

θ.IsPos ↔ 0 < θ.toReal ∧ θ.toReal < Real.pi

theorem EuclidGeom.AngValue.not_isPos_iff {θ : EuclidGeom.AngValue} :

¬θ.IsPos ↔ θ.toReal ≤ 0 ∨ θ.toReal = Real.pi

theorem EuclidGeom.AngValue.isNeg_iff {θ : EuclidGeom.AngValue} :

θ.IsNeg ↔ θ.toReal < 0

theorem EuclidGeom.AngValue.not_isNeg_iff {θ : EuclidGeom.AngValue} :

¬θ.IsNeg ↔ 0 ≤ θ.toReal

theorem EuclidGeom.AngValue.isND_iff' {θ : EuclidGeom.AngValue} :

θ.IsND ↔ θ.toReal ≠ 0 ∧ θ.toReal ≠ Real.pi

theorem EuclidGeom.AngValue.not_isND_iff' {θ : EuclidGeom.AngValue} :

¬θ.IsND ↔ θ.toReal = 0 ∨ θ.toReal = Real.pi

theorem EuclidGeom.AngValue.isNeg_iff_sin_neg {θ : EuclidGeom.AngValue} :

θ.IsNeg ↔ EuclidGeom.AngValue.sin θ < 0

theorem EuclidGeom.AngValue.isND_iff_sin_ne_zero {θ : EuclidGeom.AngValue} :

θ.IsND ↔ EuclidGeom.AngValue.sin θ ≠ 0

theorem EuclidGeom.AngValue.not_isND_iff_sin_eq_zero {θ : EuclidGeom.AngValue} :

¬θ.IsND ↔ EuclidGeom.AngValue.sin θ = 0

theorem EuclidGeom.AngValue.sin_neg_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

EuclidGeom.AngValue.sin θ < 0

theorem EuclidGeom.AngValue.isNeg_of_sin_neg {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.sin θ < 0) :

θ.IsNeg

theorem EuclidGeom.AngValue.sin_eq_zero_of_not_isND {θ : EuclidGeom.AngValue} (h : ¬θ.IsND) :

EuclidGeom.AngValue.sin θ = 0

theorem EuclidGeom.AngValue.not_isND_of_sin_eq_zero {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.sin θ = 0) :

¬θ.IsND

theorem EuclidGeom.AngValue.sin_ne_zero_of_isND {θ : EuclidGeom.AngValue} (h : θ.IsND) :

EuclidGeom.AngValue.sin θ ≠ 0

theorem EuclidGeom.AngValue.isND_of_sin_eq_zero {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.sin θ ≠ 0) :

θ.IsND

theorem EuclidGeom.AngValue.sin_pos_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

0 < EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.isPos_of_sin_pos {θ : EuclidGeom.AngValue} (h : 0 < EuclidGeom.AngValue.sin θ) :

θ.IsPos

theorem EuclidGeom.AngValue.isPos_iff_sin_pos {θ : EuclidGeom.AngValue} :

θ.IsPos ↔ 0 < EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.not_isNeg_iff_sin_nonneg {θ : EuclidGeom.AngValue} :

¬θ.IsNeg ↔ 0 ≤ EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.not_isPos_iff_sin_nonpos {θ : EuclidGeom.AngValue} :

¬θ.IsPos ↔ EuclidGeom.AngValue.sin θ ≤ 0

theorem EuclidGeom.AngValue.pi_div_two_isPos :

∠[Real.pi / 2].IsPos

theorem EuclidGeom.AngValue.pi_div_two_not_isNeg :

¬∠[Real.pi / 2].IsNeg

theorem EuclidGeom.AngValue.pi_div_two_isND :

∠[Real.pi / 2].IsND

theorem EuclidGeom.AngValue.isPos_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

θ.IsPos

theorem EuclidGeom.AngValue.not_isNeg_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.isND_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

θ.IsND

theorem EuclidGeom.AngValue.neg_pi_div_two_isNeg :

∠[-Real.pi / 2].IsNeg

theorem EuclidGeom.AngValue.neg_pi_div_two_not_isPos :

¬∠[-Real.pi / 2].IsPos

theorem EuclidGeom.AngValue.neg_pi_div_two_isND :

∠[-Real.pi / 2].IsND

theorem EuclidGeom.AngValue.isNeg_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

θ.IsNeg

theorem EuclidGeom.AngValue.not_isPos_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

¬θ.IsPos

theorem EuclidGeom.AngValue.isND_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

θ.IsND

@[simp]

theorem EuclidGeom.AngValue.neg_isPos_iff_isNeg {θ : EuclidGeom.AngValue} :

(-θ).IsPos ↔ θ.IsNeg

@[simp]

theorem EuclidGeom.AngValue.neg_isNeg_iff_isPos {θ : EuclidGeom.AngValue} :

(-θ).IsNeg ↔ θ.IsPos

@[simp]

theorem EuclidGeom.AngValue.neg_isND_iff_isND {θ : EuclidGeom.AngValue} :

(-θ).IsND ↔ θ.IsND

theorem EuclidGeom.AngValue.ne_neg_of_isPos {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) :

θ ≠ -ψ

theorem EuclidGeom.AngValue.ne_neg_of_isNeg {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) :

θ ≠ -ψ

theorem EuclidGeom.AngValue.coe_isPos_of_zero_lt_self_lt_pi {x : ℝ} (h0 : 0 < x) (hp : x < Real.pi) :

∠[x].IsPos

theorem EuclidGeom.AngValue.coe_isNeg_of_neg_pi_lt_self_lt_zero {x : ℝ} (hp : -Real.pi < x) (h0 : x < 0) :

∠[x].IsNeg

theorem EuclidGeom.AngValue.coe_not_isNeg_of_zero_le_self_le_pi {x : ℝ} (h0 : 0 ≤ x) (hp : x ≤ Real.pi) :

¬∠[x].IsNeg

@[simp]

theorem EuclidGeom.AngValue.add_pi_isPos_iff_isNeg {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsPos ↔ θ.IsNeg

@[simp]

theorem EuclidGeom.AngValue.add_pi_isNeg_iff_isPos {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsNeg ↔ θ.IsPos

@[simp]

theorem EuclidGeom.AngValue.add_pi_isND_iff_isND {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsND ↔ θ.IsND

theorem EuclidGeom.AngValue.ne_add_pi_of_isPos {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) :

θ ≠ ψ + ∠[Real.pi]

theorem EuclidGeom.AngValue.eq_of_isPos_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) (h : 2 • θ = 2 • ψ) :

θ = ψ

theorem EuclidGeom.AngValue.eq_of_isPos_of_coe_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) (h : ↑θ = ↑ψ) :

θ = ψ

theorem EuclidGeom.AngValue.ne_add_pi_of_isNeg {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) :

θ ≠ ψ + ∠[Real.pi]

theorem EuclidGeom.AngValue.eq_of_isNeg_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) (h : 2 • θ = 2 • ψ) :

θ = ψ

theorem EuclidGeom.AngValue.eq_of_isNeg_of_coe_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) (h : ↑θ = ↑ψ) :

θ = ψ

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isPos_iff_isPos {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsPos ↔ θ.IsPos

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isNeg_iff_isNeg {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsNeg ↔ θ.IsNeg

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isND_iff_isND {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsND ↔ θ.IsND

theorem EuclidGeom.AngValue.isPos_iff_isPos_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsPos ↔ ψ.IsPos

theorem EuclidGeom.AngValue.isNeg_iff_isNeg_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsNeg ↔ ψ.IsNeg

theorem EuclidGeom.AngValue.isND_iff_isND_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsND ↔ ψ.IsND

def EuclidGeom.AngValue.IsAcu (θ : EuclidGeom.AngValue) :

An angle is acute if it is strictly between - π / 2 and π / 2.

Equations

θ.IsAcu = sbtw ∠[-Real.pi / 2] θ ∠[Real.pi / 2]

Instances For

def EuclidGeom.AngValue.IsObt (θ : EuclidGeom.AngValue) :

An angle is obtuse if it is strictly between π / 2 and - π / 2.

Equations

θ.IsObt = sbtw ∠[Real.pi / 2] θ ∠[-Real.pi / 2]

Instances For

def EuclidGeom.AngValue.IsRt (θ : EuclidGeom.AngValue) :

An angle is right if it is - π / 2 or π / 2.

Equations

θ.IsRt = (θ = ∠[-Real.pi / 2] ∨ θ = ∠[Real.pi / 2])

Instances For

theorem EuclidGeom.AngValue.pi_div_two_not_isAcu :

¬∠[Real.pi / 2].IsAcu

theorem EuclidGeom.AngValue.not_isAcu_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

¬θ.IsAcu

theorem EuclidGeom.AngValue.pi_div_two_not_isObt :

¬∠[Real.pi / 2].IsObt

theorem EuclidGeom.AngValue.not_isObt_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

¬θ.IsObt

theorem EuclidGeom.AngValue.pi_div_two_isRt :

∠[Real.pi / 2].IsRt

theorem EuclidGeom.AngValue.isRt_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

θ.IsRt

theorem EuclidGeom.AngValue.neg_pi_div_two_not_isAcu :

¬∠[-Real.pi / 2].IsAcu

theorem EuclidGeom.AngValue.not_isAcu_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

¬θ.IsAcu

theorem EuclidGeom.AngValue.neg_pi_div_two_not_isObt :

¬∠[-Real.pi / 2].IsObt

theorem EuclidGeom.AngValue.not_isObt_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

¬θ.IsObt

theorem EuclidGeom.AngValue.neg_pi_div_two_isRt :

∠[-Real.pi / 2].IsRt

theorem EuclidGeom.AngValue.isRt_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

θ.IsRt

theorem EuclidGeom.AngValue.isRt_iff {θ : EuclidGeom.AngValue} :

θ.IsRt ↔ θ = ∠[Real.pi / 2] ∨ θ = ∠[-Real.pi / 2]

theorem EuclidGeom.AngValue.not_isRt_iff {θ : EuclidGeom.AngValue} :

¬θ.IsRt ↔ θ ≠ ∠[-Real.pi / 2] ∧ θ ≠ ∠[Real.pi / 2]

theorem EuclidGeom.AngValue.isRt_iff_coe {θ : EuclidGeom.AngValue} :

θ.IsRt ↔ ↑θ = ↑∠[Real.pi / 2]

theorem EuclidGeom.AngValue.not_isObt_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

¬θ.IsObt

theorem EuclidGeom.AngValue.not_isAcu_of_isObt {θ : EuclidGeom.AngValue} (h : θ.IsObt) :

¬θ.IsAcu

theorem EuclidGeom.AngValue.not_isAcu_of_not_isRt {θ : EuclidGeom.AngValue} (h : θ.IsRt) :

¬θ.IsAcu

theorem EuclidGeom.AngValue.not_isObt_of_not_isRt {θ : EuclidGeom.AngValue} (h : θ.IsRt) :

¬θ.IsObt

theorem EuclidGeom.AngValue.not_isRt_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

¬θ.IsRt

theorem EuclidGeom.AngValue.not_isRt_of_isObt {θ : EuclidGeom.AngValue} (h : θ.IsObt) :

¬θ.IsRt

theorem EuclidGeom.AngValue.isAcu_or_isNeg_of_isRt {θ : EuclidGeom.AngValue} (h : ¬θ.IsRt) :

θ.IsAcu ∨ θ.IsObt

theorem EuclidGeom.AngValue.not_isRt_or_isAcu_or_isNeg {θ : EuclidGeom.AngValue} :

θ.IsRt ∨ θ.IsAcu ∨ θ.IsObt

theorem EuclidGeom.AngValue.isRt_or_isObt_of_not_isAcu {θ : EuclidGeom.AngValue} (h : ¬θ.IsAcu) :

θ.IsRt ∨ θ.IsObt

theorem EuclidGeom.AngValue.isRt_or_isAcu_of_not_isObt {θ : EuclidGeom.AngValue} (h : ¬θ.IsObt) :

θ.IsRt ∨ θ.IsAcu

theorem EuclidGeom.AngValue.neg_pi_div_two_le_toReal_le_pi_div_two_iff_btw {θ : EuclidGeom.AngValue} :

-Real.pi / 2 ≤ θ.toReal ∧ θ.toReal ≤ Real.pi / 2 ↔ btw ∠[-Real.pi / 2] θ ∠[Real.pi / 2]

theorem EuclidGeom.AngValue.not_isObt_iff {θ : EuclidGeom.AngValue} :

¬θ.IsObt ↔ -Real.pi / 2 ≤ θ.toReal ∧ θ.toReal ≤ Real.pi / 2

theorem EuclidGeom.AngValue.neg_pi_div_two_le_toReal_of_isObt {θ : EuclidGeom.AngValue} (h : ¬θ.IsObt) :

-Real.pi / 2 ≤ θ.toReal

theorem EuclidGeom.AngValue.toReal_le_pi_div_two_of_isObt {θ : EuclidGeom.AngValue} (h : ¬θ.IsObt) :

θ.toReal ≤ Real.pi / 2

theorem EuclidGeom.AngValue.isObt_iff {θ : EuclidGeom.AngValue} :

θ.IsObt ↔ θ.toReal < -Real.pi / 2 ∨ Real.pi / 2 < θ.toReal

theorem EuclidGeom.AngValue.isObt_of_toReal_lt_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ.toReal < -Real.pi / 2) :

θ.IsObt

theorem EuclidGeom.AngValue.isObt_of_pi_div_two_lt_toReal {θ : EuclidGeom.AngValue} (h : Real.pi / 2 < θ.toReal) :

θ.IsObt

theorem EuclidGeom.AngValue.isRt_iff' {θ : EuclidGeom.AngValue} :

θ.IsRt ↔ θ.toReal = -Real.pi / 2 ∨ θ.toReal = Real.pi / 2

theorem EuclidGeom.AngValue.not_isRt_iff' {θ : EuclidGeom.AngValue} :

¬θ.IsRt ↔ θ.toReal ≠ -Real.pi / 2 ∧ θ.toReal ≠ Real.pi / 2

theorem EuclidGeom.AngValue.neg_pi_div_two_le_toReal_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

-Real.pi / 2 ≤ θ.toReal

theorem EuclidGeom.AngValue.neg_pi_div_two_lt_toReal_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

-Real.pi / 2 < θ.toReal

theorem EuclidGeom.AngValue.toReal_le_pi_div_two_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

θ.toReal ≤ Real.pi / 2

theorem EuclidGeom.AngValue.toReal_lt_pi_div_two_of_isAcu {θ : EuclidGeom.AngValue} (h : θ.IsAcu) :

θ.toReal < Real.pi / 2

theorem EuclidGeom.AngValue.isAcu_iff {θ : EuclidGeom.AngValue} :

θ.IsAcu ↔ -Real.pi / 2 < θ.toReal ∧ θ.toReal < Real.pi / 2

theorem EuclidGeom.AngValue.not_isAcu_iff {θ : EuclidGeom.AngValue} :

¬θ.IsAcu ↔ θ.toReal ≤ -Real.pi / 2 ∨ Real.pi / 2 ≤ θ.toReal

theorem EuclidGeom.AngValue.isAcu_iff_cos_pos {θ : EuclidGeom.AngValue} :

θ.IsAcu ↔ 0 < EuclidGeom.AngValue.cos θ

theorem EuclidGeom.AngValue.isObt_iff_cos_neg {θ : EuclidGeom.AngValue} :

θ.IsObt ↔ EuclidGeom.AngValue.cos θ < 0

theorem EuclidGeom.AngValue.isRt_iff_cos_eq_zero {θ : EuclidGeom.AngValue} :

θ.IsRt ↔ EuclidGeom.AngValue.cos θ = 0

theorem EuclidGeom.AngValue.not_isRt_iff_cos_ne_zero {θ : EuclidGeom.AngValue} :

¬θ.IsRt ↔ EuclidGeom.AngValue.cos θ ≠ 0

theorem EuclidGeom.AngValue.zero_isAcu :

0.IsAcu

theorem EuclidGeom.AngValue.zero_not_isObt :

¬0.IsObt

theorem EuclidGeom.AngValue.zero_not_isRt :

¬0.IsRt

theorem EuclidGeom.AngValue.isAcu_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

θ.IsAcu

theorem EuclidGeom.AngValue.not_isObt_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

¬θ.IsObt

theorem EuclidGeom.AngValue.not_isRt_of_eq_zero {θ : EuclidGeom.AngValue} (h : θ = 0) :

¬θ.IsRt

theorem EuclidGeom.AngValue.pi_isObt :

∠[Real.pi].IsObt

theorem EuclidGeom.AngValue.pi_not_isAcu :

¬∠[Real.pi].IsAcu

theorem EuclidGeom.AngValue.pi_not_isRt :

¬∠[Real.pi].IsRt

theorem EuclidGeom.AngValue.isAcu_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

θ.IsObt

theorem EuclidGeom.AngValue.not_isAcu_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

¬θ.IsAcu

theorem EuclidGeom.AngValue.not_isRt_of_eq_pi {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi]) :

¬θ.IsRt

@[simp]

theorem EuclidGeom.AngValue.neg_isAcu_iff_isAcu {θ : EuclidGeom.AngValue} :

(-θ).IsAcu ↔ θ.IsAcu

@[simp]

theorem EuclidGeom.AngValue.neg_isObt_iff_isObt {θ : EuclidGeom.AngValue} :

(-θ).IsObt ↔ θ.IsObt

@[simp]

theorem EuclidGeom.AngValue.neg_isRt_iff_isRt {θ : EuclidGeom.AngValue} :

(-θ).IsRt ↔ θ.IsRt

@[simp]

theorem EuclidGeom.AngValue.add_pi_isAcu_iff_isObt {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsAcu ↔ θ.IsObt

@[simp]

theorem EuclidGeom.AngValue.add_pi_isObt_iff_isAcu {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsObt ↔ θ.IsAcu

@[simp]

theorem EuclidGeom.AngValue.add_pi_isRt_iff_isRt {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi]).IsRt ↔ θ.IsRt

theorem EuclidGeom.AngValue.ne_add_pi_of_isAcu {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsAcu) :

θ ≠ ψ + ∠[Real.pi]

theorem EuclidGeom.AngValue.eq_of_isAcu_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsAcu) (h : 2 • θ = 2 • ψ) :

θ = ψ

theorem EuclidGeom.AngValue.eq_of_isAcu_of_coe_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsAcu) (h : ↑θ = ↑ψ) :

θ = ψ

theorem EuclidGeom.AngValue.ne_add_pi_of_isObt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsObt) (hp : ψ.IsObt) :

θ ≠ ψ + ∠[Real.pi]

theorem EuclidGeom.AngValue.eq_of_isObt_of_two_nsmul_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsObt) (hp : ψ.IsObt) (h : 2 • θ = 2 • ψ) :

θ = ψ

theorem EuclidGeom.AngValue.eq_of_isObt_of_coe_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsObt) (hp : ψ.IsObt) (h : ↑θ = ↑ψ) :

θ = ψ

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isAcu_iff_isObt {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsAcu ↔ θ.IsObt

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isObt_iff_isAcu {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsObt ↔ θ.IsAcu

@[simp]

theorem EuclidGeom.AngValue.pi_sub_isRt_iff_isRt {θ : EuclidGeom.AngValue} :

(∠[Real.pi] - θ).IsRt ↔ θ.IsRt

theorem EuclidGeom.AngValue.add_ne_pi_of_isAcu {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsAcu) :

θ + ψ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.add_ne_pi_of_isObt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsObt) (hp : ψ.IsObt) :

θ + ψ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.isAcu_iff_isObt_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsAcu ↔ ψ.IsObt

theorem EuclidGeom.AngValue.isObt_iff_isAcu_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsObt ↔ ψ.IsAcu

theorem EuclidGeom.AngValue.isRt_iff_isRt_of_add_eq_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : θ + ψ = ∠[Real.pi]) :

θ.IsRt ↔ ψ.IsRt

theorem EuclidGeom.AngValue.add_pi_div_two_isPos_iff_isAcu {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsPos ↔ θ.IsAcu

theorem EuclidGeom.AngValue.add_pi_div_two_isNeg_iff_isObt {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsNeg ↔ θ.IsObt

theorem EuclidGeom.AngValue.add_pi_div_two_not_isND_iff_isRt {θ : EuclidGeom.AngValue} :

¬(θ + ∠[Real.pi / 2]).IsND ↔ θ.IsRt

theorem EuclidGeom.AngValue.add_pi_div_two_isND_iff_not_isRt {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsND ↔ ¬θ.IsRt

theorem EuclidGeom.AngValue.add_pi_div_two_isAcu_iff_isNeg {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsAcu ↔ θ.IsNeg

theorem EuclidGeom.AngValue.add_pi_div_two_isObt_iff_isPos {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsObt ↔ θ.IsPos

theorem EuclidGeom.AngValue.add_pi_div_two_isRt_iff_not_isND {θ : EuclidGeom.AngValue} :

(θ + ∠[Real.pi / 2]).IsRt ↔ ¬θ.IsND

theorem EuclidGeom.AngValue.add_pi_div_two_not_isRt_iff_isND {θ : EuclidGeom.AngValue} :

¬(θ + ∠[Real.pi / 2]).IsRt ↔ θ.IsND

theorem EuclidGeom.AngValue.sub_pi_div_two_isPos_iff_isObt {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsPos ↔ θ.IsObt

theorem EuclidGeom.AngValue.sub_pi_div_two_isNeg_iff_isAcu {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsNeg ↔ θ.IsAcu

theorem EuclidGeom.AngValue.sub_pi_div_two_not_isND_iff_isRt {θ : EuclidGeom.AngValue} :

¬(θ - ∠[Real.pi / 2]).IsND ↔ θ.IsRt

theorem EuclidGeom.AngValue.sub_pi_div_two_isND_iff_not_isRt {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsND ↔ ¬θ.IsRt

theorem EuclidGeom.AngValue.sub_pi_div_two_isAcu_iff_isPos {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsAcu ↔ θ.IsPos

theorem EuclidGeom.AngValue.sub_pi_div_two_isObt_iff_isNeg {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsObt ↔ θ.IsNeg

theorem EuclidGeom.AngValue.sub_pi_div_two_isRt_iff_not_isND {θ : EuclidGeom.AngValue} :

(θ - ∠[Real.pi / 2]).IsRt ↔ ¬θ.IsND

theorem EuclidGeom.AngValue.sub_pi_div_two_not_isRt_iff_isND {θ : EuclidGeom.AngValue} :

¬(θ - ∠[Real.pi / 2]).IsRt ↔ θ.IsND

theorem EuclidGeom.AngValue.pi_div_two_sub_isPos_iff_isAcu {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsPos ↔ θ.IsAcu

theorem EuclidGeom.AngValue.pi_div_two_sub_isNeg_iff_isAcu {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsNeg ↔ θ.IsObt

theorem EuclidGeom.AngValue.pi_div_two_sub_not_isND_iff_isRt {θ : EuclidGeom.AngValue} :

¬(∠[Real.pi / 2] - θ).IsND ↔ θ.IsRt

theorem EuclidGeom.AngValue.pi_div_two_sub_isND_iff_not_isRt {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsND ↔ ¬θ.IsRt

theorem EuclidGeom.AngValue.pi_div_two_sub_isAcu_iff_isPos {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsAcu ↔ θ.IsPos

theorem EuclidGeom.AngValue.pi_div_two_sub_isObt_iff_isNeg {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsObt ↔ θ.IsNeg

theorem EuclidGeom.AngValue.pi_div_two_sub_isRt_iff_not_isND {θ : EuclidGeom.AngValue} :

(∠[Real.pi / 2] - θ).IsRt ↔ ¬θ.IsND

theorem EuclidGeom.AngValue.pi_div_two_sub_not_isRt_iff_isND {θ : EuclidGeom.AngValue} :

¬(∠[Real.pi / 2] - θ).IsRt ↔ θ.IsND

theorem EuclidGeom.AngValue.eq_pi_div_two_of_isRt_of_isPos {θ : EuclidGeom.AngValue} (hr : θ.IsRt) (h : ¬θ.IsNeg) :

θ = ∠[Real.pi / 2]

theorem EuclidGeom.AngValue.eq_neg_pi_div_two_of_isRt_of_isNeg {θ : EuclidGeom.AngValue} (hr : θ.IsRt) (h : ¬θ.IsPos) :

θ = ∠[-Real.pi / 2]

theorem EuclidGeom.AngValue.eq_zero_of_not_isND_of_isAcu {θ : EuclidGeom.AngValue} (hr : ¬θ.IsND) (h : θ.IsAcu) :

θ = 0

theorem EuclidGeom.AngValue.eq_pi_of_not_isND_of_isObt {θ : EuclidGeom.AngValue} (hr : ¬θ.IsND) (h : θ.IsObt) :

θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.cos_eq_iff_eq_of_isPos {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) :

EuclidGeom.AngValue.cos θ = EuclidGeom.AngValue.cos ψ ↔ θ = ψ

theorem EuclidGeom.AngValue.cos_eq_iff_eq_of_isNeg {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) :

EuclidGeom.AngValue.cos θ = EuclidGeom.AngValue.cos ψ ↔ θ = ψ

theorem EuclidGeom.AngValue.sin_eq_iff_eq_of_isAcu {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsAcu) :

EuclidGeom.AngValue.sin θ = EuclidGeom.AngValue.sin ψ ↔ θ = ψ

theorem EuclidGeom.AngValue.sin_eq_iff_eq_of_isObt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsObt) (hp : ψ.IsObt) :

EuclidGeom.AngValue.sin θ = EuclidGeom.AngValue.sin ψ ↔ θ = ψ

def EuclidGeom.AngDValue.Double :

EuclidGeom.AngDValue → EuclidGeom.AngValue

Equations

EuclidGeom.AngDValue.Double = (AddCircle.equivAddCircle Real.pi (2 * Real.pi) Real.pi_ne_zero EuclidGeom.AngDValue.Double.proof_2).toEquiv.toFun

Instances For

def EuclidGeom.AngDValue.DoubleHom :

EuclidGeom.AngDValue →+ EuclidGeom.AngValue

Equations

EuclidGeom.AngDValue.DoubleHom = AddEquiv.toAddMonoidHom (AddCircle.equivAddCircle Real.pi (2 * Real.pi) Real.pi_ne_zero EuclidGeom.AngDValue.DoubleHom.proof_4)

Instances For

@[simp]

theorem EuclidGeom.AngDValue.doubleHom_toFun_eq_double :

EuclidGeom.AngDValue.DoubleHom.toFun = EuclidGeom.AngDValue.Double

@[simp]

theorem EuclidGeom.AngDValue.zero_double :

EuclidGeom.AngDValue.Double 0 = 0

theorem EuclidGeom.AngDValue.double_coe_coe_eq_coe_mul_two (x : ℝ) :

EuclidGeom.AngDValue.Double ↑∠[x] = ∠[x * 2]

theorem EuclidGeom.AngDValue.real_div_two_double (x : ℝ) :

EuclidGeom.AngDValue.Double ↑∠[x / 2] = ∠[x]

theorem EuclidGeom.AngDValue.pi_div_two_double :

EuclidGeom.AngDValue.Double ↑∠[Real.pi / 2] = ∠[Real.pi]

theorem AngValue.double_coe_eq_two_nsmul {θ : EuclidGeom.AngValue} :

EuclidGeom.AngDValue.Double ↑θ = 2 • θ

theorem EuclidGeom.AngDValue.coe_double_eq_two_nsmul {θ : EuclidGeom.AngDValue} :

↑(EuclidGeom.AngDValue.Double θ) = 2 • θ

@[simp]

theorem EuclidGeom.AngDValue.double_add {x : EuclidGeom.AngDValue} {y : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double (x + y) = EuclidGeom.AngDValue.Double x + EuclidGeom.AngDValue.Double y

@[simp]

theorem EuclidGeom.AngDValue.double_neg {x : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double (-x) = -EuclidGeom.AngDValue.Double x

@[simp]

theorem EuclidGeom.AngDValue.double_sub {x : EuclidGeom.AngDValue} {y : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double (x - y) = EuclidGeom.AngDValue.Double x - EuclidGeom.AngDValue.Double y

@[simp]

theorem EuclidGeom.AngDValue.double_nsmul (n : ℕ) {x : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double (n • x) = n • EuclidGeom.AngDValue.Double x

@[simp]

theorem EuclidGeom.AngDValue.double_zsmul (n : ℤ) {x : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double (n • x) = n • EuclidGeom.AngDValue.Double x

@[simp]

theorem EuclidGeom.AngDValue.double_inj {x : EuclidGeom.AngDValue} {y : EuclidGeom.AngDValue} :

EuclidGeom.AngDValue.Double x = EuclidGeom.AngDValue.Double y ↔ x = y

def EuclidGeom.AngValue.abs (θ : EuclidGeom.AngValue) :

The absolute value of an angle $θ$ is the absolute value of $θ.toReal$.

Equations

EuclidGeom.AngValue.abs θ = |θ.toReal|

Instances For

theorem EuclidGeom.AngValue.abs_nonneg {θ : EuclidGeom.AngValue} :

0 ≤ EuclidGeom.AngValue.abs θ

theorem EuclidGeom.AngValue.abs_le_pi {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ ≤ Real.pi

theorem EuclidGeom.AngValue.neg_pi_lt_abs {θ : EuclidGeom.AngValue} :

-Real.pi < EuclidGeom.AngValue.abs θ

theorem EuclidGeom.AngValue.coe_abs_eq_abs {x : ℝ} (hn : -Real.pi < x) (h : x ≤ Real.pi) :

EuclidGeom.AngValue.abs ∠[x] = |x|

theorem EuclidGeom.AngValue.coe_abs_eq_abs_of_abs_le_pi {x : ℝ} (h : |x| ≤ Real.pi) :

EuclidGeom.AngValue.abs ∠[x] = |x|

theorem EuclidGeom.AngValue.coe_abs_le_abs (x : ℝ) :

EuclidGeom.AngValue.abs ∠[x] ≤ |x|

theorem EuclidGeom.AngValue.abs_min {θ : EuclidGeom.AngValue} {x : ℝ} (h : θ = ∠[x]) :

EuclidGeom.AngValue.abs θ ≤ |x|

theorem EuclidGeom.AngValue.eq_coe_or_neg_coe_of_abs_eq {θ : EuclidGeom.AngValue} {x : ℝ} (h : EuclidGeom.AngValue.abs θ = x) :

θ = ∠[x] ∨ θ = -∠[x]

theorem EuclidGeom.AngValue.abs_eq_toReal_or_neg_toeal {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ = θ.toReal ∨ EuclidGeom.AngValue.abs θ = -θ.toReal

theorem EuclidGeom.AngValue.coe_abs_eq_self_or_neg {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ] = θ ∨ ∠[EuclidGeom.AngValue.abs θ] = -θ

theorem EuclidGeom.AngValue.zero_abs :

EuclidGeom.AngValue.abs 0 = 0

theorem EuclidGeom.AngValue.abs_eq_zero_iff_eq_zero {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ = 0 ↔ θ = 0

theorem EuclidGeom.AngValue.abs_ne_zero_iff_ne_zero {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ ≠ 0 ↔ θ ≠ 0

theorem EuclidGeom.AngValue.abs_pos_iff_ne_zero {θ : EuclidGeom.AngValue} :

0 < EuclidGeom.AngValue.abs θ ↔ θ ≠ 0

theorem EuclidGeom.AngValue.pi_abs :

EuclidGeom.AngValue.abs ∠[Real.pi] = Real.pi

theorem EuclidGeom.AngValue.eq_pi_of_abs_eq_pi {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.abs θ = Real.pi) :

θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.abs_eq_pi_iff_eq_pi {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ = Real.pi ↔ θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.abs_ne_pi_iff_ne_pi {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ ≠ Real.pi ↔ θ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.abs_lt_pi_iff_ne_pi {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ < Real.pi ↔ θ ≠ ∠[Real.pi]

theorem EuclidGeom.AngValue.pi_div_two_abs :

EuclidGeom.AngValue.abs ∠[Real.pi / 2] = Real.pi / 2

theorem EuclidGeom.AngValue.abs_eq_pi_div_two_of_eq_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[Real.pi / 2]) :

EuclidGeom.AngValue.abs θ = Real.pi / 2

theorem EuclidGeom.AngValue.neg_pi_div_two_abs :

EuclidGeom.AngValue.abs ∠[-Real.pi / 2] = Real.pi / 2

theorem EuclidGeom.AngValue.abs_eq_pi_div_two_of_eq_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : θ = ∠[-Real.pi / 2]) :

EuclidGeom.AngValue.abs θ = Real.pi / 2

theorem EuclidGeom.AngValue.abs_eq_iff {α : EuclidGeom.AngValue} {β : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs α = EuclidGeom.AngValue.abs β ↔ α = β ∨ α = -β

theorem EuclidGeom.AngValue.abs_congr {α : EuclidGeom.AngValue} {β : EuclidGeom.AngValue} (h : α = β) :

EuclidGeom.AngValue.abs α = EuclidGeom.AngValue.abs β

theorem EuclidGeom.AngValue.abs_pos_lt_pi_iff_isND {θ : EuclidGeom.AngValue} :

0 < EuclidGeom.AngValue.abs θ ∧ EuclidGeom.AngValue.abs θ < Real.pi ↔ θ.IsND

theorem EuclidGeom.AngValue.coe_abs_not_isNeg {θ : EuclidGeom.AngValue} :

¬∠[EuclidGeom.AngValue.abs θ].IsNeg

theorem EuclidGeom.AngValue.coe_abs_isPos_iff_isND {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ].IsPos ↔ θ.IsND

theorem EuclidGeom.AngValue.coe_abs_isPos_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

∠[EuclidGeom.AngValue.abs θ].IsPos

theorem EuclidGeom.AngValue.abs_eq_toReal_of_not_isNeg {θ : EuclidGeom.AngValue} (h : ¬θ.IsNeg) :

EuclidGeom.AngValue.abs θ = θ.toReal

theorem EuclidGeom.AngValue.coe_abs_eq_self_of_not_isNeg {θ : EuclidGeom.AngValue} (h : ¬θ.IsNeg) :

∠[EuclidGeom.AngValue.abs θ] = θ

theorem EuclidGeom.AngValue.abs_eq_toReal_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

EuclidGeom.AngValue.abs θ = θ.toReal

theorem EuclidGeom.AngValue.coe_abs_eq_self_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

∠[EuclidGeom.AngValue.abs θ] = θ

theorem EuclidGeom.AngValue.abs_eq_toReal_of_isND {θ : EuclidGeom.AngValue} (h : ¬θ.IsND) :

EuclidGeom.AngValue.abs θ = θ.toReal

theorem EuclidGeom.AngValue.coe_abs_eq_self_of_isND {θ : EuclidGeom.AngValue} (h : ¬θ.IsND) :

∠[EuclidGeom.AngValue.abs θ] = θ

theorem EuclidGeom.AngValue.abs_eq_neg_toReal_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

EuclidGeom.AngValue.abs θ = -θ.toReal

theorem EuclidGeom.AngValue.coe_abs_eq_neg_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

∠[EuclidGeom.AngValue.abs θ] = -θ

theorem EuclidGeom.AngValue.not_isNeg_of_abs_eq_toReal {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.abs θ = θ.toReal) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.not_isNeg_of_coe_abs_eq_self {θ : EuclidGeom.AngValue} (h : ∠[EuclidGeom.AngValue.abs θ] = θ) :

¬θ.IsNeg

theorem EuclidGeom.AngValue.abs_eq_toReal_iff {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ = θ.toReal ↔ ¬θ.IsNeg

theorem EuclidGeom.AngValue.abs_ne_toReal_iff {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ ≠ θ.toReal ↔ θ.IsNeg

theorem EuclidGeom.AngValue.coe_abs_eq_neg_iff_isNeg {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ] = θ ↔ ¬θ.IsNeg

theorem EuclidGeom.AngValue.coe_abs_ne_neg_iff_not_isNeg {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ] ≠ θ ↔ θ.IsNeg

theorem EuclidGeom.AngValue.eq_of_isPos_of_abs_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsPos) (hp : ψ.IsPos) (h : EuclidGeom.AngValue.abs θ = EuclidGeom.AngValue.abs ψ) :

θ = ψ

theorem EuclidGeom.AngValue.eq_of_isNeg_of_abs_eq {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsNeg) (hp : ψ.IsNeg) (h : EuclidGeom.AngValue.abs θ = EuclidGeom.AngValue.abs ψ) :

θ = ψ

theorem EuclidGeom.AngValue.coe_abs_isAcu_iff_isAcu {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ].IsAcu ↔ θ.IsAcu

theorem EuclidGeom.AngValue.coe_abs_isObt_iff_isObt {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ].IsObt ↔ θ.IsObt

theorem EuclidGeom.AngValue.coe_abs_isRt_iff_isRt {θ : EuclidGeom.AngValue} :

∠[EuclidGeom.AngValue.abs θ].IsRt ↔ θ.IsRt

theorem EuclidGeom.AngValue.isRt_iff_abs_eq_pi_div_two {θ : EuclidGeom.AngValue} :

θ.IsRt ↔ EuclidGeom.AngValue.abs θ = Real.pi / 2

theorem EuclidGeom.AngValue.isAcu_iff_abs_lt_pi_div_two {θ : EuclidGeom.AngValue} :

θ.IsAcu ↔ EuclidGeom.AngValue.abs θ < Real.pi / 2

theorem EuclidGeom.AngValue.not_isAcu_iff_pi_div_two_le_abs {θ : EuclidGeom.AngValue} :

¬θ.IsAcu ↔ Real.pi / 2 ≤ EuclidGeom.AngValue.abs θ

theorem EuclidGeom.AngValue.isObt_iff_pi_div_two_lt_abs {θ : EuclidGeom.AngValue} :

θ.IsObt ↔ Real.pi / 2 < EuclidGeom.AngValue.abs θ

theorem EuclidGeom.AngValue.not_isObt_iff_abs_le_pi_div_two {θ : EuclidGeom.AngValue} :

¬θ.IsObt ↔ EuclidGeom.AngValue.abs θ ≤ Real.pi / 2

theorem EuclidGeom.AngValue.abs_lt_of_isAcu_of_isObt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsAcu) (hp : ψ.IsObt) :

EuclidGeom.AngValue.abs θ < EuclidGeom.AngValue.abs ψ

theorem EuclidGeom.AngValue.abs_le_of_not_isObt_of_not_isAcu {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : ¬θ.IsObt) (hp : ¬ψ.IsAcu) :

EuclidGeom.AngValue.abs θ ≤ EuclidGeom.AngValue.abs ψ

theorem EuclidGeom.AngValue.abs_eq_of_isRt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsRt) (hp : ψ.IsRt) :

EuclidGeom.AngValue.abs θ = EuclidGeom.AngValue.abs ψ

theorem EuclidGeom.AngValue.eq_or_eq_neg_of_isRt {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (hs : θ.IsRt) (hp : ψ.IsRt) :

θ = ψ ∨ θ = -ψ

theorem EuclidGeom.AngValue.abs_eq_norm {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs θ = ‖θ‖

The absolute value of an angle is equal to its norm.

@[simp]

theorem EuclidGeom.AngValue.abs_neg {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs (-θ) = EuclidGeom.AngValue.abs θ

theorem EuclidGeom.AngValue.abs_add_le {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs (θ + ψ) ≤ EuclidGeom.AngValue.abs θ + EuclidGeom.AngValue.abs ψ

def EuclidGeom.AngValue.half (θ : EuclidGeom.AngValue) :

EuclidGeom.AngValue

Half of an angle. Note that there are two possible values when dividing by two in AngValue (their difference is π). We choose the acute angle as the canonical value for half of an angle for angles not equal to π, and the half of π is defined as π / 2.

Equations

EuclidGeom.AngValue.half θ = ∠[θ.toReal / 2]

Instances For

theorem EuclidGeom.AngValue.coe_half {x : ℝ} (hn : -Real.pi < x) (h : x ≤ Real.pi) :

EuclidGeom.AngValue.half ∠[x] = ∠[x / 2]

@[simp]

theorem EuclidGeom.AngValue.two_nsmul_half {θ : EuclidGeom.AngValue} :

2 • EuclidGeom.AngValue.half θ = θ

theorem EuclidGeom.AngValue.two_nsmul_eq_iff_eq_half_or_eq_half_add_pi {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} :

2 • ψ = θ ↔ ψ = EuclidGeom.AngValue.half θ ∨ ψ = EuclidGeom.AngValue.half θ + ∠[Real.pi]

theorem EuclidGeom.AngValue.two_nsmul_half_add_pi {θ : EuclidGeom.AngValue} :

2 • (EuclidGeom.AngValue.half θ + ∠[Real.pi]) = θ

theorem EuclidGeom.AngValue.sub_half_eq_half {θ : EuclidGeom.AngValue} :

θ - EuclidGeom.AngValue.half θ = EuclidGeom.AngValue.half θ

@[simp]

theorem EuclidGeom.AngValue.half_toReal {θ : EuclidGeom.AngValue} :

(EuclidGeom.AngValue.half θ).toReal = θ.toReal / 2

theorem EuclidGeom.AngValue.half_toReal_le_two_inv_mul_pi {θ : EuclidGeom.AngValue} :

(EuclidGeom.AngValue.half θ).toReal ≤ Real.pi / 2

theorem EuclidGeom.AngValue.half_toReal_lt_two_inv_mul_pi_of_ne_pi {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

(EuclidGeom.AngValue.half θ).toReal < Real.pi / 2

theorem EuclidGeom.AngValue.neg_two_inv_mul_pi_lt_half_toReal {θ : EuclidGeom.AngValue} :

-Real.pi / 2 < (EuclidGeom.AngValue.half θ).toReal

theorem EuclidGeom.AngValue.half_toReal_lt_pi {θ : EuclidGeom.AngValue} :

(EuclidGeom.AngValue.half θ).toReal < Real.pi

theorem EuclidGeom.AngValue.eq_two_mul_coe_of_half_toReal_eq {θ : EuclidGeom.AngValue} {x : ℝ} (h : (EuclidGeom.AngValue.half θ).toReal = x) :

θ = ∠[2 * x]

theorem EuclidGeom.AngValue.half_inj {α : EuclidGeom.AngValue} {β : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.half α = EuclidGeom.AngValue.half β) :

α = β

@[simp]

theorem EuclidGeom.AngValue.half_congr {α : EuclidGeom.AngValue} {β : EuclidGeom.AngValue} :

EuclidGeom.AngValue.half α = EuclidGeom.AngValue.half β ↔ α = β

theorem EuclidGeom.AngValue.half_neg {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

EuclidGeom.AngValue.half (-θ) = -EuclidGeom.AngValue.half θ

theorem EuclidGeom.AngValue.half_neg_of_isND {θ : EuclidGeom.AngValue} (h : θ.IsND) :

EuclidGeom.AngValue.half (-θ) = -EuclidGeom.AngValue.half θ

@[simp]

theorem EuclidGeom.AngValue.zero_half :

EuclidGeom.AngValue.half 0 = 0

theorem EuclidGeom.AngValue.eq_zero_of_half_eq_zero {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.half θ = 0) :

θ = 0

@[simp]

theorem EuclidGeom.AngValue.half_eq_zero_iff_eq_zero {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.half θ = 0 ↔ θ = 0

@[simp]

theorem EuclidGeom.AngValue.pi_half :

EuclidGeom.AngValue.half ∠[Real.pi] = ∠[Real.pi / 2]

theorem EuclidGeom.AngValue.eq_pi_of_half_eq_pi {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.half θ = ∠[Real.pi / 2]) :

θ = ∠[Real.pi]

@[simp]

theorem EuclidGeom.AngValue.half_eq_pi_iff_eq_pi {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.half θ = ∠[Real.pi / 2] ↔ θ = ∠[Real.pi]

theorem EuclidGeom.AngValue.half_pi_div_nat (n : ℕ) :

EuclidGeom.AngValue.half ∠[Real.pi / ↑n] = ∠[Real.pi / (↑n * 2)]

theorem EuclidGeom.AngValue.pi_div_two_half :

EuclidGeom.AngValue.half ∠[Real.pi / 2] = ∠[Real.pi / 4]

theorem EuclidGeom.AngValue.pi_div_three_half :

EuclidGeom.AngValue.half ∠[Real.pi / 3] = ∠[Real.pi / 6]

theorem EuclidGeom.AngValue.half_neg_pi_div_nat {n : ℕ} (h : 2 ≤ n) :

EuclidGeom.AngValue.half ∠[-Real.pi / ↑n] = ∠[-Real.pi / (↑n * 2)]

theorem EuclidGeom.AngValue.neg_pi_div_two_half :

EuclidGeom.AngValue.half ∠[-Real.pi / 2] = ∠[-Real.pi / 4]

theorem EuclidGeom.AngValue.neg_pi_div_three_half :

EuclidGeom.AngValue.half ∠[-Real.pi / 3] = ∠[-Real.pi / 6]

theorem EuclidGeom.AngValue.half_isPos_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

(EuclidGeom.AngValue.half θ).IsPos

theorem EuclidGeom.AngValue.half_isNeg_iff_isNeg {θ : EuclidGeom.AngValue} :

(EuclidGeom.AngValue.half θ).IsNeg ↔ θ.IsNeg

theorem EuclidGeom.AngValue.half_not_isObt {θ : EuclidGeom.AngValue} :

¬(EuclidGeom.AngValue.half θ).IsObt

theorem EuclidGeom.AngValue.half_isAcu_of_ne_pi {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

(EuclidGeom.AngValue.half θ).IsAcu

theorem EuclidGeom.AngValue.half_add_pi_not_isAcu {θ : EuclidGeom.AngValue} :

¬(EuclidGeom.AngValue.half θ + ∠[Real.pi]).IsAcu

theorem EuclidGeom.AngValue.half_add_pi_isObt_of_ne_pi {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

(EuclidGeom.AngValue.half θ + ∠[Real.pi]).IsObt

theorem EuclidGeom.AngValue.abs_sin_half {θ : EuclidGeom.AngValue} :

|EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ)| = Real.sqrt ((1 - EuclidGeom.AngValue.cos θ) / 2)

theorem EuclidGeom.AngValue.sin_half_of_not_isNeg {θ : EuclidGeom.AngValue} (h : ¬θ.IsNeg) :

EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ) = Real.sqrt ((1 - EuclidGeom.AngValue.cos θ) / 2)

theorem EuclidGeom.AngValue.sin_half_of_isPos {θ : EuclidGeom.AngValue} (h : θ.IsPos) :

EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ) = Real.sqrt ((1 - EuclidGeom.AngValue.cos θ) / 2)

theorem EuclidGeom.AngValue.sin_half_of_isNeg {θ : EuclidGeom.AngValue} (h : θ.IsNeg) :

EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ) = -Real.sqrt ((1 - EuclidGeom.AngValue.cos θ) / 2)

theorem EuclidGeom.AngValue.cos_half {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ) = Real.sqrt ((1 + EuclidGeom.AngValue.cos θ) / 2)

theorem EuclidGeom.AngValue.sin_sub_sin {θ : EuclidGeom.AngValue} (ψ : EuclidGeom.AngValue) :

EuclidGeom.AngValue.sin θ - EuclidGeom.AngValue.sin ψ = 2 * (EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ - EuclidGeom.AngValue.half ψ) * EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ + EuclidGeom.AngValue.half ψ))

theorem EuclidGeom.AngValue.cos_half_mul_sin_half {θ : EuclidGeom.AngValue} :

2 * (EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ) * EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ)) = EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.sin_half_mul_cos_half {θ : EuclidGeom.AngValue} :

2 * (EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ) * EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ)) = EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.sin_add_sin {θ : EuclidGeom.AngValue} (ψ : EuclidGeom.AngValue) :

EuclidGeom.AngValue.sin θ + EuclidGeom.AngValue.sin ψ = 2 * (EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ + EuclidGeom.AngValue.half ψ) * EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ - EuclidGeom.AngValue.half ψ))

theorem EuclidGeom.AngValue.cos_sub_cos {θ : EuclidGeom.AngValue} (ψ : EuclidGeom.AngValue) :

EuclidGeom.AngValue.cos θ - EuclidGeom.AngValue.cos ψ = -2 * (EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ + EuclidGeom.AngValue.half ψ) * EuclidGeom.AngValue.sin (EuclidGeom.AngValue.half θ - EuclidGeom.AngValue.half ψ))

theorem EuclidGeom.AngValue.cos_add_cos {θ : EuclidGeom.AngValue} (ψ : EuclidGeom.AngValue) :

EuclidGeom.AngValue.cos θ + EuclidGeom.AngValue.cos ψ = 2 * (EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ + EuclidGeom.AngValue.half ψ) * EuclidGeom.AngValue.cos (EuclidGeom.AngValue.half θ - EuclidGeom.AngValue.half ψ))

theorem EuclidGeom.AngValue.half_abs {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ) = EuclidGeom.AngValue.abs θ / 2

theorem EuclidGeom.AngValue.half_abs_le_pi_div_two {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ) ≤ Real.pi / 2

theorem EuclidGeom.AngValue.half_abs_lt_pi_div_two_of_ne_pi {θ : EuclidGeom.AngValue} (h : θ ≠ ∠[Real.pi]) :

EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ) < Real.pi / 2

theorem EuclidGeom.AngValue.half_abs_le_half_add_pi_abs {θ : EuclidGeom.AngValue} :

EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ) ≤ EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ + ∠[Real.pi])

theorem EuclidGeom.AngValue.half_abs_min {θ : EuclidGeom.AngValue} {ψ : EuclidGeom.AngValue} (h : 2 • ψ = θ) :

EuclidGeom.AngValue.abs (EuclidGeom.AngValue.half θ) ≤ EuclidGeom.AngValue.abs ψ