inner_left_of_mem_orthogonal

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

← MathLib Explorer

English

If v ∈ K⊥ and u ∈ K then ⟪v, u⟫ = 0 (by symmetry).

Русский

Если v ∈ K⊥ и u ∈ K, то ⟪v, u⟫ = 0 (по симметрии).

LaTeX

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

Lean4

/-- A vector in `Kᗮ` is orthogonal to one in `K`. -/
theorem inner_left_of_mem_orthogonal {u v : E} (hu : u ∈ K) (hv : v ∈ Kᗮ) : ⟪v, u⟫ = 0 := by rw [inner_eq_zero_symm];
  exact inner_right_of_mem_orthogonal hu hv

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

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

Разделы

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

Аффилиация

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