isOrtho_sSup_right — Mathlib

English

U ⟂ sSup V iff ∀ V_i ∈ V, U ⟂ V_i.

Русский

U ⟂ sSup V тогда и только тогда, когда для каждого V_i внутри V выполняется U ⟂ V_i.

LaTeX

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

Lean4

@[simp]
theorem isOrtho_sSup_right {U : Submodule 𝕜 E} {V : Set (Submodule 𝕜 E)} : U ⟂ sSup V ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ :=
  isOrtho_comm.trans <| isOrtho_sSup_left.trans <| by simp_rw [isOrtho_comm]

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