inner_right_of_mem_orthogonal

Mathlib.Analysis.InnerProductSpace.Orthogonal

URI: https://scilib.ai/kg/mathlib#Submodule.inner_right_of_mem_orthogonal

← MathLib Explorer

English

If u ∈ K and v ∈ K⊥ then ⟪u, v⟫ = 0.

Русский

Если u ∈ K и v ∈ K⊥, то ⟪u, v⟫ = 0.

LaTeX

$$$$ \langle u, v \rangle = 0. $$$$

Lean4

/-- A vector in `K` is orthogonal to one in `Kᗮ`. -/
theorem inner_right_of_mem_orthogonal {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) : ⟪u, v⟫ = 0 :=
  (K.mem_orthogonal v).1 hv u hu

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru