Theorems · Theorem · geometry

EuclideanGeometry.similar_of_angle_angle

∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
      EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' → Similar ![a, b, c] ![a', b', c']

If two triangles have two pairs equal angles, then the triangles are similar.

Defined in

Mathlib.Geometry.Euclidean.Similarity

Cited by

0 results in Mathlib

Foundations

Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceMetricSpaceMetricSpaceNormedAddTorsorNormedAddTorsor