mono

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

English

If U2 ≤ U1 and V2 ≤ V1, and U1 ⟂ V1, then U2 ⟂ V2.

Русский

Если U2 ⊆ U1 и V2 ⊆ V1, и U1 ⟂ V1, то U2 ⟂ V2.

LaTeX

$$$(U_2 \subseteq U_1) \land (V_2 \subseteq V_1) \land (U_1 \perp V_1) \Rightarrow (U_2 \perp V_2)$$$

Lean4

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

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

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

Разделы

Аффилиация

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