orthogonalComplement_mem_invtSubmodule

English

If a subspace p is invariant under a linear map T, then its orthogonal complement p⊥ is also invariant under T.

Русский

Если подпространство p инвариантно относительно линейного отображения T, то его ортогональное дополнение p⊥ тоже инвариантно относительно T.

LaTeX

$$$p\\in T^{\\text{invtSubmodule}} \\Rightarrow p^{\\perp} \\in T^{\\text{invtSubmodule}}$.$$

Lean4

/-- The orthogonal complement of an invariant submodule is invariant. -/
theorem orthogonalComplement_mem_invtSubmodule (hp : p ∈ T.invtSubmodule) : pᗮ ∈ T.invtSubmodule := fun x hx y hy ↦
  hT y x ▸ hx (T y) (hp hy)

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