mathlib3documentation

geometry.euclidean.angle.unoriented.affine

Angles between points #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines unoriented angles in Euclidean affine spaces.

Main definitions #

• euclidean_geometry.angle, with notation ∠, is the undirected angle determined by three points.
noncomputable def euclidean_geometry.angle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 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_locale euclidean_geometry to access the ∠ p1 p2 p3 notation.

Equations
theorem euclidean_geometry.continuous_at_angle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {x : P × P × P} (hx12 : x.fst x.snd.fst) (hx32 : x.snd.snd x.snd.fst) :
continuous_at (λ (y : P × P × P), y.snd.snd) x
@[simp]
theorem affine_isometry.angle_map {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {V₂ : Type u_3} {P₂ : Type u_4} [ V₂] [metric_space P₂] [ P₂] (f : P →ᵃⁱ[] P₂) (p₁ p₂ p₃ : P) :
(f p₂) (f p₃) = p₃
@[simp, norm_cast]
theorem affine_subspace.angle_coe {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {s : P} (p₁ p₂ p₃ : s) :
p₃ = p₃
@[simp]
theorem euclidean_geometry.angle_const_vadd {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (v : V) (p₁ p₂ p₃ : P) :
euclidean_geometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = p₃

Angles are translation invariant

@[simp]
theorem euclidean_geometry.angle_vadd_const {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (v₁ v₂ v₃ : V) (p : P) :
euclidean_geometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = v₃

Angles are translation invariant

@[simp]
theorem euclidean_geometry.angle_const_vsub {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p p₁ p₂ p₃ : P) :
euclidean_geometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = p₃

Angles are translation invariant

@[simp]
theorem euclidean_geometry.angle_vsub_const {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p₁ p₂ p₃ p : P) :
euclidean_geometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = p₃

Angles are translation invariant

@[simp]
theorem euclidean_geometry.angle_add_const {V : Type u_1} (v₁ v₂ v₃ v : V) :
euclidean_geometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = v₃

Angles in a vector space are translation invariant

@[simp]
theorem euclidean_geometry.angle_const_add {V : Type u_1} (v v₁ v₂ v₃ : V) :
euclidean_geometry.angle (v + v₁) (v + v₂) (v + v₃) = v₃

Angles in a vector space are translation invariant

@[simp]
theorem euclidean_geometry.angle_sub_const {V : Type u_1} (v₁ v₂ v₃ v : V) :
euclidean_geometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = v₃

Angles in a vector space are translation invariant

@[simp]
theorem euclidean_geometry.angle_const_sub {V : Type u_1} (v v₁ v₂ v₃ : V) :
euclidean_geometry.angle (v - v₁) (v - v₂) (v - v₃) = v₃

Angles in a vector space are invariant to inversion

@[simp]
theorem euclidean_geometry.angle_neg {V : Type u_1} (v₁ v₂ v₃ : V) :
(-v₂) (-v₃) = v₃

Angles in a vector space are invariant to inversion

theorem euclidean_geometry.angle_comm {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 p3 : P) :
p3 = p1

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

theorem euclidean_geometry.angle_nonneg {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 p3 : P) :
0 p3

The angle at a point is nonnegative.

theorem euclidean_geometry.angle_le_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 p3 : P) :

The angle at a point is at most π.

theorem euclidean_geometry.angle_eq_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 : P) :
p2 =

The angle ∠AAB at a point.

theorem euclidean_geometry.angle_eq_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 : P) :
p2 =

The angle ∠ABB at a point.

theorem euclidean_geometry.angle_eq_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 : P} (h : p1 p2) :
p1 = 0

The angle ∠ABA at a point.

theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_left {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = real.pi) :
p3 = 0

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

theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_right {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = real.pi) :
p1 = 0

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

theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 : P) {p2 p3 p4 : P} (h : p4 = real.pi) :
p3 = p4

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

theorem euclidean_geometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 : P) {p2 p3 p4 : P} (h : p4 = real.pi) :
p2 + p4 = real.pi

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

theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 p4 p5 : P} (hapc : p3 = real.pi) (hbpd : p4 = real.pi) :
p2 = p4

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

theorem euclidean_geometry.left_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = real.pi) :
p2 0

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

