Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.mapHom

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        {f : Ω → Ω'} → Measurable f → MeasureTheory.FiniteMeasure Ω →ₗ[NNReal] MeasureTheory.FiniteMeasure Ω'

The push-forward of a finite measure by a function between measurable spaces as a linear map.

Defined in: Mathlib.MeasureTheory.Measure.FiniteMeasure
Cited by: 0 results in Mathlib
Foundations: Depth 203 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.

Cites9

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

RingHom.idstatement · cited by 18,349
MeasurableSpacestatement and proof · cited by 13,106
LinearMapstatement · cited by 10,215
NNRealstatement · cited by 4,310
Measurablestatement and proof · cited by 1,499
MeasureTheory.FiniteMeasurestatement and proof · cited by 150
MeasureTheory.FiniteMeasure.mapproof · cited by 16
MeasureTheory.FiniteMeasure.map_addproof · cited by 0
MeasureTheory.FiniteMeasure.map_smulproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.