English
In a Hilbert space, the double orthogonal is the closure of the original subspace.
Русский
В пространстве Гильберта двойственное ортогональное множество равно замыканию исходного подппространства.
LaTeX
$$$K^{\perp\perp} = \overline{K}$$$
Lean4
/-- In a Hilbert space, the orthogonal complement of the orthogonal complement of a subspace `K`
is the topological closure of `K`.
Note that the completeness assumption is necessary. Let `E` be the space `ℕ →₀ ℝ` with inner space
structure inherited from `PiLp 2 (fun _ : ℕ ↦ ℝ)`. Let `K` be the subspace of sequences with the sum
of all elements equal to zero. Then `Kᗮ = ⊥`, `Kᗮᗮ = ⊤`. -/
theorem orthogonal_orthogonal_eq_closure [CompleteSpace E] : Kᗮᗮ = K.topologicalClosure :=
by
refine le_antisymm ?_ ?_
· convert Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure using 1
rw [K.topologicalClosure.orthogonal_orthogonal]
· exact K.topologicalClosure_minimal K.le_orthogonal_orthogonal Kᗮ.isClosed_orthogonal
