coe_affineIsometryOfStrictConvexSpace

English

The affine isometry constructed from a given isometry f coincides with f as a map; i.e., the underlying function of the constructed affine isometry equals f.

Русский

Аффинная изометрия, построенная из заданной изометрии f, совпадает с f как отображение; то есть функция, лежащая в основе полученной аффинной изометрии, равна f.

LaTeX

$$$\text{coe}_{\text{affine}}(f) = f$$$

Lean4

@[simp]
theorem coe_affineIsometryOfStrictConvexSpace (hi : Isometry f) : ⇑hi.affineIsometryOfStrictConvexSpace = f :=
  rfl

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