ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>NormedRing α<VAR>Nontrivial α<VAR>x : αˣ<GOAL>0 < ‖↑x‖₊
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a b : α<GOAL>‖a * b‖ = ‖a‖ * ‖b‖
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a b : α<GOAL>‖a * b‖₊ = ‖a‖₊ * ‖b‖₊
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>∀ (x : α), normHom x = ‖x‖
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>∀ (x : α), nnnormHom x = ‖x‖₊
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ n‖ = ‖a‖ ^ n
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ n‖₊ = ‖a‖₊ ^ n
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>l : List α<GOAL>‖l.prod‖ = (List.map norm l).prod
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>l : List α<GOAL>‖l.prod‖₊ = (List.map nnnorm l).prod
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a b : α<GOAL>‖a / b‖ = ‖a‖ / ‖b‖
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a b : α<GOAL>‖a / b‖₊ = ‖a‖₊ / ‖b‖₊
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<GOAL>‖a⁻¹‖ = ‖a‖⁻¹
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<GOAL>‖a⁻¹‖₊ = ‖a‖₊⁻¹
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>n : ℤ<GOAL>‖a ^ n‖ = ‖a‖ ^ n
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>n : ℤ<GOAL>‖a ^ n‖₊ = ‖a‖₊ ^ n
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>z w : α<VAR>hz : z ≠ 0<VAR>hw : w ≠ 0<GOAL>dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>z w : α<VAR>hz : z ≠ 0<VAR>hw : w ≠ 0<GOAL>nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>AntilipschitzWith ‖a‖₊⁻¹ fun x => a * x
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>AntilipschitzWith ‖a‖₊⁻¹ fun x => x * a
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(DilationEquiv.mulLeft a ha) x = a * x
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(DilationEquiv.mulLeft a ha).symm x = a⁻¹ * x
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(DilationEquiv.mulRight a ha) x = x * a
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<VAR>x : α<GOAL>(DilationEquiv.mulRight a ha).symm x = x * a⁻¹
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.comap (fun x => a * x) (Bornology.cobounded α) = Bornology.cobounded α
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.map (fun x => a * x) (Bornology.cobounded α) = Bornology.cobounded α
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.comap (fun x => x * a) (Bornology.cobounded α) = Bornology.cobounded α
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.map (fun x => x * a) (Bornology.cobounded α) = Bornology.cobounded α
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => a * x) (Bornology.cobounded α) (Bornology.cobounded α)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Filter.Tendsto (fun x => x * a) (Bornology.cobounded α) (Bornology.cobounded α)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>(Bornology.cobounded α)⁻¹ = 𝓝[≠] 0
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>(𝓝[≠] 0)⁻¹ = Bornology.cobounded α
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>Filter.Tendsto Inv.inv (Bornology.cobounded α) (𝓝[≠] 0)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>Filter.Tendsto Inv.inv (Bornology.cobounded α) (𝓝 0)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<GOAL>Filter.Tendsto Inv.inv (𝓝[≠] 0) (Bornology.cobounded α)
<VAR>α : Type u_1<VAR>NormedDivisionRing α<VAR>a : α<VAR>ha : IsOfFinOrder a<GOAL>‖a‖ = 1
<VAR>α : Type u_5<VAR>self : NormedField α<VAR>a b : α<GOAL>‖a * b‖ = ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : NormedField α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : NontriviallyNormedField α<GOAL>∃ x, 1 < ‖x‖
<VAR>α : Type u_5<VAR>self : DenselyNormedField α<VAR>x y : ℝ<GOAL>0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField α<VAR>s : Finset β<VAR>f : β → α<GOAL>‖∏ b ∈ s, f b‖ = ∏ b ∈ s, ‖f b‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField α<VAR>s : Finset β<VAR>f : β → α<GOAL>‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<GOAL>∃ x, 1 < ‖x‖
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<VAR>r : ℝ<GOAL>∃ x, r < ‖x‖
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>∃ x, 0 < ‖x‖ ∧ ‖x‖ < r
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<GOAL>∃ x, 0 < ‖x‖ ∧ ‖x‖ < 1
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<VAR>x : α<GOAL>(𝓝[≠] x).NeBot
<VAR>α : Type u_1<VAR>NontriviallyNormedField α<GOAL>(𝓝[{x | IsUnit x}] 0).NeBot
<VAR>α : Type u_1<VAR>DenselyNormedField α<VAR>r₁ r₂ : ℝ<VAR>h₀ : 0 ≤ r₁<VAR>h : r₁ < r₂<GOAL>∃ x, r₁ < ‖x‖ ∧ ‖x‖ < r₂
<VAR>α : Type u_1<VAR>DenselyNormedField α<VAR>r₁ r₂ : ℝ≥0<VAR>h : r₁ < r₂<GOAL>∃ x, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂
<VAR>α : Type u_1<VAR>DenselyNormedField α<GOAL>DenseRange nnnorm
<VAR>x : ℝ<VAR>y : ℝ<VAR>hx : 0 ≤ x<GOAL>x.toNNReal * ‖y‖₊ = ‖x * y‖₊
<VAR>x : ℝ<VAR>y : ℝ<VAR>hy : 0 ≤ y<GOAL>‖x‖₊ * y.toNNReal = ‖x * y‖₊
<VAR>x : ℝ≥0<GOAL>‖↑x‖ = ↑x
<VAR>x : ℝ≥0<GOAL>‖↑x‖₊ = x
<GOAL>LipschitzWith 2 fun p => p.1 - p.2
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>x : α<GOAL>‖‖x‖‖ = ‖x‖
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>a : α<GOAL>‖‖a‖‖₊ = ‖a‖₊
<VAR>α : Type u_1<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>b : β<GOAL>Filter.Tendsto f Filter.atTop (𝓝 b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε
<VAR>α : Type u_1<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>b : β<GOAL>Filter.Tendsto f Filter.atTop (𝓝 b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Norm R₁<VAR>Norm R₂<VAR>σ : R₁ →+* R₂<VAR>self : RingHomIsometric σ<VAR>x : R₁<GOAL>‖σ x‖ = ‖x‖
<VAR>F : Type u_8<VAR>R : Type u_9<VAR>S : Type u_10<VAR>Ring R<VAR>SeminormedRing S<VAR>NormOneClass S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<GOAL>NormOneClass R
<VAR>α : Type u_17<VAR>E : Type u_18<VAR>F : Type u_19<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<GOAL>Asymptotics.IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖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 : Filter α<GOAL>Asymptotics.IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_17<VAR>E : Type u_18<VAR>F : Type u_19<VAR>Norm E<VAR>Norm F<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<GOAL>f =O[l] g = ∃ c, Asymptotics.IsBigOWith c l f 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 : Filter α<GOAL>f =O[l] g ↔ ∃ c, Asymptotics.IsBigOWith c l f 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 : Filter α<GOAL>f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E''' : Type u_12<VAR>Norm E<VAR>SeminormedAddGroup E'''<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → E'''<GOAL>f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E''' : Type u_12<VAR>Norm E<VAR>SeminormedAddGroup E'''<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → E'''<GOAL>f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖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>l : Filter α<VAR>c : ℝ<VAR>h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖<GOAL>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 : Filter α<VAR>h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖<GOAL>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 : Filter α<GOAL>f =O[l] g → ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_17<VAR>E : Type u_18<VAR>F : Type u_19<VAR>Norm E<VAR>Norm F<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<GOAL>f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f 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 : Filter α<GOAL>f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f 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 : Filter α<GOAL>f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖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 : Filter α<VAR>h : f =o[l] g<VAR>hc : 0 < c<GOAL>∀ᶠ (x : α) in l, ‖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 : Filter α<VAR>h : f =o[l] g<VAR>hc : 0 < c<GOAL>Asymptotics.IsBigOWith c l f 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 : Filter α<VAR>h : f =o[l] g<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖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 : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g<GOAL>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 : Filter α<VAR>hgf : f =o[l] g<GOAL>Asymptotics.IsBigOWith 1 l f 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 : Filter α<VAR>hgf : f =o[l] g<GOAL>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 : Filter α<GOAL>f =O[l] g → ∃ c, 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>c c' : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<VAR>hc : c ≤ c'<GOAL>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>c : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<GOAL>∃ c' > 0, 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 α<VAR>h : f =O[l] g'<GOAL>∃ c > 0, 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>c : ℝ<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c l f g'<GOAL>∃ c' ≥ 0, 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 α<VAR>h : f =O[l] g'<GOAL>∃ c ≥ 0, 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] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, 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] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖
<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 α<VAR>ι : Sort u_17<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : f =O[l] g'<VAR>hb : l.HasBasis p s<GOAL>∃ c > 0, ∃ i, p i ∧ ∀ x ∈ s i, ‖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 : Filter α<VAR>hc : 0 < c<GOAL>Asymptotics.IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖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>l : Filter α<VAR>h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖<GOAL>f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
<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] g' ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f 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>f' : α → E'<VAR>l : Filter α<GOAL>f' =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖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 α<VAR>Subsingleton E'<GOAL>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 α<VAR>Subsingleton E'<GOAL>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>c₁ c₂ : ℝ<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hc : c₁ = c₂<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>Asymptotics.IsBigOWith c₁ l f₁ g₁ ↔ Asymptotics.IsBigOWith c₂ l f₂ g₂
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c₁ c₂ : ℝ<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : Asymptotics.IsBigOWith c₁ l f₁ g₁<VAR>hc : c₁ = c₂<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>Asymptotics.IsBigOWith c₂ l f₂ g₂
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c₁ c₂ : ℝ<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : Asymptotics.IsBigOWith c₁ l f₁ g₁<VAR>hc : c₁ = c₂<VAR>hf : ∀ (x : α), f₁ x = f₂ x<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>Asymptotics.IsBigOWith c₂ l f₂ g₂
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>h : Asymptotics.IsBigOWith c l f₁ g<VAR>hf : ∀ (x : α), f₁ x = f₂ x<GOAL>Asymptotics.IsBigOWith c l f₂ 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>l : Filter α<VAR>g₁ g₂ : α → F<VAR>h : Asymptotics.IsBigOWith c l f g₁<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>Asymptotics.IsBigOWith c l f g₂
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>h : Asymptotics.IsBigOWith c₁ l f g<VAR>hc : c₁ = c₂<GOAL>Asymptotics.IsBigOWith c₂ l f g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : f₁ =O[l] g₁<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : f₁ =O[l] g₁<VAR>hf : ∀ (x : α), f₁ x = f₂ x<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>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>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>h : f₁ =O[l] g<VAR>hf : ∀ (x : α), f₁ x = f₂ x<GOAL>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>l : Filter α<VAR>g₁ g₂ : α → F<VAR>h : f =O[l] g₁<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : f₁ =o[l] g₁<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>h : f₁ =o[l] g₁<VAR>hf : ∀ (x : α), f₁ x = f₂ x<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>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>g : α → F<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>h : f₁ =o[l] g<VAR>hf : ∀ (x : α), f₁ x = f₂ x<GOAL>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>l : Filter α<VAR>g₁ g₂ : α → F<VAR>h : f =o[l] g₁<VAR>hg : ∀ (x : α), g₁ x = g₂ x<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>h : f₂ =O[l] g<GOAL>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>l : Filter α<VAR>f₁ f₂ : α → E<VAR>g : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>h : f₂ =o[l] g<GOAL>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>l : Filter α<VAR>f : α → E<VAR>g₁ g₂ : α → F<VAR>h : f =O[l] g₁<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>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>l : Filter α<VAR>f : α → E<VAR>g₁ g₂ : α → F<VAR>h : f =o[l] g₁<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>f =o[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<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 : Filter α<VAR>hcfg : Asymptotics.IsBigOWith c l f g<VAR>k : β → α<VAR>l' : Filter β<VAR>hk : Filter.Tendsto k l' l<GOAL>Asymptotics.IsBigOWith c l' (f ∘ k) (g ∘ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hfg : f =O[l] g<VAR>k : β → α<VAR>l' : Filter β<VAR>hk : Filter.Tendsto k l' l<GOAL>(f ∘ k) =O[l'] (g ∘ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hfg : f =o[l] g<VAR>k : β → α<VAR>l' : Filter β<VAR>hk : Filter.Tendsto k l' l<GOAL>(f ∘ k) =o[l'] (g ∘ k)
<VAR>α : Type u_1<VAR>β : Type u_2<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>k : β → α<VAR>l : Filter β<GOAL>Asymptotics.IsBigOWith c (Filter.map k l) f g ↔ Asymptotics.IsBigOWith c l (f ∘ k) (g ∘ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>k : β → α<VAR>l : Filter β<GOAL>f =O[Filter.map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>g : α → F<VAR>k : β → α<VAR>l : Filter β<GOAL>f =o[Filter.map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)
<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>hl : l ≤ l'<GOAL>Asymptotics.IsBigOWith c l f 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>hl : l ≤ l'<GOAL>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 α<VAR>h : f =o[l'] g<VAR>hl : l ≤ l'<GOAL>f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>c c' : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>l : Filter α<VAR>hfg : Asymptotics.IsBigOWith c l f g<VAR>hgk : Asymptotics.IsBigOWith c' l g k<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith (c * c') l f k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>G : Type u_5<VAR>F' : Type u_7<VAR>Norm E<VAR>Norm G<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F'<VAR>k : α → G<VAR>hfg : f =O[l] g<VAR>hgk : g =O[l] k<GOAL>f =O[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>l : Filter α<VAR>hfg : f =o[l] g<VAR>hgk : Asymptotics.IsBigOWith c l g k<VAR>hc : 0 < c<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G' : Type u_8<VAR>Norm E<VAR>Norm F<VAR>SeminormedAddCommGroup G'<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G'<VAR>hfg : f =o[l] g<VAR>hgk : g =O[l] k<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>l : Filter α<VAR>hfg : Asymptotics.IsBigOWith c l f g<VAR>hgk : g =o[l] k<VAR>hc : 0 < c<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>G : Type u_5<VAR>F' : Type u_7<VAR>Norm E<VAR>Norm G<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F'<VAR>k : α → G<VAR>hfg : f =O[l] g<VAR>hgk : g =o[l] k<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>hfg : f =o[l] g<VAR>hgk : g =o[l] k<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>G : Type u_5<VAR>F' : Type u_7<VAR>Norm E<VAR>Norm G<VAR>SeminormedAddCommGroup F'<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F'<VAR>k : α → G<VAR>hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖<VAR>hgk : g =O[l] k<GOAL>f =O[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>g : α → ℝ<VAR>l : Filter α<VAR>hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ g x<GOAL>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>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>l : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖<GOAL>Asymptotics.IsBigOWith c l f 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 : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖<GOAL>Asymptotics.IsBigOWith 1 l f 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>l : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖<GOAL>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 : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith 1 l f f
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>l : Filter α<GOAL>f =O[l] f
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>l : Filter α<VAR>f₁ f₂ : α → E<VAR>hf : f₁ =ᶠ[l] f₂<GOAL>f₁ =O[l] f₂
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>c : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>l : Filter α<VAR>hfg : Asymptotics.IsBigOWith c l f g<VAR>hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith c l f k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>G : Type u_5<VAR>F' : Type u_7<VAR>Norm E<VAR>Norm G<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>k : α → G<VAR>g' : α → F'<VAR>l : Filter α<VAR>hfg : f =O[l] g'<VAR>hgk : ∀ (x : α), ‖g' x‖ ≤ ‖k x‖<GOAL>f =O[l] k
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>Norm E<VAR>Norm F<VAR>Norm G<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>l : Filter α<VAR>hfg : f =o[l] g<VAR>hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>f' : α → E'<VAR>l : Filter α<VAR>h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0<GOAL>¬f' =o[l] f'
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>NormedAddCommGroup E''<VAR>f'' : α → E''<VAR>l : Filter α<VAR>h : ∃ᶠ (x : α) in l, f'' x ≠ 0<GOAL>¬f'' =o[l] f''
<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>l : Filter α<VAR>h : f'' =O[l] g'<VAR>hf : ∃ᶠ (x : α) in l, f'' x ≠ 0<GOAL>¬g' =o[l] f''
<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>l : Filter α<VAR>h : f'' =o[l] g'<VAR>hf : ∃ᶠ (x : α) in l, f'' x ≠ 0<GOAL>¬g' =O[l] f''
<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