α : Type u_3
β : Type ?u.690828
E : Type ?u.690831
F : Type ?u.690834
G : Type ?u.690837
E'✝ : Type ?u.690840
F' : Type u_4
G' : Type ?u.690846
E'' : Type ?u.690849
F'' : Type ?u.690852
G'' : Type ?u.690855
R : Type ?u.690858
R' : Type ?u.690861
𝕜 : Type ?u.690864
𝕜' : Type ?u.690867
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 : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
α : Type u_3
β : Type ?u.690828
E : Type ?u.690831
F : Type ?u.690834
G : Type ?u.690837
E'✝ : Type ?u.690840
F' : Type u_4
G' : Type ?u.690846
E'' : Type ?u.690849
F'' : Type ?u.690852
G'' : Type ?u.690855
R : Type ?u.690858
R' : Type ?u.690861
𝕜 : Type ?u.690864
𝕜' : Type ?u.690867
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 : ℝ
hC : 0 ≤ C
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
have : ∀ x, 0 ≤ C * ‖g' x‖ := fun x => mul_nonneg hC (norm_nonneg _)
no goals
α : Type u_3
β : Type ?u.690828
E : Type ?u.690831
F : Type ?u.690834
G : Type ?u.690837
E'✝ : Type ?u.690840
F' : Type u_4
G' : Type ?u.690846
E'' : Type ?u.690849
F'' : Type ?u.690852
G'' : Type ?u.690855
R : Type ?u.690858
R' : Type ?u.690861
𝕜 : Type ?u.690864
𝕜' : Type ?u.690867
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 : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x => f x i) g'
simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]