no goals
α : Type u_1
β : Type ?u.1746227
γ : Type ?u.1746230
δ : Type ?u.1746233
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ (∫⁻ (x : α), AEMeasurable.mk f hf x ∂μ) ≠ ⊤
rwa [← lintegral_congr_ae hf.ae_eq_mk]
no goals
α : Type u_1
β : Type ?u.1746227
γ : Type ?u.1746230
δ : Type ?u.1746233
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h2f_meas : (∫⁻ (x : α), AEMeasurable.mk f hf x ∂μ) ≠ ⊤
x : α
hx : f x = AEMeasurable.mk f hf x
h : AEMeasurable.mk f hf x < ⊤
⊢ f x < ⊤
rwa [hx]