α : Type u_1
β : Type ?u.966398
γ : Type ?u.966401
δ : Type ?u.966404
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ ε * ↑↑μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.966398
γ : Type ?u.966401
δ : Type ?u.966404
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ ↑↑μ {x | ε ≤ f x} * ε ≤ ∫⁻ (a : α), f a ∂μ
rw [mul_comm]
no goals
α : Type u_1
β : Type ?u.966398
γ : Type ?u.966401
δ : Type ?u.966404
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ⊤
⊢ ε * ↑↑μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
exact mul_meas_ge_le_lintegral₀ hf ε