Right-angled triangles

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

Implementation notes

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

References

• https://en.wikipedia.org/wiki/Pythagorean_theorem

theorem InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = Real.pi / 2

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

theorem InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq' {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) (h : angle x y = Real.pi / 2) : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, vector angle form.

theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = Real.pi / 2

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

theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq' {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) (h : angle x y = Real.pi / 2) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, subtracting vectors, vector angle form.

theorem InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

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

theorem InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y ≠ 0) : angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)

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

theorem InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0) : angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

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

theorem InnerProductGeometry.angle_add_pos_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : 0 < angle x (x + y)

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

theorem InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : angle x (x + y) ≤ Real.pi / 2

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

theorem InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0) : angle x (x + y) < Real.pi / 2

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

theorem InnerProductGeometry.cos_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖

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

theorem InnerProductGeometry.sin_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y ≠ 0) : Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖

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

theorem InnerProductGeometry.tan_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖

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

theorem InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖

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

theorem InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖

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

theorem InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y = 0) : Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖

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

theorem InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y = 0) : ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖

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

theorem InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

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

theorem InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖

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

theorem InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)

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

theorem InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y ≠ 0) : angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

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

theorem InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0) : angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)

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

theorem InnerProductGeometry.angle_sub_pos_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : 0 < angle x (x - y)

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

theorem InnerProductGeometry.angle_sub_le_pi_div_two_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : angle x (x - y) ≤ Real.pi / 2

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

theorem InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0) : angle x (x - y) < Real.pi / 2

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

theorem InnerProductGeometry.cos_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖

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

theorem InnerProductGeometry.sin_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y ≠ 0) : Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

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

theorem InnerProductGeometry.tan_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖

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

theorem InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

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

theorem InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) : Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

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

theorem InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y = 0) : Real.tan (angle x (x - y)) * ‖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 InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x ≠ 0 ∨ y = 0) : ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

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

theorem InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

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

theorem InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : inner ℝ x y = 0) (h0 : x = 0 ∨ y ≠ 0) : ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

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

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ angle p₁ p₂ p₃ = Real.pi / 2

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

theorem EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : angle p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

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

theorem EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : angle p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

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

theorem EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₃ ≠ p₂) : angle p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

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

theorem EuclideanGeometry.angle_pos_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : 0 < angle p₂ p₃ p₁

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

theorem EuclideanGeometry.angle_le_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] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : angle p₂ p₃ p₁ ≤ Real.pi / 2

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

theorem EuclideanGeometry.angle_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] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₃ ≠ p₂) : angle p₂ p₃ p₁ < Real.pi / 2

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

theorem EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : Real.cos (angle p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

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

theorem EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : Real.sin (angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

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

theorem EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : Real.tan (angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

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

theorem EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : Real.cos (angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

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

theorem EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) : Real.sin (angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

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

theorem EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : Real.tan (angle p₂ p₃ p₁) * 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.

theorem EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : dist p₃ p₂ / Real.cos (angle p₂ p₃ p₁) = dist p₁ p₃

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

theorem EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.sin (angle p₂ p₃ p₁) = dist p₁ p₃

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

theorem EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.tan (angle p₂ p₃ p₁) = dist p₃ p₂

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