α : Type u_1
β : Type ?u.296904
E : Type u_2
F : Type u_3
G : Type ?u.296913
E' : Type ?u.296916
F' : Type ?u.296919
G' : Type ?u.296922
E'' : Type ?u.296925
F'' : Type ?u.296928
G'' : Type ?u.296931
R : Type ?u.296934
R' : Type ?u.296937
𝕜 : Type ?u.296940
𝕜' : Type ?u.296943
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 α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖
α : Type u_1
β : Type ?u.296904
E : Type u_2
F : Type u_3
G : Type ?u.296913
E' : Type ?u.296916
F' : Type ?u.296919
G' : Type ?u.296922
E'' : Type ?u.296925
F'' : Type ?u.296928
G'' : Type ?u.296931
R : Type ?u.296934
R' : Type ?u.296937
𝕜 : Type ?u.296940
𝕜' : Type ?u.296943
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 α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (f =O[l] fun _x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖
simp only [isBigO_iff, norm_one, mul_one]
no goals
α : Type u_1
β : Type ?u.296904
E : Type u_2
F : Type u_3
G : Type ?u.296913
E' : Type ?u.296916
F' : Type ?u.296919
G' : Type ?u.296922
E'' : Type ?u.296925
F'' : Type ?u.296928
G'' : Type ?u.296931
R : Type ?u.296934
R' : Type ?u.296937
𝕜 : Type ?u.296940
𝕜' : Type ?u.296943
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 α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖
rfl