Theorems · Theorem · measure theory

MeasureTheory.integrable_comp

∀ {E' : Type u_2} {F' : Type u_3} {A : Type u_4} [inst : NormedAddCommGroup E'] [inst_1 : InnerProductSpace ℝ E']
  [inst_2 : FiniteDimensional ℝ E'] [inst_3 : MeasurableSpace E'] [inst_4 : BorelSpace E']
  [inst_5 : NormedAddCommGroup F'] [inst_6 : InnerProductSpace ℝ F'] [inst_7 : FiniteDimensional ℝ F']
  [inst_8 : MeasurableSpace F'] [inst_9 : BorelSpace F'] (f : E' ≃ₗᵢ[ℝ] F') [inst_10 : NormedAddCommGroup A]
  (g : F' → A), MeasureTheory.Integrable (g ∘ ⇑f) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume

Defined in

Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedAddCommGroup