geometry.euclidean.angle.oriented.right_angle

source

theorem orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_right_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.tan_oangle_add_left_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_right_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem orientation.oangle_sub_left_smul_rotation_pi_div_two {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] [hd2 : fact (fdim 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

theorem euclidean_geometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₂ p₃ p₁ = ↑(real.arccos (has_dist.dist p₃ p₂ / has_dist.dist p₁ p₃))

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

source

theorem euclidean_geometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₃ p₁ p₂ = ↑(real.arccos (has_dist.dist p₁ p₂ / has_dist.dist p₁ p₃))

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

source

theorem euclidean_geometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₂ p₃ p₁ = ↑(real.arcsin (has_dist.dist p₁ p₂ / has_dist.dist p₁ p₃))

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

source

theorem euclidean_geometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₃ p₁ p₂ = ↑(real.arcsin (has_dist.dist p₃ p₂ / has_dist.dist p₁ p₃))

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

source

theorem euclidean_geometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₂ p₃ p₁ = ↑(real.arctan (has_dist.dist p₁ p₂ / has_dist.dist p₃ p₂))

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

source

theorem euclidean_geometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

euclidean_geometry.oangle p₃ p₁ p₂ = ↑(real.arctan (has_dist.dist p₃ p₂ / has_dist.dist p₁ p₂))

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

source

theorem euclidean_geometry.cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).cos = has_dist.dist p₃ p₂ / has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).cos = has_dist.dist p₁ p₂ / has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).sin = has_dist.dist p₁ p₂ / has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).sin = has_dist.dist p₃ p₂ / has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).tan = has_dist.dist p₁ p₂ / has_dist.dist p₃ p₂

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

source

theorem euclidean_geometry.tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).tan = has_dist.dist p₃ p₂ / has_dist.dist p₁ p₂

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

source

theorem euclidean_geometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).cos * has_dist.dist p₁ p₃ = has_dist.dist p₃ p₂

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

source

theorem euclidean_geometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).cos * has_dist.dist p₁ p₃ = has_dist.dist p₁ p₂

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

source

theorem euclidean_geometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).sin * has_dist.dist p₁ p₃ = has_dist.dist p₁ p₂

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

source

theorem euclidean_geometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).sin * has_dist.dist p₁ p₃ = has_dist.dist p₃ p₂

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

source

theorem euclidean_geometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₂ p₃ p₁).tan * has_dist.dist p₃ p₂ = has_dist.dist p₁ p₂

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

source

theorem euclidean_geometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

(euclidean_geometry.oangle p₃ p₁ p₂).tan * has_dist.dist p₁ p₂ = has_dist.dist p₃ p₂

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

source

theorem euclidean_geometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₃ p₂ / (euclidean_geometry.oangle p₂ p₃ p₁).cos = has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₁ p₂ / (euclidean_geometry.oangle p₃ p₁ p₂).cos = has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₁ p₂ / (euclidean_geometry.oangle p₂ p₃ p₁).sin = has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₃ p₂ / (euclidean_geometry.oangle p₃ p₁ p₂).sin = has_dist.dist p₁ p₃

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

source

theorem euclidean_geometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₁ p₂ / (euclidean_geometry.oangle p₂ p₃ p₁).tan = has_dist.dist p₃ p₂

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

source

theorem euclidean_geometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [hd2 : fact (fdim V = 2)] [module.oriented ℝ V (fin 2)] {p₁ p₂ p₃ : P} (h : euclidean_geometry.oangle p₁ p₂ p₃ = ↑(real.pi / 2)) :

has_dist.dist p₃ p₂ / (euclidean_geometry.oangle p₃ p₁ p₂).tan = has_dist.dist p₁ p₂

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

mathlib3 documentation

Oriented angles in right-angled triangles. #