_aux_Mathlib_Geometry_Euclidean_Angle_Unoriented_Affine___macroRules_EuclideanGeometry_term∠_1

English

For an affine isometry f, the angle between the images of three points equals the angle between the original three points.

Русский

Пусть f — аффинная изометрия; угол между изображениями трёх точек равен углу между исходными тремя точками.

LaTeX

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

Lean4

@[scoped macro EuclideanGeometry.«term∠»]
public meta def «_aux_Mathlib_Geometry_Euclidean_Angle_Unoriented_Affine___macroRules_EuclideanGeometry_term∠_1» :
    Macro✝ := fun
  | `(∠) => ``(EuclideanGeometry.angle)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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