α : Type u_3
β : Type ?u.694033
E : Type ?u.694036
F : Type ?u.694039
G : Type ?u.694042
E'✝ : Type ?u.694045
F' : Type u_4
G' : Type ?u.694051
E'' : Type ?u.694054
F'' : Type ?u.694057
G'' : Type ?u.694060
R : Type ?u.694063
R' : Type ?u.694066
𝕜 : Type ?u.694069
𝕜' : Type ?u.694072
inst✝¹⁴ : Norm E
inst✝¹³ : Norm F
inst✝¹² : Norm G
inst✝¹¹ : SeminormedAddCommGroup E'✝
inst✝¹⁰ : SeminormedAddCommGroup F'
inst✝⁹ : SeminormedAddCommGroup G'
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedAddCommGroup F''
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : SeminormedRing R
inst✝⁴ : SeminormedRing R'
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g : α → F
k : α → G
f' : α → E'✝
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
ι : Type u_1
inst✝¹ : Fintype ι
E' : ι → Type u_2
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x => f x i) g'
α : Type u_3
β : Type ?u.694033
E : Type ?u.694036
F : Type ?u.694039
G : Type ?u.694042
E'✝ : Type ?u.694045
F' : Type u_4
G' : Type ?u.694051
E'' : Type ?u.694054
F'' : Type ?u.694057
G'' : Type ?u.694060
R : Type ?u.694063
R' : Type ?u.694066
𝕜 : Type ?u.694069
𝕜' : Type ?u.694072
inst✝¹⁴ : Norm E
inst✝¹³ : Norm F
inst✝¹² : Norm G
inst✝¹¹ : SeminormedAddCommGroup E'✝
inst✝¹⁰ : SeminormedAddCommGroup F'
inst✝⁹ : SeminormedAddCommGroup G'
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedAddCommGroup F''
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : SeminormedRing R
inst✝⁴ : SeminormedRing R'
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g : α → F
k : α → G
f' : α → E'✝
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
ι : Type u_1
inst✝¹ : Fintype ι
E' : ι → Type u_2
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =O[l] g' ↔ ∀ (i : ι), (fun x => f x i) =O[l] g'
simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]
no goals
α : Type u_3
β : Type ?u.694033
E : Type ?u.694036
F : Type ?u.694039
G : Type ?u.694042
E'✝ : Type ?u.694045
F' : Type u_4
G' : Type ?u.694051
E'' : Type ?u.694054
F'' : Type ?u.694057
G'' : Type ?u.694060
R : Type ?u.694063
R' : Type ?u.694066
𝕜 : Type ?u.694069
𝕜' : Type ?u.694072
inst✝¹⁴ : Norm E
inst✝¹³ : Norm F
inst✝¹² : Norm G
inst✝¹¹ : SeminormedAddCommGroup E'✝
inst✝¹⁰ : SeminormedAddCommGroup F'
inst✝⁹ : SeminormedAddCommGroup G'
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedAddCommGroup F''
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : SeminormedRing R
inst✝⁴ : SeminormedRing R'
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f✝ : α → E
g : α → F
k : α → G
f' : α → E'✝
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
ι : Type u_1
inst✝¹ : Fintype ι
E' : ι → Type u_2
inst✝ : (i : ι) → NormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x => f x i) g'
exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)