Theorems · Theorem · geometry

EuclideanGeometry.angle_side_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' →
      dist b c = dist b' c' →
        EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' → Congruent ![a, b, c] ![a', b', c']

Angle–Side–Angle (ASA) congruence If two triangles have two equal angles and the included side equal, then the triangles are congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the other is then implied by the given equalities.

Defined in

Mathlib.Geometry.Euclidean.Congruence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceMetricSpaceMetricSpaceNormedAddTorsorNormedAddTorsor