Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.map

{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → [inst : MeasurableSpace α] → (β → γ) → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α γ

Given a function g : β → γ and a simple function f : α →ₛ β, f.map g return the simple function g ∘ f : α →ₛ γ

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

54 results in Mathlib

Foundations

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

Assumes

MeasurableSpace