topologicalClosure_eq_top_iff — Mathlib

English

The closure of K is the whole space iff K⊥ is trivial.

Русский

Замыкание K есть вся пространство тогда, когда K⊥ тривиально.

LaTeX

$$$K^{\text{topologicalClosure}} = \top \iff K^{\perp} = \{0\}$$$

Lean4

/-- The closure of `K` is the full space iff `Kᗮ` is trivial. -/
theorem topologicalClosure_eq_top_iff [CompleteSpace E] : K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥ :=
  by
  rw [← K.orthogonal_orthogonal_eq_closure]
  constructor <;> intro h
  · rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]
  · rw [h, Submodule.bot_orthogonal_eq_top]

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