Triangle Similarity #
This file contains theorems about similarity of triangles, including conditions for similarity based on sides and angles.
theorem
EuclideanGeometry.similar_of_angle_angle
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[NormedAddCommGroup V₁]
[NormedAddCommGroup V₂]
[InnerProductSpace ℝ V₁]
[InnerProductSpace ℝ V₂]
[MetricSpace P₁]
[MetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
{a b c : P₁}
{a' b' c' : P₂}
(h_not_col : ¬Collinear ℝ {a, b, c})
(h₁ : angle a b c = angle a' b' c')
(h₂ : angle b c a = angle b' c' a')
:
If two triangles have two pairs equal angles, then the triangles are similar.
theorem
EuclideanGeometry.similar_of_side_angle_side
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[NormedAddCommGroup V₁]
[NormedAddCommGroup V₂]
[InnerProductSpace ℝ V₁]
[InnerProductSpace ℝ V₂]
[MetricSpace P₁]
[MetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
{a b c : P₁}
{a' b' c' : P₂}
(h_not_col : ¬Collinear ℝ {a, b, c})
(h_not_col' : ¬Collinear ℝ {a', b', c'})
(h : angle a b c = angle a' b' c')
(hd : dist a b * dist b' c' = dist b c * dist a' b')
:
If two triangles have proportional adjacent sides and an equal included angle, then the triangles are similar.
theorem
Similar.angle_eq
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[NormedAddCommGroup V₁]
[NormedAddCommGroup V₂]
[InnerProductSpace ℝ V₁]
[InnerProductSpace ℝ V₂]
[MetricSpace P₁]
[MetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
{a b c : P₁}
{a' b' c' : P₂}
(h : Similar ![a, b, c] ![a', b', c'])
:
For two similar triangles, the corresponding angles are equal.
theorem
Similar.angle_eq_all
{V₁ : Type u_2}
{V₂ : Type u_3}
{P₁ : Type u_4}
{P₂ : Type u_5}
[NormedAddCommGroup V₁]
[NormedAddCommGroup V₂]
[InnerProductSpace ℝ V₁]
[InnerProductSpace ℝ V₂]
[MetricSpace P₁]
[MetricSpace P₂]
[NormedAddTorsor V₁ P₁]
[NormedAddTorsor V₂ P₂]
{a b c : P₁}
{a' b' c' : P₂}
(h : Similar ![a, b, c] ![a', b', c'])
:
EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' ∧ EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' ∧ EuclideanGeometry.angle c a b = EuclideanGeometry.angle c' a' b'
In two similar triangles, all three corresponding angles are equal.