# mathlibdocumentation

geometry.euclidean.angle.oriented.right_angle

# Oriented angles in right-angled triangles. #

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

theorem orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle x (x + y) = (real.arccos (x / x + y))

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

theorem orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle (x + y) y = (real.arccos (y / x + y))

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

theorem orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle x (x + y) = (real.arcsin (y / x + y))

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

theorem orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle (x + y) y = (real.arcsin (x / x + y))

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

theorem orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :

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

theorem orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :

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

theorem orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).cos = x / x + y

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

theorem orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).cos = y / x + y

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

theorem orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).sin = y / x + y

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

theorem orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).sin = x / x + y

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

theorem orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).tan = y / x

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

theorem orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).tan = x / y

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

theorem orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).cos * x + y = x

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

theorem orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).cos * x + y = y

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

theorem orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).sin * x + y = y

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

theorem orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).sin * x + y = x

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

theorem orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle x (x + y)).tan * x = y

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

theorem orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x + y) y).tan * y = x

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

theorem orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle x (x + y)).cos = x + y

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

theorem orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle (x + y) y).cos = x + y

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

theorem orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle x (x + y)).sin = x + y

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

theorem orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle (x + y) y).sin = x + y

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

theorem orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle x (x + y)).tan = x

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

theorem orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle (x + y) y).tan = y

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

theorem orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle y (y - x) = (real.arccos (y / y - x))

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

theorem orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle (x - y) x = (real.arccos (x / x - y))

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

theorem orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle y (y - x) = (real.arcsin (x / y - x))

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

theorem orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
o.oangle (x - y) x = (real.arcsin (y / x - y))

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

theorem orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :

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

theorem orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :

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

theorem orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).cos = y / y - x

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

theorem orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).cos = x / x - y

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

theorem orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).sin = x / y - x

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

theorem orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).sin = y / x - y

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

theorem orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).tan = x / y

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

theorem orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).tan = y / x

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

theorem orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).cos * y - x = y

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

theorem orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).cos * 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 orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).sin * y - x = x

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

theorem orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).sin * 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 orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle y (y - x)).tan * y = x

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

theorem orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
(o.oangle (x - y) x).tan * x = y

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

theorem orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle y (y - x)).cos = y - x

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

theorem orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle (x - y) x).cos = x - y

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

theorem orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle y (y - x)).sin = y - x

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

theorem orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle (x - y) x).sin = x - y

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

theorem orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
x / (o.oangle y (y - x)).tan = y

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

theorem orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x y : V} (h : o.oangle x y = (real.pi / 2)) :
y / (o.oangle (x - y) x).tan = x

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

theorem orientation.oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :

An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple of a rotation of another by `π / 2`.

theorem orientation.oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :
o.oangle (x + r (o.rotation (real.pi / 2)) x) (r (o.rotation (real.pi / 2)) x) =

An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple of a rotation of another by `π / 2`.

theorem orientation.tan_oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :
(o.oangle x (x + r (o.rotation (real.pi / 2)) x)).tan = r

The tangent of an angle in a right-angled triangle, where one side is a multiple of a rotation of another by `π / 2`.

theorem orientation.tan_oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :
(o.oangle (x + r (o.rotation (real.pi / 2)) x) (r (o.rotation (real.pi / 2)) x)).tan = r⁻¹

The tangent of an angle in a right-angled triangle, where one side is a multiple of a rotation of another by `π / 2`.

theorem orientation.oangle_sub_right_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :
o.oangle (r (o.rotation (real.pi / 2)) x) (r (o.rotation (real.pi / 2)) x - x) =

An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple of a rotation of another by `π / 2`, version subtracting vectors.

theorem orientation.oangle_sub_left_smul_rotation_pi_div_two {V : Type u_1} [hd2 : fact (fdim V = 2)] (o : (fin 2)) {x : V} (h : x 0) (r : ) :

An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple of a rotation of another by `π / 2`, version subtracting vectors.

theorem euclidean_geometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ = (real.arccos p₂ / p₃))

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

theorem euclidean_geometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ = (real.arccos p₂ / p₃))

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

theorem euclidean_geometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ = (real.arcsin p₂ / p₃))

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

theorem euclidean_geometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ = (real.arcsin p₂ / p₃))

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

theorem euclidean_geometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁ = (real.arctan p₂ / p₂))

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

theorem euclidean_geometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ = (real.arctan p₂ / p₂))

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

theorem euclidean_geometry.cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).cos = p₂ / p₃

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

theorem euclidean_geometry.cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).cos = p₂ / p₃

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

theorem euclidean_geometry.sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).sin = p₂ / p₃

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

theorem euclidean_geometry.sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).sin = p₂ / p₃

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

theorem euclidean_geometry.tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).tan = p₂ / p₂

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

theorem euclidean_geometry.tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).tan = p₂ / p₂

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

theorem euclidean_geometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).cos * p₃ = p₂

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

theorem euclidean_geometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).cos * p₃ = p₂

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

theorem euclidean_geometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).sin * p₃ = p₂

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

theorem euclidean_geometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).sin * p₃ = p₂

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

theorem euclidean_geometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₁).tan * p₂ = p₂

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

theorem euclidean_geometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂).tan * 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_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₁).cos = p₃

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

theorem euclidean_geometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₂).cos = 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_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₁).sin = p₃

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

theorem euclidean_geometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₂).sin = 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_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₁).tan = p₂

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

theorem euclidean_geometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] [hd2 : fact (fdim V = 2)] [ (fin 2)] {p₁ p₂ p₃ : P} (h : p₃ = (real.pi / 2)) :
p₂ / p₂).tan = p₂

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