Theorems · Theorem · measure theory

MeasurableEquiv.map_ae

∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] (f : α ≃ᵐ β)
  (μ : MeasureTheory.Measure α),
  Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ)

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

DFunLike.coestatement and proof · cited by 62,936
Setproof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Filterstatement · cited by 8,121
Set.preimageproof · cited by 4,946
Compl.complproof · cited by 2,925
MeasureTheory.aestatement and proof · cited by 2,352
MeasureTheory.Measure.mapstatement and proof · cited by 858
Filter.mapstatement · cited by 819
MeasurableEquivstatement and proof · cited by 269
Filter.extproof · cited by 60

Cited by8

Results whose statement or proof uses this declaration.

MeasureTheory.map_add_left_aeproof · cited by 1
MeasureTheory.map_add_right_aeproof · cited by 1
MeasureTheory.map_div_right_aeproof · cited by 1
MeasureTheory.map_mul_left_aeproof · cited by 1
MeasureTheory.map_mul_right_aeproof · cited by 1
MeasureTheory.map_sub_right_aeproof · cited by 1
MeasureTheory.Measure.map_div_left_aeproof · cited by 0
MeasureTheory.Measure.map_sub_left_aeproof · cited by 0