# mathlib3documentation

geometry.euclidean.angle.unoriented.right_angle

# Right-angled triangles #

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

This file proves basic geometrical results about distances and angles in (possibly degenerate) right-angled triangles in real inner product spaces and Euclidean affine spaces.

## Implementation notes #

Results in this file are generally given in a form with only those non-degeneracy conditions needed for the particular result, rather than requiring affine independence of the points of a triangle unnecessarily.

## References #

Pythagorean theorem, if-and-only-if vector angle form.

Pythagorean theorem, vector angle form.

Pythagorean theorem, subtracting vectors, if-and-only-if vector angle form.

Pythagorean theorem, subtracting vectors, vector angle form.

theorem inner_product_geometry.angle_add_eq_arccos_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
(x + y) = real.arccos (x / x + y)

An angle in a right-angled triangle expressed using arccos.

theorem inner_product_geometry.angle_add_eq_arcsin_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y 0) :
(x + y) = real.arcsin (y / x + y)

An angle in a right-angled triangle expressed using arcsin.

theorem inner_product_geometry.angle_add_eq_arctan_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0) :

An angle in a right-angled triangle expressed using arctan.

theorem inner_product_geometry.angle_add_pos_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :
0 < (x + y)

An angle in a non-degenerate right-angled triangle is positive.

theorem inner_product_geometry.angle_add_le_pi_div_two_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
(x + y)

An angle in a right-angled triangle is at most π / 2.

theorem inner_product_geometry.angle_add_lt_pi_div_two_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0) :
(x + y) <

An angle in a non-degenerate right-angled triangle is less than π / 2.

theorem inner_product_geometry.cos_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.cos (x + y)) = x / x + y

The cosine of an angle in a right-angled triangle as a ratio of sides.

theorem inner_product_geometry.sin_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y 0) :
real.sin (x + y)) = y / x + y

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem inner_product_geometry.tan_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem inner_product_geometry.cos_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.cos (x + y)) * x + y = x

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

theorem inner_product_geometry.sin_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.sin (x + y)) * x + y = y

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem inner_product_geometry.tan_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y = 0) :

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem inner_product_geometry.norm_div_cos_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y = 0) :
x / real.cos (x + y)) = x + y

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

theorem inner_product_geometry.norm_div_sin_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :
y / real.sin (x + y)) = x + y

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem inner_product_geometry.norm_div_tan_angle_add_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.

theorem inner_product_geometry.angle_sub_eq_arccos_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
(x - y) = real.arccos (x / x - y)

An angle in a right-angled triangle expressed using arccos, version subtracting vectors.

theorem inner_product_geometry.angle_sub_eq_arcsin_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y 0) :
(x - y) = real.arcsin (y / x - y)

An angle in a right-angled triangle expressed using arcsin, version subtracting vectors.

theorem inner_product_geometry.angle_sub_eq_arctan_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0) :

An angle in a right-angled triangle expressed using arctan, version subtracting vectors.

theorem inner_product_geometry.angle_sub_pos_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :
0 < (x - y)

An angle in a non-degenerate right-angled triangle is positive, version subtracting vectors.

theorem inner_product_geometry.angle_sub_le_pi_div_two_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
(x - y)

An angle in a right-angled triangle is at most π / 2, version subtracting vectors.

theorem inner_product_geometry.angle_sub_lt_pi_div_two_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0) :
(x - y) <

An angle in a non-degenerate right-angled triangle is less than π / 2, version subtracting vectors.

theorem inner_product_geometry.cos_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.cos (x - y)) = x / x - y

The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem inner_product_geometry.sin_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y 0) :
real.sin (x - y)) = y / x - y

The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem inner_product_geometry.tan_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :

The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting vectors.

theorem inner_product_geometry.cos_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.cos (x - y)) * x - y = x

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side, version subtracting vectors.

theorem inner_product_geometry.sin_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) :
real.sin (x - y)) * x - y = y

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side, version subtracting vectors.

theorem inner_product_geometry.tan_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y = 0) :

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side, version subtracting vectors.

theorem inner_product_geometry.norm_div_cos_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x 0 y = 0) :
x / real.cos (x - y)) = x - y

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse, version subtracting vectors.

theorem inner_product_geometry.norm_div_sin_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :
y / real.sin (x - y)) = x - y

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse, version subtracting vectors.

theorem inner_product_geometry.norm_div_tan_angle_sub_of_inner_eq_zero {V : Type u_1} {x y : V} (h : = 0) (h0 : x = 0 y 0) :

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side, version subtracting vectors.

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

Pythagorean theorem, if-and-only-if angle-at-point form.

theorem euclidean_geometry.angle_eq_arccos_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) :
p₁ = real.arccos p₂ / p₃)

An angle in a right-angled triangle expressed using arccos.

theorem euclidean_geometry.angle_eq_arcsin_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₁ p₂ p₃ p₂) :
p₁ = real.arcsin p₂ / p₃)

An angle in a right-angled triangle expressed using arcsin.

theorem euclidean_geometry.angle_eq_arctan_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₃ p₂) :
p₁ = real.arctan p₂ / p₂)

An angle in a right-angled triangle expressed using arctan.

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

An angle in a non-degenerate right-angled triangle is positive.

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

An angle in a right-angled triangle is at most π / 2.

theorem euclidean_geometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₃ p₂) :
p₁ <

An angle in a non-degenerate right-angled triangle is less than π / 2.

theorem euclidean_geometry.cos_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) :
real.cos p₃ p₁) = p₂ / p₃

The cosine of an angle in a right-angled triangle as a ratio of sides.

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

The sine of an angle in a right-angled triangle as a ratio of sides.

theorem euclidean_geometry.tan_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) :
real.tan p₃ p₁) = p₂ / p₂

The tangent of an angle in a right-angled triangle as a ratio of sides.

theorem euclidean_geometry.cos_angle_mul_dist_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) :
real.cos p₃ p₁) * p₃ = p₂

The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the adjacent side.

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

The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the opposite side.

theorem euclidean_geometry.tan_angle_mul_dist_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₁ = p₂ p₃ p₂) :
real.tan p₃ p₁) * p₂ = p₂

The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals the opposite side.

theorem euclidean_geometry.dist_div_cos_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₁ = p₂ p₃ p₂) :
p₂ / real.cos p₃ p₁) = p₃

A side of a right-angled triangle divided by the cosine of the adjacent angle equals the hypotenuse.

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

A side of a right-angled triangle divided by the sine of the opposite angle equals the hypotenuse.

theorem euclidean_geometry.dist_div_tan_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : p₃ = ) (h0 : p₁ p₂ p₃ = p₂) :
p₂ / real.tan p₃ p₁) = p₂

A side of a right-angled triangle divided by the tangent of the opposite angle equals the adjacent side.