add_left_iff — Mathlib

English

Let μ1, μ2, and ν be measures on a measurable space. Then μ1 + μ2 is mutually singular with ν if and only if μ1 is mutually singular with ν and μ2 is mutually singular with ν.

Русский

Пусть μ1, μ2 и ν — меры на измеримом пространстве. Тогда μ1 + μ2 взаимно-сингуларна по отношению к ν тогда и только тогда, когда μ1⊥ν и μ2⊥ν.

LaTeX

$$$$(\\mu_1 + \\mu_2) \\perp_{m} \\nu \\;\\iff\\; (\\mu_1 \\perp_{m} \\nu) \\land (\\mu_2 \\perp_{m} \\nu).$$$$

Lean4

@[simp]
theorem add_left_iff : μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν := by
  rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]

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