Theorems · Theorem · geometry

EuclideanGeometry.angle_eq_of_congruent

∀ {ι : Type u_1} {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₂]
  {v₁ : ι → P₁} {v₂ : ι → P₂},
  Congruent v₁ v₂ →
    ∀ (i j k : ι), EuclideanGeometry.angle (v₁ i) (v₁ j) (v₁ k) = EuclideanGeometry.angle (v₂ i) (v₂ j) (v₂ k)

Corresponding angles are equal for congruent triangles.

Defined in

Mathlib.Geometry.Euclidean.Congruence

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceMetricSpaceMetricSpaceNormedAddTorsorNormedAddTorsor