sum_right — Mathlib

English

For a countable index set, mutual singularity of μ with sum ν is equivalent to mutual singularity with each ν i.

Русский

Для счётного множества индексов взаимная неразделимость μ с суммой ν эквивалентна взаимной неразделимости μ с каждым ν_i.

LaTeX

$$$\\forall ι\\, [Countable ι],\\; \\mu \\perp_m (\\sum_i \\nu_i) \\iff \\forall i, \\mu \\perp_m \\nu_i$$$

Lean4

@[simp]
theorem sum_right {ι : Type*} [Countable ι] {ν : ι → Measure α} : μ ⟂ₘ sum ν ↔ ∀ i, μ ⟂ₘ ν i :=
  comm.trans <| sum_left.trans <| forall_congr' fun _ => comm

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