Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.extend

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

Extend a SimpleFunc along a measurable embedding: f₁.extend g hg f₂ is the function F : β →ₛ γ such that F ∘ g = f₁ and F y = f₂ y whenever y ∉ range g.

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

7 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace