inf_orthogonal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The inf of two orthogonal subspaces equals the subspace orthogonal
to the sup. -/
theorem inf_orthogonal (K₁ K₂ : Submodule 𝕜 E) : K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ :=
  (orthogonal_gc 𝕜 E).l_sup.symm

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