isClosed_orthogonal — Mathlib

English

The orthogonal complement of any subspace is a closed subset of the ambient space.

Русский

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

LaTeX

$$$\operatorname{IsClosed}(K^\perp)$$$

Lean4

/-- The orthogonal complement of any submodule `K` is closed. -/
theorem isClosed_orthogonal : IsClosed (Kᗮ : Set E) :=
  by
  rw [orthogonal_eq_inter K]
  convert isClosed_iInter <| fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))
  simp only [coe_iInf]

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