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]