coe_toRealAffineIsometryEquiv — Mathlib

English

Let f be an isometry between two metric affine spaces PE and PF. The real-affine realization of f has the same underlying isometry as f; i.e., the corresponding isometry equivalence equals f.

Русский

Пусть f — изометрическое эквивалентное отображение между метрическими аффинными пространствами PE и PF. Соответствующее ему изометрическое отображение через вещественную афинную реализацию совпадает с f.

LaTeX

$$$f.toRealAffineIsometryEquiv.toIsometryEquiv = f$$$

Lean4

@[simp]
theorem coe_toRealAffineIsometryEquiv (f : PE ≃ᵢ PF) : f.toRealAffineIsometryEquiv.toIsometryEquiv = f :=
  by
  ext
  rfl

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