isometryOfOrthonormal_toLinearMap

English

For a linear isometry f, an orthonormal sequence v is orthonormal after applying f if and only if v was orthonormal before.

Русский

Для линейной изометрии f ортонормированная последовательность v остаётся ортонормированной после применения f ⇔ изначальная последовательность v была ортонормированной.

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v) \\iff \\operatorname{Orthonormal}_{\\mathbb{K}}(v)$.$$

Lean4

@[simp]
theorem isometryOfOrthonormal_toLinearMap (f : E →ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v)
    (hf : Orthonormal 𝕜 (f ∘ v)) : (f.isometryOfOrthonormal hv hf).toLinearMap = f :=
  rfl

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