Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.mapCLM

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        [inst_2 : TopologicalSpace Ω] →
          [inst_3 : OpensMeasurableSpace Ω] →
            [inst_4 : TopologicalSpace Ω'] →
              [inst_5 : BorelSpace Ω'] →
                {f : Ω → Ω'} → Continuous f → MeasureTheory.FiniteMeasure Ω →L[NNReal] MeasureTheory.FiniteMeasure Ω'

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

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceTopologicalSpaceOpensMeasurableSpaceTopologicalSpaceBorelSpace