add_right_iff — Mathlib

English

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

Русский

Пусть μ, ν1 и ν2 — меры. Тогда μ ⟂ₘ ν1 + ν2 тогда и только тогда, когда μ ⟂ₘ ν1 и μ ⟂ₘ ν2.

LaTeX

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

Lean4

@[simp]
theorem add_right_iff : μ ⟂ₘ ν₁ + ν₂ ↔ μ ⟂ₘ ν₁ ∧ μ ⟂ₘ ν₂ :=
  comm.trans <| add_left_iff.trans <| and_congr comm comm

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