Theorems · Theorem · measure theory

MeasureTheory.Measure.MutuallySingular.sum_left

∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} {ι : Type u_2} [Countable ι]
  {μ : ι → MeasureTheory.Measure α},
  (MeasureTheory.Measure.sum μ).MutuallySingular ν ↔ ∀ (i : ι), (μ i).MutuallySingular ν

Defined in: Mathlib.MeasureTheory.Measure.MutuallySingular
Cited by: 2 results in Mathlib
Foundations: Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Countable

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealproof · cited by 9,879
MeasurableSetproof · cited by 3,075
Compl.complproof · cited by 2,925
le_rflproof · cited by 1,558
Set.iInterproof · cited by 1,084
Countablestatement and proof · cited by 633
MeasureTheory.Measure.sumstatement and proof · cited by 121
MeasureTheory.Measure.MutuallySingularstatement and proof · cited by 91

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.MutuallySingular.add_left_iffproof · cited by 6
MeasureTheory.Measure.MutuallySingular.sum_rightproof · cited by 0