map — Mathlib

English

If U ⟂ V, then U.map f ⟂ V.map f for a linear isometry f.

Русский

Если U ⟂ V, то U.map f ⟂ V.map f для линейного изометрического отображения f.

LaTeX

$$(U \perp V) \Rightarrow (U.map f \perp V.map f)$$

Lean4

theorem map (f : E →ₗᵢ[𝕜] F) {U V : Submodule 𝕜 E} (h : U ⟂ V) : U.map f ⟂ V.map f :=
  by
  rw [isOrtho_iff_inner_eq] at *
  simp_rw [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, LinearIsometry.inner_map_map]
  exact h

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