iInf_orthogonal — Mathlib

English

The infimum over an indexed family of orthogonal subspaces equals the orthogonal to the supremum of that family.

Русский

Наименьшее по индексу семейство ортогональных подпространств равно ортогональному дополнению над supFamily.

LaTeX

$$$\bigwedge_i (K_i)^{\perp} = (\bigvee_i K_i)^{\perp}$$$

Lean4

/-- The inf of an indexed family of orthogonal subspaces equals the
subspace orthogonal to the sup. -/
theorem iInf_orthogonal {ι : Type*} (K : ι → Submodule 𝕜 E) : ⨅ i, (K i)ᗮ = (iSup K)ᗮ :=
  (orthogonal_gc 𝕜 E).l_iSup.symm

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