no goals
α : Type ?u.1279631
E : Type ?u.1279634
F : Type ?u.1279637
𝕜 : Type ?u.1279640
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.1282331
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ range f ∪ {0}
simp
α : Type u_2
E : Type u_1
F : Type ?u.1279637
𝕜 : Type ?u.1279640
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.1282331
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s
α : Type u_2
E : Type u_1
F : Type ?u.1279637
𝕜 : Type ?u.1279640
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.1282331
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f fmeas s 0 (_ : 0 ∈ s) n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)
no goals
α : Type u_2
E : Type u_1
F : Type ?u.1279637
𝕜 : Type ?u.1279640
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.1282331
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s
exact eventually_of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))