Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.map_ofFunction_le

∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : α → β),
  (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) ≤
    MeasureTheory.OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

1 results in Mathlib

Foundations

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