comp_linearIsometry — Mathlib

English

A linear isometry preserves the property of being orthonormal under composition: if v is orthonormal, then f ∘ v is orthonormal for any linear isometry f.

Русский

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

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(v) \\implies \\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v)$ for a linear isometry $f$.$$

Lean4

/-- A linear isometry preserves the property of being orthonormal. -/
theorem comp_linearIsometry {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (f ∘ v) := by
  rwa [f.orthonormal_comp_iff]

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