comp_linearIsometryEquiv — Mathlib

English

A linear isometric equivalence preserves orthonormality under composition: if v is orthonormal, then f ∘ v is orthonormal for any linear isometric equivalence f.

Русский

Линейная изометрическая эквивалентность сохраняет ортонормированность при композиции: если v ортонормальна, то f ∘ v ортонормирована для любой линейной изометрической эквивалентности f.

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(v) \\Rightarrow \\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v)$ for a linear isometric equivalence $f$.$$

Lean4

/-- A linear isometric equivalence preserves the property of being orthonormal. -/
theorem comp_linearIsometryEquiv {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 (f ∘ v) :=
  hv.comp_linearIsometry f.toLinearIsometry

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