Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.pair

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

Combine two simple functions f : α →ₛ β and g : α →ₛ β into fun a => (f a, g a).

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

16 results in Mathlib

Foundations

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

Assumes

MeasurableSpace