isOrtho_sSup_left — Mathlib

English

The supremum of a set of subspaces is orthogonal to V iff every member is orthogonal to V.

Русский

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

LaTeX

$$\operatorname{sSup} U \perp V \iff \forall U_i \in U, U_i \perp V$$

Lean4

@[simp]
theorem isOrtho_sSup_left {U : Set (Submodule 𝕜 E)} {V : Submodule 𝕜 E} : sSup U ⟂ V ↔ ∀ Uᵢ ∈ U, Uᵢ ⟂ V :=
  sSup_le_iff

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