Theorem: Measure_theory.continuous_integral_trim (Untitled/Probability/Indep.lean)

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => integral μ ↑↑f
Tactic:
simp_rw [← integral_congr_ae Lp_trim_to_Lp.ae_eq]
State after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => ∫ (a : α), ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ Continuous fun f => ∫ (a : α), ↑↑(Lp_trim_to_Lp 1 μ hm f) a ∂μ
Tactic:
exact continuous_integral.comp Lp_trim_to_Lp.isometry.continuous
State after:
no goals