α : Type u_2
E : Type u_3
F✝ : Type ?u.1025604
𝕜 : Type ?u.1025607
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
bound : α → ℝ
s : Set X
hF_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s
⊢ ContinuousOn
    (fun x => if hf : Integrable fun a => F x a then ↑L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0) s
α : Type u_2
E : Type u_3
F✝ : Type ?u.1025604
𝕜 : Type ?u.1025607
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
bound : α → ℝ
s : Set X
hF_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s
⊢ ContinuousOn (fun x => ∫ (a : α), F x a ∂μ) s
simp only [integral, L1.integral]
no goals
α : Type u_2
E : Type u_3
F✝ : Type ?u.1025604
𝕜 : Type ?u.1025607
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
bound : α → ℝ
s : Set X
hF_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s
⊢ ContinuousOn
    (fun x => if hf : Integrable fun a => F x a then ↑L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0) s
exact continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
  hF_meas h_bound bound_integrable h_cont