angle_map — Mathlib

English

For any affine isometry f, the angle at the image points equals the angle at the original points.

Русский

Для любой аффинной изометрии f угол между изображёнными точками равен углу между исходными точками.

LaTeX

$$$\angle( f(p_1)) (f(p_2)) (f(p_3)) = \angle(p_1,p_2,p_3)$.$$

Lean4

@[simp]
theorem _root_.AffineIsometry.angle_map {V₂ P₂ : Type*} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂]
    [MetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ] P₂) (p₁ p₂ p₃ : P) : ∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃ :=
  by simp_rw [angle, ← AffineIsometry.map_vsub, LinearIsometry.angle_map]

Похожие утверждения