α : Type u_2
β : Type u_1
γ : Type ?u.243975
ι : Type ?u.243978
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ ∀ (n : ℕ), ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n * FinStronglyMeasurable.approx hg n) n)) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.243975
ι : Type ?u.243978
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f * g) μ
refine'
  ⟨fun n => hf.approx n * hg.approx n, _, fun x =>
    (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩
α : Type u_2
β : Type u_1
γ : Type ?u.243975
ι : Type ?u.243978
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n * FinStronglyMeasurable.approx hg n) n)) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.243975
ι : Type ?u.243978
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ ∀ (n : ℕ), ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n * FinStronglyMeasurable.approx hg n) n)) < ⊤
intro n
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.243975
ι : Type ?u.243978
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n * FinStronglyMeasurable.approx hg n) n)) < ⊤
exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)