Theorems · Theorem · measure theory

Measurable.pow_const

∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {f : α → β},
  Measurable f → ∀ (c : γ), Measurable fun x => f x ^ c

Defined in

Mathlib.MeasureTheory.Group.Arithmetic

Cited by

26 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpacePowMeasurablePow