orthogonal_closure — Mathlib

English

The orthogonal of a closure equals the orthogonal of the subspace: (closure K)^⊥ = K^⊥.

Русский

Ортогональное дополнение замыкания подпространства равно ортогональному дополнению самого подпространства.

LaTeX

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

Lean4

/-- The closure of a submodule has the same orthogonal complement and the submodule itself. -/
@[simp]
theorem orthogonal_closure (K : Submodule 𝕜 E) : K.topologicalClosureᗮ = Kᗮ :=
  le_antisymm (orthogonal_le <| le_topologicalClosure _) fun x hx y hy ↦
    closure_minimal hx (isClosed_eq (by fun_prop) (by fun_prop)) hy

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