orthogonal — Mathlib

English

The orthogonal complement K⊥ consists of all vectors that are orthogonal to every vector in K.

Русский

Перпендиклярное дополнение K⊥ состоит из векторов, ортогональных каждому вектору из K.

LaTeX

$$$$ K^{\perp} = \{ v \in E : \langle u, v \rangle = 0 \text{ for all } u \in K \}. $$$$

Lean4

/-- The subspace of vectors orthogonal to a given subspace, denoted `Kᗮ`. -/
def orthogonal : Submodule 𝕜 E where
  carrier := {v | ∀ u ∈ K, ⟪u, v⟫ = 0}
  zero_mem' _ _ := inner_zero_right _
  add_mem' hx hy u hu := by rw [inner_add_right, hx u hu, hy u hu, add_zero]
  smul_mem' c x hx u hu := by rw [inner_smul_right, hx u hu, mul_zero]

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