α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => -FinStronglyMeasurable.approx hf n) n)) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (-f) μ
refine' ⟨fun n => -hf.approx n, fun n => _, fun x => (hf.tendsto_approx x).neg⟩
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support fun x => -↑(FinStronglyMeasurable.approx hf n) x) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => -FinStronglyMeasurable.approx hf n) n)) < ⊤
suffices μ (Function.support fun x => -(hf.approx n) x) < ∞ by convert this
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support ↑(FinStronglyMeasurable.approx hf n)) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support fun x => -↑(FinStronglyMeasurable.approx hf n) x) < ⊤
rw [Function.support_neg (hf.approx n)]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ ↑↑μ (support ↑(FinStronglyMeasurable.approx hf n)) < ⊤
exact hf.fin_support_approx n
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.251943
ι : Type ?u.251946
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : TopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
this : ↑↑μ (support fun x => -↑(FinStronglyMeasurable.approx hf n) x) < ⊤
⊢ ↑↑μ (support ↑((fun n => -FinStronglyMeasurable.approx hf n) n)) < ⊤
convert this