no goals
α : Type u_1
β : Type ?u.481261
E : Type ?u.481264
F : Type ?u.481267
G : Type ?u.481270
E' : Type ?u.481273
F' : Type ?u.481276
G' : Type ?u.481279
E'' : Type ?u.481282
F'' : Type ?u.481285
G'' : Type ?u.481288
R : Type u_2
R' : Type ?u.481294
𝕜 : Type u_3
𝕜' : Type ?u.481300
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 α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 0 ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ 0) fun x => g x ^ 0
simpa using isBigOWith_const_const (1 : R) (one_ne_zero' 𝕜) l
no goals
α : Type u_1
β : Type ?u.481261
E : Type ?u.481264
F : Type ?u.481267
G : Type ?u.481270
E' : Type ?u.481273
F' : Type ?u.481276
G' : Type ?u.481279
E'' : Type ?u.481282
F'' : Type ?u.481285
G'' : Type ?u.481288
R : Type u_2
R' : Type ?u.481294
𝕜 : Type u_3
𝕜' : Type ?u.481300
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 α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 1 ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ 1) fun x => g x ^ 1
simpa
no goals
α : Type u_1
β : Type ?u.481261
E : Type ?u.481264
F : Type ?u.481267
G : Type ?u.481270
E' : Type ?u.481273
F' : Type ?u.481276
G' : Type ?u.481279
E'' : Type ?u.481282
F'' : Type ?u.481285
G'' : Type ?u.481288
R : Type u_2
R' : Type ?u.481294
𝕜 : Type u_3
𝕜' : Type ?u.481300
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 α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
n : ℕ
⊢ IsBigOWith (Nat.casesOn (n + 2) ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ (n + 2)) fun x => g x ^ (n + 2)
simpa [pow_succ] using h.mul (IsBigOWith.pow' h (n + 1))