Angles between points #

This file defines unoriented angles in Euclidean affine spaces.

Main definitions #

EuclideanGeometry.angle, with notation ∠, is the undirected angle determined by three points.

TODO #

Prove the triangle inequality for the angle.

def EuclideanGeometry.angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) (p3 : P) :

ℝ

The undirected angle at p2 between the line segments to p1 and p3. If either of those points equals p2, this is π/2. Use open scoped EuclideanGeometry to access the ∠ p1 p2 p3 notation.

Equations

EuclideanGeometry.angle p1 p2 p3 = InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2)

Instances For

source

def EuclideanGeometry.«term∠» :

Lean.ParserDescr

Equations

EuclideanGeometry.«term∠» = Lean.ParserDescr.node `EuclideanGeometry.term∠ 1024 (Lean.ParserDescr.symbol "∠")

Instances For

source

theorem EuclideanGeometry.continuousAt_angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) :

ContinuousAt (fun (y : P × P × P) => EuclideanGeometry.angle y.1 y.2.1 y.2.2) x

source

@[simp]

theorem AffineIsometry.angle_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ ] P₂) (p₁ : P) (p₂ : P) (p₃ : P) :

EuclideanGeometry.angle (f p₁) (f p₂) (f p₃) = EuclideanGeometry.angle p₁ p₂ p₃

source

@[simp]

theorem AffineSubspace.angle_coe {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (p₁ : ↥s) (p₂ : ↥s) (p₃ : ↥s) :

EuclideanGeometry.angle ↑p₁ ↑p₂ ↑p₃ = EuclideanGeometry.angle p₁ p₂ p₃

source

@[simp]

theorem EuclideanGeometry.angle_const_vadd {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p₁ : P) (p₂ : P) (p₃ : P) :

EuclideanGeometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃

Angles are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_vadd_const {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v₁ : V) (v₂ : V) (v₃ : V) (p : P) :

EuclideanGeometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = EuclideanGeometry.angle v₁ v₂ v₃

Angles are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_const_vsub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p : P) (p₁ : P) (p₂ : P) (p₃ : P) :

EuclideanGeometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃

Angles are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_vsub_const {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) (p : P) :

EuclideanGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = EuclideanGeometry.angle p₁ p₂ p₃

Angles are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_add_const {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ : V) (v₂ : V) (v₃ : V) (v : V) :

EuclideanGeometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = EuclideanGeometry.angle v₁ v₂ v₃

Angles in a vector space are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_const_add {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v : V) (v₁ : V) (v₂ : V) (v₃ : V) :

EuclideanGeometry.angle (v + v₁) (v + v₂) (v + v₃) = EuclideanGeometry.angle v₁ v₂ v₃

Angles in a vector space are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_sub_const {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ : V) (v₂ : V) (v₃ : V) (v : V) :

EuclideanGeometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = EuclideanGeometry.angle v₁ v₂ v₃

Angles in a vector space are translation invariant

source

@[simp]

theorem EuclideanGeometry.angle_const_sub {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v : V) (v₁ : V) (v₂ : V) (v₃ : V) :

EuclideanGeometry.angle (v - v₁) (v - v₂) (v - v₃) = EuclideanGeometry.angle v₁ v₂ v₃

Angles in a vector space are invariant to inversion

source

@[simp]

theorem EuclideanGeometry.angle_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ : V) (v₂ : V) (v₃ : V) :

EuclideanGeometry.angle (-v₁) (-v₂) (-v₃) = EuclideanGeometry.angle v₁ v₂ v₃

Angles in a vector space are invariant to inversion

source

theorem EuclideanGeometry.angle_comm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) (p3 : P) :

EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p3 p2 p1

The angle at a point does not depend on the order of the other two points.

source

theorem EuclideanGeometry.angle_nonneg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) (p3 : P) :

0 ≤ EuclideanGeometry.angle p1 p2 p3

The angle at a point is nonnegative.

source

theorem EuclideanGeometry.angle_le_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) (p3 : P) :

EuclideanGeometry.angle p1 p2 p3 ≤ Real.pi

The angle at a point is at most π.

source

@[simp]

theorem EuclideanGeometry.angle_self_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ : P) (p : P) :

EuclideanGeometry.angle p₀ p₀ p = Real.pi / 2

The angle ∠AAB at a point is always π / 2.

source

@[simp]

theorem EuclideanGeometry.angle_self_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ : P) (p : P) :

EuclideanGeometry.angle p p₀ p₀ = Real.pi / 2

The angle ∠ABB at a point is always π / 2.

source

theorem EuclideanGeometry.angle_self_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p : P} {p₀ : P} (h : p ≠ p₀) :

EuclideanGeometry.angle p p₀ p = 0

The angle ∠ABA at a point is 0, unless A = B.

source

@[deprecated EuclideanGeometry.angle_self_left]

theorem EuclideanGeometry.angle_eq_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ : P) (p : P) :

EuclideanGeometry.angle p₀ p₀ p = Real.pi / 2

Alias of EuclideanGeometry.angle_self_left.

The angle ∠AAB at a point is always π / 2.

source

@[deprecated EuclideanGeometry.angle_self_right]

theorem EuclideanGeometry.angle_eq_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ : P) (p : P) :

EuclideanGeometry.angle p p₀ p₀ = Real.pi / 2

Alias of EuclideanGeometry.angle_self_right.

The angle ∠ABB at a point is always π / 2.

source

@[deprecated EuclideanGeometry.angle_self_of_ne]

theorem EuclideanGeometry.angle_eq_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p : P} {p₀ : P} (h : p ≠ p₀) :

EuclideanGeometry.angle p p₀ p = 0

Alias of EuclideanGeometry.angle_self_of_ne.

The angle ∠ABA at a point is 0, unless A = B.

source

theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = Real.pi) :

EuclideanGeometry.angle p2 p1 p3 = 0

If the angle ∠ABC at a point is π, the angle ∠BAC is 0.

source

theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = Real.pi) :

EuclideanGeometry.angle p2 p3 p1 = 0

If the angle ∠ABC at a point is π, the angle ∠BCA is 0.

source

theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) {p2 : P} {p3 : P} {p4 : P} (h : EuclideanGeometry.angle p2 p3 p4 = Real.pi) :

EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p2 p4

If ∠BCD = π, then ∠ABC = ∠ABD.

source

theorem EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) {p2 : P} {p3 : P} {p4 : P} (h : EuclideanGeometry.angle p2 p3 p4 = Real.pi) :

EuclideanGeometry.angle p1 p3 p2 + EuclideanGeometry.angle p1 p3 p4 = Real.pi

If ∠BCD = π, then ∠ACB + ∠ACD = π.

source

theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} {p4 : P} {p5 : P} (hapc : EuclideanGeometry.angle p1 p5 p3 = Real.pi) (hbpd : EuclideanGeometry.angle p2 p5 p4 = Real.pi) :

EuclideanGeometry.angle p1 p5 p2 = EuclideanGeometry.angle p3 p5 p4

Vertical Angles Theorem: angles opposite each other, formed by two intersecting straight lines, are equal.

source

theorem EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = Real.pi) :

dist p1 p2 ≠ 0

If ∠ABC = π then dist A B ≠ 0.

source

theorem EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = Real.pi) :

dist p3 p2 ≠ 0

If ∠ABC = π then dist C B ≠ 0.

source

theorem EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = Real.pi) :

dist p1 p3 = dist p1 p2 + dist p3 p2

If ∠ABC = π, then (dist A C) = (dist A B) + (dist B C).

source

theorem EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :

dist p1 p3 = dist p1 p2 + dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi

If A ≠ B and C ≠ B then ∠ABC = π if and only if (dist A C) = (dist A B) + (dist B C).

source

theorem EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : EuclideanGeometry.angle p1 p2 p3 = 0) :

dist p1 p3 = |dist p1 p2 - dist p3 p2|

If ∠ABC = 0, then (dist A C) = abs ((dist A B) - (dist B C)).

source

theorem EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :

dist p1 p3 = |dist p1 p2 - dist p3 p2| ↔ EuclideanGeometry.angle p1 p2 p3 = 0

If A ≠ B and C ≠ B then ∠ABC = 0 if and only if (dist A C) = abs ((dist A B) - (dist B C)).

source

theorem EuclideanGeometry.angle_midpoint_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p1 : P) (p2 : P) (hp1p2 : p1 ≠ p2) :

EuclideanGeometry.angle p1 (midpoint ℝ p1 p2) p2 = Real.pi

If M is the midpoint of the segment AB, then ∠AMB = π.

source

theorem EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : dist p3 p1 = dist p3 p2) :

EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p1 = Real.pi / 2

If M is the midpoint of the segment AB and C is the same distance from A as it is from B then ∠CMA = π / 2.

source

theorem EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h : dist p3 p1 = dist p3 p2) :

EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p2 = Real.pi / 2

If M is the midpoint of the segment AB and C is the same distance from A as it is from B then ∠CMB = π / 2.

source

theorem Sbtw.angle₁₂₃_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi

If the second of three points is strictly between the other two, the angle at that point is π.

source

theorem Sbtw.angle₃₂₁_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi

If the second of three points is strictly between the other two, the angle at that point (reversed) is π.

source

theorem EuclideanGeometry.angle_eq_pi_iff_sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi ↔ Sbtw ℝ p₁ p₂ p₃

The angle between three points is π if and only if the second point is strictly between the other two.

source

theorem Wbtw.angle₂₁₃_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) :

EuclideanGeometry.angle p₂ p₁ p₃ = 0

If the second of three points is weakly between the other two, and not equal to the first, the angle at the first point is zero.

source

theorem Sbtw.angle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₂ p₁ p₃ = 0

If the second of three points is strictly between the other two, the angle at the first point is zero.

source

theorem Wbtw.angle₃₁₂_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) :

EuclideanGeometry.angle p₃ p₁ p₂ = 0

If the second of three points is weakly between the other two, and not equal to the first, the angle at the first point (reversed) is zero.

source

theorem Sbtw.angle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₃ p₁ p₂ = 0

If the second of three points is strictly between the other two, the angle at the first point (reversed) is zero.

source

theorem Wbtw.angle₂₃₁_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₃ : p₂ ≠ p₃) :

EuclideanGeometry.angle p₂ p₃ p₁ = 0

If the second of three points is weakly between the other two, and not equal to the third, the angle at the third point is zero.

source

theorem Sbtw.angle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₂ p₃ p₁ = 0

If the second of three points is strictly between the other two, the angle at the third point is zero.

source

theorem Wbtw.angle₁₃₂_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₃ : p₂ ≠ p₃) :

EuclideanGeometry.angle p₁ p₃ p₂ = 0

If the second of three points is weakly between the other two, and not equal to the third, the angle at the third point (reversed) is zero.

source

theorem Sbtw.angle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :

EuclideanGeometry.angle p₁ p₃ p₂ = 0

If the second of three points is strictly between the other two, the angle at the third point (reversed) is zero.

source

theorem EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

The angle between three points is zero if and only if one of the first and third points is weakly between the other two, and not equal to the second.

source

theorem EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

The angle between three points is zero if and only if one of the first and third points is strictly between the other two, or those two points are equal but not equal to the second.

source

theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi

Three points are collinear if and only if the first or third point equals the second or the angle between them is 0 or π.

source

theorem EuclideanGeometry.collinear_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = 0) :

Collinear ℝ {p₁, p₂, p₃}

If the angle between three points is 0, they are collinear.

source

theorem EuclideanGeometry.collinear_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) :

Collinear ℝ {p₁, p₂, p₃}

If the angle between three points is π, they are collinear.

source

theorem EuclideanGeometry.angle_ne_zero_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

EuclideanGeometry.angle p₁ p₂ p₃ ≠ 0

If three points are not collinear, the angle between them is nonzero.

source

theorem EuclideanGeometry.angle_ne_pi_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

EuclideanGeometry.angle p₁ p₂ p₃ ≠ Real.pi

If three points are not collinear, the angle between them is not π.

source

theorem EuclideanGeometry.angle_pos_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

0 < EuclideanGeometry.angle p₁ p₂ p₃

If three points are not collinear, the angle between them is positive.

source

theorem EuclideanGeometry.angle_lt_pi_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi

If three points are not collinear, the angle between them is less than π.

source

theorem EuclideanGeometry.cos_eq_one_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0

The cosine of the angle between three points is 1 if and only if the angle is 0.

source

theorem EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2

The cosine of the angle between three points is 0 if and only if the angle is π / 2.

source

theorem EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = -1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi

The cosine of the angle between three points is -1 if and only if the angle is π.

source

theorem EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi

The sine of the angle between three points is 0 if and only if the angle is 0 or π.

source

theorem EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2

The sine of the angle between three points is 1 if and only if the angle is π / 2.

source

theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} :

Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0

Three points are collinear if and only if the first or third point equals the second or the sine of the angle between three points is zero.

source

theorem EuclideanGeometry.sin_pos_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

0 < Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)

If three points are not collinear, the sine of the angle between them is positive.

source

theorem EuclideanGeometry.sin_ne_zero_of_not_collinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) :

Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) ≠ 0

If three points are not collinear, the sine of the angle between them is nonzero.

source

theorem EuclideanGeometry.collinear_of_sin_eq_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0) :

Collinear ℝ {p₁, p₂, p₃}

If the sine of the angle between three points is 0, they are collinear.

Documentation

Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Angles between points #

Main definitions #

TODO #