theorem euclidean_geometry.right_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = real.pi) :
p2 0

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

theorem euclidean_geometry.dist_eq_add_dist_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = real.pi) :
p3 = p2 + p2

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

theorem euclidean_geometry.dist_eq_add_dist_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (hp1p2 : p1 p2) (hp3p2 : p3 p2) :
p3 = p2 + 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).

theorem euclidean_geometry.dist_eq_abs_sub_dist_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p3 = 0) :
p3 = | p2 - p2|

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

theorem euclidean_geometry.dist_eq_abs_sub_dist_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (hp1p2 : p1 p2) (hp3p2 : p3 p2) :
p3 = | p2 - 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)).

theorem euclidean_geometry.angle_midpoint_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 : P) (hp1p2 : p1 p2) :
p1 p2) p2 = real.pi

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

theorem euclidean_geometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p1 = p2) :
p1 p2) p1 =

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.

theorem euclidean_geometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p1 = p2) :
p1 p2) p2 =

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.

theorem sbtw.angle₁₂₃_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₃ = real.pi

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

theorem sbtw.angle₃₂₁_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₁ = real.pi

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

theorem euclidean_geometry.angle_eq_pi_iff_sbtw {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
p₃ = real.pi p₁ p₂ p₃

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

theorem wbtw.angle₂₁₃_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) (hp₂p₁ : 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.

theorem sbtw.angle₂₁₃_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₃ = 0

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

theorem wbtw.angle₃₁₂_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) (hp₂p₁ : 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.

theorem sbtw.angle₃₁₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ 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.

theorem wbtw.angle₂₃₁_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) (hp₂p₃ : 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.

theorem sbtw.angle₂₃₁_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) :
p₁ = 0

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

theorem wbtw.angle₁₃₂_eq_zero_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ p₂ p₃) (hp₂p₃ : 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.

theorem sbtw.angle₁₃₂_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₁ 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.

theorem euclidean_geometry.angle_eq_zero_iff_ne_and_wbtw {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
p₃ = 0 p₁ p₂ p₂ p₁ p₃ p₃ p₂ 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.

theorem euclidean_geometry.angle_eq_zero_iff_eq_and_ne_or_sbtw {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
p₃ = 0 p₁ = p₃ p₁ p₂ p₂ p₁ p₃ 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.

theorem euclidean_geometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
{p₁, p₂, p₃} p₁ = p₂ p₃ = p₂ p₃ = 0 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 π.

theorem euclidean_geometry.collinear_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = 0) :
{p₁, p₂, p₃}

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

theorem euclidean_geometry.collinear_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = real.pi) :
{p₁, p₂, p₃}

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

theorem euclidean_geometry.angle_ne_zero_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
p₃ 0

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

theorem euclidean_geometry.angle_ne_pi_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
p₃ real.pi

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

theorem euclidean_geometry.angle_pos_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
0 < p₃

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

theorem euclidean_geometry.angle_lt_pi_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
p₃ < real.pi

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

theorem euclidean_geometry.cos_eq_one_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
real.cos p₂ p₃) = 1 p₃ = 0

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

theorem euclidean_geometry.cos_eq_zero_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
real.cos p₂ p₃) = 0 p₃ =

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

theorem euclidean_geometry.cos_eq_neg_one_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
real.cos p₂ p₃) = -1 p₃ = real.pi

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

theorem euclidean_geometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
real.sin p₂ p₃) = 0 p₃ = 0 p₃ = real.pi

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

theorem euclidean_geometry.sin_eq_one_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
real.sin p₂ p₃) = 1 p₃ =

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

theorem euclidean_geometry.collinear_iff_eq_or_eq_or_sin_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} :
{p₁, p₂, p₃} p₁ = p₂ p₃ = p₂ real.sin 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.

theorem euclidean_geometry.sin_pos_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
0 < real.sin p₂ p₃)

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

theorem euclidean_geometry.sin_ne_zero_of_not_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : ¬ {p₁, p₂, p₃}) :
real.sin p₂ p₃) 0

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

theorem euclidean_geometry.collinear_of_sin_eq_zero {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : real.sin p₂ p₃) = 0) :
{p₁, p₂, p₃}

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