Documentation

Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Oriented angles in right-angled triangles. #

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

source
šŸ“ coverage
theorem Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x y : V} (h : o.oangle x y = ā†‘(Real.pi / 2)) :
o.oangle x (x + y) = ā†‘(Real.arctan (ā€–yā€– / ā€–xā€–))

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

source
šŸ“ coverage
theorem Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x y : V} (h : o.oangle x y = ā†‘(Real.pi / 2)) :
o.oangle (x + y) y = ā†‘(Real.arctan (ā€–xā€– / ā€–yā€–))

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

source
šŸ“ coverage
theorem Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x y : V} (h : o.oangle x y = ā†‘(Real.pi / 2)) :
o.oangle y (y - x) = ā†‘(Real.arctan (ā€–xā€– / ā€–yā€–))

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

source
šŸ“ coverage
theorem Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x y : V} (h : o.oangle x y = ā†‘(Real.pi / 2)) :
o.oangle (x - y) x = ā†‘(Real.arctan (ā€–yā€– / ā€–xā€–))

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

source
šŸ“ coverage
theorem Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x : V} (h : x ā‰  0) (r : ā„) :
o.oangle x (x + r ā€¢ (o.rotation ā†‘(Real.pi / 2)) x) = ā†‘(Real.arctan r)

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

source
šŸ“ coverage
theorem Orientation.oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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) = ā†‘(Real.arctan rā»Ā¹)

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

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.tan_oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_right_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (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) = ā†‘(Real.arctan 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.

source
šŸ“ coverage
theorem Orientation.oangle_sub_left_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [hd2 : Fact (Module.finrank ā„ V = 2)] (o : Orientation ā„ V (Fin 2)) {x : V} (h : x ā‰  0) (r : ā„) :
o.oangle (x - r ā€¢ (o.rotation ā†‘(Real.pi / 2)) x) x = ā†‘(Real.arctan 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.

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚‚ pā‚ƒ pā‚ = ā†‘(Real.arccos (dist pā‚ƒ pā‚‚ / dist pā‚ pā‚ƒ))

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

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚ƒ pā‚ pā‚‚ = ā†‘(Real.arccos (dist pā‚ pā‚‚ / dist pā‚ pā‚ƒ))

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

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚‚ pā‚ƒ pā‚ = ā†‘(Real.arcsin (dist pā‚ pā‚‚ / dist pā‚ pā‚ƒ))

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

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚ƒ pā‚ pā‚‚ = ā†‘(Real.arcsin (dist pā‚ƒ pā‚‚ / dist pā‚ pā‚ƒ))

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

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚‚ pā‚ƒ pā‚ = ā†‘(Real.arctan (dist pā‚ pā‚‚ / dist pā‚ƒ pā‚‚))

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

source
šŸ“ coverage
theorem EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
oangle pā‚ƒ pā‚ pā‚‚ = ā†‘(Real.arctan (dist pā‚ƒ pā‚‚ / dist pā‚ pā‚‚))

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

source
šŸ“ coverage
theorem EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : angle pā‚ pā‚‚ pā‚ƒ = Real.pi / 2) :
|(oangle pā‚‚ pā‚ƒ pā‚).toReal| < Real.pi / 2

An oriented angle in a right-angled triangle (even a degenerate one) has absolute value less than Ļ€ / 2. The right-angled property is expressed using unoriented angles to cover either orientation of right-angled triangles and include degenerate cases.

source
theorem EuclideanGeometry.oangle_eq_oangle_of_two_zsmul_eq_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ pā‚„ pā‚… pā‚† : P} (h : 2 ā€¢ oangle pā‚‚ pā‚ƒ pā‚ = 2 ā€¢ oangle pā‚… pā‚† pā‚„) (hā‚ā‚‚ā‚ƒ : angle pā‚ pā‚‚ pā‚ƒ = Real.pi / 2) (hā‚„ā‚…ā‚† : angle pā‚„ pā‚… pā‚† = Real.pi / 2) :
oangle pā‚‚ pā‚ƒ pā‚ = oangle pā‚… pā‚† pā‚„

Two oriented angles in right-angled triangles are equal if twice those angles are equal.

source
theorem EuclideanGeometry.oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ pā‚„ pā‚… pā‚† : P} (h : 2 ā€¢ oangle pā‚‚ pā‚ƒ pā‚ = 2 ā€¢ oangle pā‚„ pā‚† pā‚…) (hā‚ā‚‚ā‚ƒ : angle pā‚ pā‚‚ pā‚ƒ = Real.pi / 2) (hā‚„ā‚…ā‚† : angle pā‚„ pā‚… pā‚† = Real.pi / 2) :
oangle pā‚‚ pā‚ƒ pā‚ = oangle pā‚„ pā‚† pā‚…

Two oriented angles in oppositely-oriented right-angled triangles are equal if twice those angles are equal.

source
šŸ“ coverage
theorem EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).cos = dist pā‚ƒ pā‚‚ / dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).cos = dist pā‚ pā‚‚ / dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).sin = dist pā‚ pā‚‚ / dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).sin = dist pā‚ƒ pā‚‚ / dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).tan = dist pā‚ pā‚‚ / dist pā‚ƒ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).tan = dist pā‚ƒ pā‚‚ / dist pā‚ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).cos * dist pā‚ pā‚ƒ = dist pā‚ƒ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).cos * dist pā‚ pā‚ƒ = dist pā‚ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).sin * dist pā‚ pā‚ƒ = dist pā‚ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).sin * dist pā‚ pā‚ƒ = dist pā‚ƒ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚‚ pā‚ƒ pā‚).tan * dist pā‚ƒ pā‚‚ = dist pā‚ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
(oangle pā‚ƒ pā‚ pā‚‚).tan * dist pā‚ pā‚‚ = dist pā‚ƒ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ƒ pā‚‚ / (oangle pā‚‚ pā‚ƒ pā‚).cos = dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ pā‚‚ / (oangle pā‚ƒ pā‚ pā‚‚).cos = dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ pā‚‚ / (oangle pā‚‚ pā‚ƒ pā‚).sin = dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ƒ pā‚‚ / (oangle pā‚ƒ pā‚ pā‚‚).sin = dist pā‚ pā‚ƒ

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ pā‚‚ / (oangle pā‚‚ pā‚ƒ pā‚).tan = dist pā‚ƒ pā‚‚

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

source
šŸ“ coverage
theorem EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ā„ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ā„ V = 2)] [Module.Oriented ā„ V (Fin 2)] {pā‚ pā‚‚ pā‚ƒ : P} (h : oangle pā‚ pā‚‚ pā‚ƒ = ā†‘(Real.pi / 2)) :
dist pā‚ƒ pā‚‚ / (oangle pā‚ƒ pā‚ pā‚‚).tan = dist pā‚ pā‚‚

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