toRealLinearIsometryEquiv_apply — Mathlib

English

In the real setting, dist(pointReflection Real x y, y) equals 2 times dist x y.

Русский

В вещественном случае dist(pointReflection Real x y, y) = 2 · dist(x, y).

LaTeX

$$$\operatorname{dist}(\operatorname{pointReflection}_{\mathbb{R}}(x)(y), y) = 2 \cdot \operatorname{dist}(x, y)$$$

Lean4

@[simp]
theorem toRealLinearIsometryEquiv_apply (f : E ≃ᵢ F) (x : E) : (f.toRealLinearIsometryEquiv : E → F) x = f x - f 0 :=
  (sub_eq_add_neg (f x) (f 0)).symm

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