isOrtho_iSup_left — Mathlib

English

The supremum over an indexed family is orthogonal to V iff every member is orthogonal to V.

Русский

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

LaTeX

$$$(\bigvee_i U_i) \perp V \iff \forall i, U_i \perp V$$$

Lean4

@[simp]
theorem isOrtho_iSup_left {ι : Sort*} {U : ι → Submodule 𝕜 E} {V : Submodule 𝕜 E} : iSup U ⟂ V ↔ ∀ i, U i ⟂ V :=
  iSup_le_iff

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