add_right

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.MutuallySingular.add_right

English

Let v ⟂ᵥ w1 and v ⟂ᵥ w2. Then v ⟂ᵥ w1 + w2.

Русский

Пусть v ⟂ᵥ w1 и v ⟂ᵥ w2. Тогда v ⟂ᵥ w1 + w2.

LaTeX

$$$ (v \\perp_{\\mathcal{V}} w_1) \\land (v \\perp_{\\mathcal{V}} w_2) \\implies v \\perp_{\\mathcal{V}} (w_1 + w_2) $$$

Lean4

theorem add_right [T2Space M] [ContinuousAdd N] (h₁ : v ⟂ᵥ w₁) (h₂ : v ⟂ᵥ w₂) : v ⟂ᵥ w₁ + w₂ :=
  (add_left h₁.symm h₂.symm).symm

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

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

Разделы

Аффилиация

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