α : Type u_3
β : Type u_2
γ : Type ?u.268899
ι : Type ?u.268902
inst✝⁶ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ ↑↑μ (support ↑((fun n => c • FinStronglyMeasurable.approx hf n) n)) < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.268899
ι : Type ?u.268902
inst✝⁶ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ
refine' ⟨fun n => c • hf.approx n, fun n => _, fun x => (hf.tendsto_approx x).const_smul c⟩
α : Type u_3
β : Type u_2
γ : Type ?u.268899
ι : Type ?u.268902
inst✝⁶ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ ↑↑μ (support (c • ↑(FinStronglyMeasurable.approx hf n))) < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.268899
ι : Type ?u.268902
inst✝⁶ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ ↑↑μ (support ↑((fun n => c • FinStronglyMeasurable.approx hf n) n)) < ⊤
rw [SimpleFunc.coe_smul]
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.268899
ι : Type ?u.268902
inst✝⁶ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ ↑↑μ (support (c • ↑(FinStronglyMeasurable.approx hf n))) < ⊤
refine' (measure_mono (support_smul_subset_right c _)).trans_lt (hf.fin_support_approx n)