add_left

Mathlib.MeasureTheory.Measure.MutuallySingular

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.MutuallySingular.add_left

English

If ν1 ⟂ μ and ν2 ⟂ μ, then ν1 + ν2 ⟂ μ.

Русский

Если ν1 ⟂ₘ μ и ν2 ⟂ₘ μ, тогда ν1 + ν2 ⟂ₘ μ.

LaTeX

$$$$ \\nu_1 \\perp_{m} \\mu \\land \\nu_2 \\perp_{m} \\mu \\;\Longrightarrow\\; (\\nu_1 + \\nu_2) \\perp_{m} \\mu. $$$$

Lean4

theorem add_left (h₁ : ν₁ ⟂ₘ μ) (h₂ : ν₂ ⟂ₘ μ) : ν₁ + ν₂ ⟂ₘ μ :=
  add_left_iff.2 ⟨h₁, h₂⟩

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

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

Разделы

Аффилиация

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