Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.comap

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] → (Ω → Ω') → MeasureTheory.FiniteMeasure Ω' → MeasureTheory.FiniteMeasure Ω

The pullback of a finite measure under a map. If f is injective and sends each measurable set to a null-measurable set, then for each measurable set s we have comap f μ s = μ (f '' s). Otherwise, the pullback is defined to be zero.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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.FiniteMeasurestatement and proof · cited by 150
MeasureTheory.Measure.comapproof · cited by 96
MeasureTheory.FiniteMeasure.toMeasureproof · cited by 87

Cited by5

Results whose statement or proof uses this declaration.

isCompact_setOfPred_finiteMeasure_le_of_isCompactproof · cited by 2
Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasurestatement · cited by 1
MeasureTheory.FiniteMeasure.mass_comap_lestatement · cited by 1
MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasureproof · cited by 0
MeasureTheory.FiniteMeasure.toMeasure_comapstatement · cited by 0