Theorems · Theorem · measure theory

MeasureTheory.integrable_smul_iff

∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedDivisionRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜},
  c ≠ 0 → ∀ (f : α → β), MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ

Defined in: Mathlib.MeasureTheory.Function.L1Space.Integrable
Cited by: 5 results in Mathlib
Foundations: Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedDivisionRing MulActionWithZero IsBoundedSMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.Integrablestatement · cited by 1,367
NormedDivisionRingstatement and proof · cited by 360
IsBoundedSMulstatement and proof · cited by 329
MulActionWithZerostatement and proof · cited by 79
IsUnit.mk0proof · cited by 33
IsUnit.integrable_smul_iffproof · cited by 3

Cited by5

Results whose statement or proof uses this declaration.

MeasureTheory.setToFun_smulproof · cited by 3
MeasureTheory.withDensityᵥ_smulproof · cited by 2
MeasureTheory.integrableOn_Ioi_comp_rpow_iff'proof · cited by 2
MeasureTheory.integrable_fun_smul_iffproof · cited by 1
MellinConvergent.comp_mul_leftproof · cited by 0