triorthogonal_eq_orthogonal — Mathlib

English

For a subspace K, the triple orthogonal relation holds: Kᗮᗮᗮ = Kᗮ.

Русский

Для подпространства K выполняется тройное ортогоональное равенство: Kᗮᗮᗮ = Kᗮ.

LaTeX

$$$K^{\perp\perp\perp} = K^{\perp}$$$

Lean4

/-- The orthogonal complement satisfies `Kᗮᗮᗮ = Kᗮ`. -/
theorem triorthogonal_eq_orthogonal [CompleteSpace E] : Kᗮᗮᗮ = Kᗮ :=
  by
  rw [Kᗮ.orthogonal_orthogonal_eq_closure]
  exact K.isClosed_orthogonal.submodule_topologicalClosure_eq

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