English
Let K be a subspace of an inner product space E. The orthogonal complement K^⊥ consists of all vectors orthogonal to every vector in K, and it can be described as the intersection of kernels of the linear functionals x ↦ ⟨x, v⟩ for v ∈ K.
Русский
Пусть K — подпространство векторного пространства E equipped с скалярным произведением. Ортогональное дополнение K^⊥ состоит из всех векторов, ортогональных каждому вектору из K; эквивалентно это пересечение ядер линейных функционалов x ↦ ⟨x, v⟩ по всем v ∈ K.
LaTeX
$$$K^\perp = \bigcap_{v \in K} \ker (\ell_v)\quad\text{где}\quad \ell_v(x)=\langle x,v\rangle$$$
Lean4
/-- `Kᗮ` can be characterized as the intersection of the kernels of the operations of
inner product with each of the elements of `K`. -/
theorem orthogonal_eq_inter : Kᗮ = ⨅ v : K, LinearMap.ker (innerSL 𝕜 (v : E)) :=
by
apply le_antisymm
· rw [le_iInf_iff]
rintro ⟨v, hv⟩ w hw
simpa using hw _ hv
· intro v hv w hw
simp only [mem_iInf] at hv
exact hv ⟨w, hw⟩
