Theorems · Theorem · measure theory

MeasureTheory.Measure.QuasiMeasurePreserving.mono

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa μa' : MeasureTheory.Measure α}
  {μb μb' : MeasureTheory.Measure β} {f : α → β},
  μa'.AbsolutelyContinuous μa →
    μb.AbsolutelyContinuous μb' →
      MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb'

Defined in: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Cited by: 9 results in Mathlib
Foundations: Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.Measure.AbsolutelyContinuousstatement and proof · cited by 325
MeasureTheory.Measure.QuasiMeasurePreservingstatement and proof · cited by 101
MeasureTheory.Measure.QuasiMeasurePreserving.mono_leftproof · cited by 2
MeasureTheory.Measure.QuasiMeasurePreserving.mono_rightproof · cited by 1

Cited by9

Results whose statement or proof uses this declaration.

MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariantproof · cited by 7
MeasureTheory.quasiMeasurePreserving_add_leftproof · cited by 1
MeasureTheory.Conservative.congr_aeproof · cited by 1
MeasureTheory.quasiMeasurePreserving_inv_of_right_invariantproof · cited by 1
MeasureTheory.quasiMeasurePreserving_neg_of_right_invariantproof · cited by 1
MeasureTheory.quasiMeasurePreserving_divproof · cited by 0
MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariantproof · cited by 0
MeasureTheory.quasiMeasurePreserving_mul_leftproof · cited by 0
MeasureTheory.quasiMeasurePreserving_subproof · cited by 0