affineIsometryOfStrictConvexSpace_apply

English

For any isometry f, applying the affineIsometryOfStrictConvexSpace to a point p yields f(p); i.e., the affine isometry agrees with f pointwise.

Русский

Для любой изометрии f применение к точке p аффинной изометрии дает f(p); то есть аффинная изометрия совпадает с f на каждой точке.

LaTeX

$$$\forall p:\ PF,\ \text{affineIsometryOfStrictConvexSpace}(f)(p) = f(p).$$$

Lean4

@[simp]
theorem affineIsometryOfStrictConvexSpace_apply (hi : Isometry f) (p : PF) :
    hi.affineIsometryOfStrictConvexSpace p = f p :=
  rfl

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