Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.MutuallySingular

{α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : AddCommMonoid M] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : TopologicalSpace N] → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α N → Prop

Two vector measures v and w are said to be mutually singular if there exists a measurable set s, such that for all t ⊆ s, v t = 0 and for all t ⊆ sᶜ, w t = 0. We note that we do not require the measurability of t in the definition since this makes it easier to use. This is equivalent to the definition which requires measurability. To prove MutuallySingular with the measurability condition, use MeasureTheory.VectorMeasure.MutuallySingular.mk.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

20 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpaceAddCommMonoidTopologicalSpace