mono_left

Mathlib.Analysis.InnerProductSpace.Orthogonal

URI: https://scilib.ai/kg/mathlib#Submodule.IsOrtho.mono_left

English

Let U2 be a submodule of U1 and U1 be orthogonal to V. Then U2 is orthogonal to V.

Русский

Пусть U2 ≤ U1 и U1 ≡ V взаимно ортогональны. Тогда U2 ортогонально V.

LaTeX

$$$(U_2 \subseteq U_1) \wedge (U_1 \perp V) \Rightarrow (U_2 \perp V)$$$

Lean4

theorem mono_left {U₁ U₂ V : Submodule 𝕜 E} (hU : U₂ ≤ U₁) (h : U₁ ⟂ V) : U₂ ⟂ V :=
  hU.trans h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru