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

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

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