mono_right

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

English

Let V2 ≤ V1 and U ⟂ V1. Then U ⟂ V2.

Русский

Пусть V2 ⊆ V1 и U ⟂ V1. Тогда U ⟂ V2.

LaTeX

$$$(V_2 \subseteq V_1) \land (U \perp V_1) \Rightarrow (U \perp V_2)$$$

Lean4

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

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

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

Разделы

Аффилиация

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