ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<GOAL>f =O[⊥] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<GOAL>f =o[⊥] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>x : α<GOAL>Asymptotics.IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l l' : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>h' : Asymptotics.IsBigOWith c l' f g<GOAL>Asymptotics.IsBigOWith c (l ⊔ l') f g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>c c' : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l l' : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<VAR>h' : Asymptotics.IsBigOWith c' l' f g'<GOAL>Asymptotics.IsBigOWith (max c c') (l ⊔ l') f g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l l' : Filter α<VAR>h : f =O[l] g'<VAR>h' : f =O[l'] g'<GOAL>f =O[l ⊔ l'] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>l l' : Filter α<VAR>h : f =o[l] g<VAR>h' : f =o[l'] g<GOAL>f =o[l ⊔ l'] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l l' : Filter α<GOAL>f =O[l ⊔ l'] g' ↔ f =O[l] g' ∧ f =O[l'] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>l l' : Filter α<GOAL>f =o[l ⊔ l'] g ↔ f =o[l] g ∧ f =o[l'] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>C : ℝ<VAR>g : α → E<VAR>g' : α → F<VAR>h : ‖g x‖ ≤ C * ‖g' x‖<GOAL>Asymptotics.IsBigOWith C (𝓝[insert x s] x) g g' ↔ Asymptotics.IsBigOWith C (𝓝[s] x) g g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>C : ℝ<VAR>g : α → E<VAR>g' : α → F<VAR>h1 : Asymptotics.IsBigOWith C (𝓝[s] x) g g'<VAR>h2 : ‖g x‖ ≤ C * ‖g' x‖<GOAL>Asymptotics.IsBigOWith C (𝓝[insert x s] x) g g'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<GOAL>g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h1 : g =o[𝓝[s] x] g'<VAR>h2 : g x = 0<GOAL>g =o[𝓝[insert x s] x] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>c : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(Asymptotics.IsBigOWith c l f fun x => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>c : ℝ<VAR>f : α → E<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>(Asymptotics.IsBigOWith c l f fun x => |u x|) ↔ Asymptotics.IsBigOWith c l f u
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>(f =O[l] fun x => |u x|) ↔ f =O[l] u
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>(f =o[l] fun x => |u x|) ↔ f =o[l] u
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g ↔ Asymptotics.IsBigOWith c l f' g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>Norm F<VAR>c : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>Asymptotics.IsBigOWith c l (fun x => |u x|) g ↔ Asymptotics.IsBigOWith c l u g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>(fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>Norm F<VAR>g : α → F<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>(fun x => |u x|) =O[l] g ↔ u =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>(fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>Norm F<VAR>g : α → F<VAR>l : Filter α<VAR>u : α → ℝ<GOAL>(fun x => |u x|) =o[l] g ↔ u =o[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>c : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f' g'
<VAR>α : Type u_1<VAR>c : ℝ<VAR>l : Filter α<VAR>u v : α → ℝ<GOAL>(Asymptotics.IsBigOWith c l (fun x => |u x|) fun x => |v x|) ↔ Asymptotics.IsBigOWith c l u v
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) ↔ f' =O[l] g'
<VAR>α : Type u_1<VAR>l : Filter α<VAR>u v : α → ℝ<GOAL>((fun x => |u x|) =O[l] fun x => |v x|) ↔ u =O[l] v
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) ↔ f' =o[l] g'
<VAR>α : Type u_1<VAR>l : Filter α<VAR>u v : α → ℝ<GOAL>((fun x => |u x|) =o[l] fun x => |v x|) ↔ u =o[l] v
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>c : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(Asymptotics.IsBigOWith c l f fun x => -g' x) ↔ Asymptotics.IsBigOWith c l f g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(f =O[l] fun x => -g' x) ↔ f =O[l] g'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(f =o[l] fun x => -g' x) ↔ f =o[l] g'
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith c l (fun x => -f' x) g ↔ Asymptotics.IsBigOWith c l f' g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>(fun x => -f' x) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<GOAL>(fun x => -f' x) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith 1 l f' fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith 1 l g' fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>f' =O[l] fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>g' =O[l] fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f' : α → E' × F'<GOAL>(fun x => (f' x).1) =O[l] f'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f' : α → E' × F'<GOAL>(fun x => (f' x).2) =O[l] f'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith c l f fun x => (g' x, k' x)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f : α → E<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>h : f =O[l] g'<GOAL>f =O[l] fun x => (g' x, k' x)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f : α → E<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>h : f =o[l] g'<GOAL>f =o[l] fun x => (g' x, k' x)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>c : ℝ<VAR>f : α → E<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith c l f fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f =O[l] g'<GOAL>f =O[l] fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm E<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f =o[l] g'<GOAL>f =o[l] fun x => (f' x, g' x)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>hf : Asymptotics.IsBigOWith c l f' k'<VAR>hg : Asymptotics.IsBigOWith c l g' k'<GOAL>Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c c' : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>hf : Asymptotics.IsBigOWith c l f' k'<VAR>hg : Asymptotics.IsBigOWith c' l g' k'<GOAL>Asymptotics.IsBigOWith (max c c') l (fun x => (f' x, g' x)) k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k'<GOAL>Asymptotics.IsBigOWith c l f' k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k'<GOAL>Asymptotics.IsBigOWith c l g' k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>c : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k' ↔ Asymptotics.IsBigOWith c l f' k' ∧ Asymptotics.IsBigOWith c l g' k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>hf : f' =O[l] k'<VAR>hg : g' =O[l] k'<GOAL>(fun x => (f' x, g' x)) =O[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =O[l] k' → f' =O[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =O[l] k' → g' =O[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<VAR>hf : f' =o[l] k'<VAR>hg : g' =o[l] k'<GOAL>(fun x => (f' x, g' x)) =o[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =o[l] k' → f' =o[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =o[l] k' → g' =o[l] k'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedAddCommGroup G'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>l : Filter α<GOAL>(fun x => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k'
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>c : ℝ<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f'' g''<GOAL>∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l : Filter α<VAR>h : f'' =O[l] g''<GOAL>∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c₁ c₂ : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : Asymptotics.IsBigOWith c₁ l f₁ g<VAR>h₂ : Asymptotics.IsBigOWith c₂ l f₂ g<GOAL>Asymptotics.IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =O[l] g<VAR>h₂ : f₂ =O[l] g<GOAL>(fun x => f₁ x + f₂ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =o[l] g<VAR>h₂ : f₂ =o[l] g<GOAL>(fun x => f₁ x + f₂ x) =o[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : f₁ =o[l] g₁<VAR>h₂ : f₂ =o[l] g₂<GOAL>(fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =O[l] g<VAR>h₂ : f₂ =o[l] g<GOAL>(fun x => f₁ x + f₂ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =o[l] g<VAR>h₂ : f₂ =O[l] g<GOAL>(fun x => f₁ x + f₂ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c₁ c₂ : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : Asymptotics.IsBigOWith c₁ l f₁ g<VAR>h₂ : f₂ =o[l] g<VAR>hc : c₁ < c₂<GOAL>Asymptotics.IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c₁ c₂ : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =o[l] g<VAR>h₂ : Asymptotics.IsBigOWith c₁ l f₂ g<VAR>hc : c₁ < c₂<GOAL>Asymptotics.IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c₁ c₂ : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : Asymptotics.IsBigOWith c₁ l f₁ g<VAR>h₂ : Asymptotics.IsBigOWith c₂ l f₂ g<GOAL>Asymptotics.IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c₁ c₂ : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : Asymptotics.IsBigOWith c₁ l f₁ g<VAR>h₂ : f₂ =o[l] g<VAR>hc : c₁ < c₂<GOAL>Asymptotics.IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =O[l] g<VAR>h₂ : f₂ =O[l] g<GOAL>(fun x => f₁ x - f₂ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h₁ : f₁ =o[l] g<VAR>h₂ : f₂ =o[l] g<GOAL>(fun x => f₁ x - f₂ x) =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g<GOAL>Asymptotics.IsBigOWith c l (fun x => f₂ x - f₁ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<GOAL>Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g ↔ Asymptotics.IsBigOWith c l (fun x => f₂ x - f₁ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : (fun x => f₁ x - f₂ x) =O[l] g<GOAL>(fun x => f₂ x - f₁ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<GOAL>(fun x => f₁ x - f₂ x) =O[l] g ↔ (fun x => f₂ x - f₁ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : (fun x => f₁ x - f₂ x) =o[l] g<GOAL>(fun x => f₂ x - f₁ x) =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<GOAL>(fun x => f₁ x - f₂ x) =o[l] g ↔ (fun x => f₂ x - f₁ x) =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>c c' : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ f₃ : α → E'<VAR>h₁ : Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g<VAR>h₂ : Asymptotics.IsBigOWith c' l (fun x => f₂ x - f₃ x) g<GOAL>Asymptotics.IsBigOWith (c + c') l (fun x => f₁ x - f₃ x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ f₃ : α → E'<VAR>h₁ : (fun x => f₁ x - f₂ x) =O[l] g<VAR>h₂ : (fun x => f₂ x - f₃ x) =O[l] g<GOAL>(fun x => f₁ x - f₃ x) =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ f₃ : α → E'<VAR>h₁ : (fun x => f₁ x - f₂ x) =o[l] g<VAR>h₂ : (fun x => f₂ x - f₃ x) =o[l] g<GOAL>(fun x => f₁ x - f₃ x) =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : (fun x => f₁ x - f₂ x) =O[l] g<GOAL>f₁ =O[l] g ↔ f₂ =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : (fun x => f₁ x - f₂ x) =o[l] g<GOAL>f₁ =o[l] g ↔ f₂ =o[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(fun _x => 0) =o[l] g'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>c : ℝ<VAR>g' : α → F'<VAR>l : Filter α<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith c l (fun _x => 0) g'
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith 0 l (fun _x => 0) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<GOAL>(fun _x => 0) =O[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(fun x => f' x - f' x) =O[l] g'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<GOAL>(fun x => f' x - f' x) =o[l] g'
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup F'<VAR>NormedAddCommGroup E''<VAR>c : ℝ<VAR>f'' : α → E''<VAR>l : Filter α<GOAL>(Asymptotics.IsBigOWith c l f'' fun _x => 0) ↔ f'' =ᶠ[l] 0
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup F'<VAR>NormedAddCommGroup E''<VAR>f'' : α → E''<VAR>l : Filter α<GOAL>(f'' =O[l] fun _x => 0) ↔ f'' =ᶠ[l] 0
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup F'<VAR>NormedAddCommGroup E''<VAR>f'' : α → E''<VAR>l : Filter α<GOAL>(f'' =o[l] fun _x => 0) ↔ f'' =ᶠ[l] 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith (‖c‖ / ‖c'‖) l (fun _x => c) fun _x => c'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<GOAL>(fun _x => c) =O[l] fun _x => c'
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>c : E''<VAR>c' : F''<VAR>l : Filter α<VAR>l.NeBot<GOAL>((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>x : α<GOAL>f'' =O[pure x] g'' ↔ g'' x = 0 → f'' x = 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>s : Set α<GOAL>Asymptotics.IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>s : Set α<GOAL>f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup F'<VAR>NormedAddCommGroup E''<VAR>g' : α → F'<VAR>f'' : α → E''<VAR>s : Set α<GOAL>f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<GOAL>Asymptotics.IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<GOAL>f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup F'<VAR>NormedAddCommGroup E''<VAR>g' : α → F'<VAR>f'' : α → E''<GOAL>f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>One F<VAR>NormOneClass F<VAR>c : E<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith ‖c‖ l (fun _x => c) fun _x => 1