Theorems · Theorem · measure theory

MeasureTheory.integrable_smul_measure

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {c : ENNReal},
  c ≠ 0 → c ≠ ⊤ → (MeasureTheory.Integrable f (c • μ) ↔ MeasureTheory.Integrable f μ)

Defined in: Mathlib.MeasureTheory.Function.L1Space.Integrable
Cited by: 5 results in Mathlib
Foundations: Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace ESeminormedAddMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Top.topstatement and proof · cited by 9,680
one_smulproof · cited by 1,374
MeasureTheory.Integrablestatement and proof · cited by 1,367
smul_smulproof · cited by 360
ESeminormedAddMonoidstatement and proof · cited by 133
ENNReal.inv_mul_cancelproof · cited by 33
ENNReal.inv_ne_topproof · cited by 12
MeasureTheory.Integrable.smul_measureproof · cited by 8

Cited by5

Results whose statement or proof uses this declaration.

IntervalIntegrable.comp_mul_leftproof · cited by 6
MeasureTheory.integrable_comp_smul_iffproof · cited by 2
MeasureTheory.integrable_inv_smul_measureproof · cited by 1
ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_selfproof · cited by 1
MeasureTheory.integrable_averageproof · cited by 0