case mp
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
⊢ u =O[l] v → ∃ φ _hφ, u =ᶠ[l] φ * v

case mpr
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
⊢ (∃ φ _hφ, u =ᶠ[l] φ * v) → u =O[l] v
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ φ _hφ, u =ᶠ[l] φ * v
constructor
case mp
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
case mp
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
⊢ u =O[l] v → ∃ φ _hφ, u =ᶠ[l] φ * v
rintro h
case mp.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : 0 ≤ c
hc : IsBigOWith c l u v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
case mp
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : 0 ≤ c
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
case mp.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : 0 ≤ c
hc : IsBigOWith c l u v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩
no goals
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : 0 ≤ c
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
exact ⟨φ, ⟨c, hφ⟩, huvφ⟩
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun x x_1 => x ≤ x_1) x c
⊢ u =O[l] v
case mpr
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v : α → 𝕜
⊢ (∃ φ _hφ, u =ᶠ[l] φ * v) → u =O[l] v
rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.633212
E : Type ?u.633215
F : Type ?u.633218
G : Type ?u.633221
E' : Type ?u.633224
F' : Type ?u.633227
G' : Type ?u.633230
E'' : Type ?u.633233
F'' : Type ?u.633236
G'' : Type ?u.633239
R : Type ?u.633242
R' : Type ?u.633245
𝕜 : Type u_2
𝕜' : Type ?u.633251
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 α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun x x_1 => x ≤ x_1) x c
⊢ u =O[l] v
exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