sInf_orthogonal — Mathlib

English

The infimum over a set of orthogonal subspaces equals the orthogonal to the supremum of the set.

Русский

Нижняя оболочка над множеством ортогональных подпространств равна ортогональному дополнению их супремума.

LaTeX

$$$\bigwedge K \in s (K^\perp) = (\mathrm{sSup}\, s)^\perp$$$

Lean4

/-- The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup. -/
theorem sInf_orthogonal (s : Set <| Submodule 𝕜 E) : ⨅ K ∈ s, Kᗮ = (sSup s)ᗮ :=
  (orthogonal_gc 𝕜 E).l_sSup.symm

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