bilinFormOfRealInner_orthogonal — Mathlib

English

In a real inner product space, the orthogonal complement K^⊥ equals the kernel of the bilinear form bilinFormOfRealInner restricted to K, i.e., K^⊥ = {x ∈ E : ⟪x, y⟫ = 0 for all y ∈ K}.

Русский

В вещественном внутренно-пространстве ортогональное дополнение K^⊥ равно ядру билинейной формы bilinFormOfRealInner, ограниченной на K, т.е. K^⊥ = {x ∈ E : ⟪x, y⟫ = 0 для всех y ∈ K}.

LaTeX

$$$K^{\perp} = \{ x \in E : \bilinFormOfRealInner(x,y)=0 \text{ for all } y \in K\}$$$

Lean4

@[simp]
theorem bilinFormOfRealInner_orthogonal {E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) :
    K.orthogonalBilin bilinFormOfRealInner = Kᗮ :=
  rfl

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