Theorems · Theorem · measure theory

Measurable.fun_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
  {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun x => g (f x)

Eta-expanded form of Measurable.comp

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Defs

Cited by

95 results in Mathlib

Foundations

Depth 7 from the axioms, rests on 14 definitions · uses no axioms