orthogonal_range — Mathlib

English

The range of a normal operator is orthogonal to its kernel: Range(T)⊥ = Ker(T).

Русский

Образ нормального оператора ортогонален его ядру: Range(T)⊥ = Ker(T).

LaTeX

$$$\\operatorname{Im}(T)^{\\perp} = \\ker(T)$$$

Lean4

/-- The range of a normal operator is pairwise orthogonal to its kernel.

This is a weaker version of `LinearMap.IsSymmetric.orthogonal_range`
but with stronger type class assumptions (i.e., `CompleteSpace`). -/
theorem orthogonal_range (hT : IsStarNormal T) : (LinearMap.range T)ᗮ = LinearMap.ker T :=
  T.orthogonal_range ▸ hT.ker_adjoint_eq_ker

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