ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>s₁ s₂ : Set E<VAR>h : s₁ ⊆ s₂<VAR>hs₂ : Bornology.IsVonNBounded 𝕜 s₂<GOAL>Bornology.IsVonNBounded 𝕜 s₁
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>s t : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (s ∪ t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>s₁ s₂ : Set E<VAR>hs₁ : Bornology.IsVonNBounded 𝕜 s₁<VAR>hs₂ : Bornology.IsVonNBounded 𝕜 s₂<GOAL>Bornology.IsVonNBounded 𝕜 (s₁ ∪ s₂)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>BoundedSpace 𝕜<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>ι : Sort u_7<VAR>Finite ι<VAR>s : ι → Set E<GOAL>Bornology.IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>ι : Type u_7<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set E<GOAL>Bornology.IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, Bornology.IsVonNBounded 𝕜 (s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>SMul 𝕜 E<VAR>Zero E<VAR>TopologicalSpace E<VAR>S : Set (Set E)<VAR>hS : S.Finite<GOAL>Bornology.IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddZeroClass E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>DistribSMul 𝕜 E<VAR>s t : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜 s<VAR>ht : Bornology.IsVonNBounded 𝕜 t<GOAL>Bornology.IsVonNBounded 𝕜 (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>DistribMulAction 𝕜 E<VAR>s : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜 s<GOAL>Bornology.IsVonNBounded 𝕜 (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>DistribMulAction 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (-s) ↔ Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>DistribMulAction 𝕜 E<VAR>s t : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜 s<VAR>ht : Bornology.IsVonNBounded 𝕜 t<GOAL>Bornology.IsVonNBounded 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>t t' : TopologicalSpace E<VAR>h : t ≤ t'<VAR>s : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜 s<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_7<VAR>E : Type u_8<VAR>NormedDivisionRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>S : Set E<GOAL>Bornology.IsVonNBounded 𝕜 S ↔ Filter.Tendsto (fun x => x • S) (𝓝 0) (𝓝 0).smallSets
<VAR>𝕜 : Type u_7<VAR>ι : Type u_8<VAR>E : ι → Type u_9<VAR>NormedDivisionRing 𝕜<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>(i : ι) → TopologicalSpace (E i)<VAR>S : Set ((i : ι) → E i)<GOAL>Bornology.IsVonNBounded 𝕜 S ↔ ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (Function.eval i '' S)
<VAR>E : Type u_3<VAR>F : Type u_5<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>NormedDivisionRing 𝕜₁<VAR>NormedDivisionRing 𝕜₂<VAR>AddCommGroup E<VAR>Module 𝕜₁ E<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>RingHomSurjective σ<VAR>RingHomIsometric σ<VAR>s : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜₁ s<VAR>f : E →SL[σ] F<GOAL>Bornology.IsVonNBounded 𝕜₂ (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_6<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>S : Set E<VAR>ε : ι → 𝕜<VAR>x : ι → E<VAR>l : Filter ι<VAR>hS : Bornology.IsVonNBounded 𝕜 S<VAR>hxS : ∀ᶠ (n : ι) in l, x n ∈ S<VAR>hε : Filter.Tendsto ε l (𝓝 0)<GOAL>Filter.Tendsto (ε • x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>l.NeBot<VAR>hε : ∀ᶠ (n : ι) in l, ε n ≠ 0<VAR>S : Set E<VAR>H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (𝓝 0)<GOAL>Bornology.IsVonNBounded 𝕜 S
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>ι : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>l.NeBot<VAR>hε : Filter.Tendsto ε l (𝓝[≠] 0)<VAR>S : Set E<GOAL>Bornology.IsVonNBounded 𝕜 S ↔ ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>x : E<GOAL>Bornology.IsVonNBounded 𝕜 {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (insert x s) ↔ Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>hs : Bornology.IsVonNBounded 𝕜 s<VAR>x : E<GOAL>Bornology.IsVonNBounded 𝕜 (x +ᵥ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>x : E<GOAL>Bornology.IsVonNBounded 𝕜 (x +ᵥ s) ↔ Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<VAR>hst : Bornology.IsVonNBounded 𝕜 (s + t)<VAR>hs : s.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<VAR>hst : Bornology.IsVonNBounded 𝕜 (s + t)<VAR>ht : t.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 (s + t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (s + s) ↔ Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<VAR>hst : Bornology.IsVonNBounded 𝕜 (s - t)<VAR>ht : t.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>TopologicalAddGroup E<VAR>s t : Set E<VAR>hst : Bornology.IsVonNBounded 𝕜 (s - t)<VAR>hs : s.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>TopologicalAddGroup E<VAR>s t : Set E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>Bornology.IsVonNBounded 𝕜 (s - t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>TopologicalAddGroup E<VAR>s t : Set E<GOAL>Bornology.IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<GOAL>⋃₀ setOf (Bornology.IsVonNBounded 𝕜) = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : TotallyBounded s<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>f : ℕ → E<VAR>x : E<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 x)<GOAL>Bornology.IsVonNBounded 𝕜 (Set.range f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsBounded s<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<GOAL>Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<GOAL>Bornology.IsVonNBounded 𝕜 (Metric.closedBall 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>α : Type u_7<VAR>f : α → E<VAR>s : Set α<GOAL>Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ x ∈ s, ‖f x‖ ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1
<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<VAR>h₂ : g =O[l] f<GOAL>f =Θ[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 : f =Θ[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 α<VAR>h : f =Θ[l] g<GOAL>g =O[l] f
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>f : α → E<VAR>l : Filter α<GOAL>f =Θ[l] f
<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 =Θ[l] g<GOAL>g =Θ[l] f
<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 =Θ[l] g ↔ g =Θ[l] f
<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>h₁ : f =Θ[l] g<VAR>h₂ : g =Θ[l] k<GOAL>f =Θ[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>h₁ : f =O[l] g<VAR>h₂ : g =Θ[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>h₁ : f =Θ[l] g<VAR>h₂ : 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_8<VAR>Norm E<VAR>Norm F<VAR>SeminormedAddCommGroup G'<VAR>l : Filter α<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G'<VAR>h₁ : f =o[l] g<VAR>h₂ : g =Θ[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>h₁ : f =Θ[l] g<VAR>h₂ : g =o[l] k<GOAL>f =o[l] k
<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 =Θ[l] g₁<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>f =Θ[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₂ =Θ[l] g<GOAL>f₁ =Θ[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>Norm E<VAR>l : Filter α<VAR>f g : α → E<VAR>h : f =ᶠ[l] g<GOAL>f =Θ[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‖) =Θ[l] g ↔ f' =Θ[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 =Θ[l] fun x => ‖g' x‖) ↔ f =Θ[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 : (fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖<GOAL>f =Θ[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>f' : α → E'<VAR>l : Filter α<VAR>g : α → ℝ<VAR>h : (fun x => ‖f' x‖) =ᶠ[l] g<GOAL>f' =Θ[l] g
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm G<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f' =Θ[l] g'<GOAL>f' =o[l] k ↔ g' =o[l] k
<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 : g' =Θ[l] k'<GOAL>f =o[l] g' ↔ f =o[l] k'
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm G<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f' =Θ[l] g'<GOAL>f' =O[l] k ↔ g' =O[l] k
<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 : g' =Θ[l] k'<GOAL>f =O[l] g' ↔ f =O[l] k'
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm G<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f' =Θ[l] g'<GOAL>f' =Θ[l] k ↔ g' =Θ[l] k
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>Norm G<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>h : f' =Θ[l] g'<GOAL>k =Θ[l] f' ↔ k =Θ[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 =Θ[l] g<VAR>hl : l' ≤ l<GOAL>f =Θ[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 l' : Filter α<VAR>h : f' =Θ[l] g'<VAR>h' : f' =Θ[l'] g'<GOAL>f' =Θ[l ⊔ 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 l' : Filter α<GOAL>f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g'
<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'' =Θ[l] g''<GOAL>∀ᶠ (x : α) in l, f'' x = 0 ↔ g'' 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'' =Θ[l] g''<GOAL>Filter.Tendsto f'' l (𝓝 0) ↔ Filter.Tendsto g'' l (𝓝 0)
<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>h : f' =Θ[l] g'<GOAL>Filter.Tendsto (norm ∘ f') l Filter.atTop ↔ Filter.Tendsto (norm ∘ g') l Filter.atTop
<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>h : f' =Θ[l] g'<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f') ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g')
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜' F'<VAR>f₁ : α → 𝕜<VAR>f₂ : α → 𝕜'<VAR>g₁ : α → E'<VAR>g₂ : α → F'<VAR>hf : f₁ =Θ[l] f₂<VAR>hg : g₁ =Θ[l] g₂<GOAL>(fun x => f₁ x • g₁ x) =Θ[l] fun x => f₂ x • g₂ x
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f₁ f₂ : α → 𝕜<VAR>g₁ g₂ : α → 𝕜'<VAR>h₁ : f₁ =Θ[l] g₁<VAR>h₂ : f₂ =Θ[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =Θ[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : f =Θ[l] g<GOAL>(fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<GOAL>((fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹) ↔ f =Θ[l] g
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f₁ f₂ : α → 𝕜<VAR>g₁ g₂ : α → 𝕜'<VAR>h₁ : f₁ =Θ[l] g₁<VAR>h₂ : f₂ =Θ[l] g₂<GOAL>(fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : f =Θ[l] g<VAR>n : ℕ<GOAL>(fun x => f x ^ n) =Θ[l] fun x => g x ^ n
<VAR>α : Type u_1<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>NormedField 𝕜<VAR>NormedField 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : f =Θ[l] g<VAR>n : ℤ<GOAL>(fun x => f x ^ n) =Θ[l] fun x => g x ^ n
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>l : Filter α<VAR>c₁ : E''<VAR>c₂ : F''<VAR>h₁ : c₁ ≠ 0<VAR>h₂ : c₂ ≠ 0<GOAL>(fun x => c₁) =Θ[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>l : Filter α<VAR>l.NeBot<VAR>c₁ : E''<VAR>c₂ : F''<GOAL>((fun x => c₁) =Θ[l] fun x => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F'' : Type u_10<VAR>SeminormedAddCommGroup E'<VAR>NormedAddCommGroup F''<VAR>g'' : α → F''<VAR>l : Filter α<GOAL>(fun x => 0) =Θ[l] g'' ↔ g'' =ᶠ[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'' =Θ[l] fun x => 0) ↔ f'' =ᶠ[l] 0
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>𝕜 : Type u_14<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>NormedField 𝕜<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>NormedSpace 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c • f' x) =Θ[l] g ↔ f' =Θ[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F' : Type u_7<VAR>𝕜 : Type u_14<VAR>Norm E<VAR>SeminormedAddCommGroup F'<VAR>NormedField 𝕜<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<VAR>NormedSpace 𝕜 F'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =Θ[l] fun x => c • g' x) ↔ f =Θ[l] g'
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>𝕜 : Type u_14<VAR>Norm F<VAR>NormedField 𝕜<VAR>g : α → F<VAR>l : Filter α<VAR>c : 𝕜<VAR>f : α → 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c * f x) =Θ[l] g ↔ f =Θ[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_14<VAR>Norm E<VAR>NormedField 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>c : 𝕜<VAR>g : α → 𝕜<VAR>hc : c ≠ 0<GOAL>(f =Θ[l] fun x => c * g x) ↔ f =Θ[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : f₁ =o[l] f₂<GOAL>f₂ =Θ[l] (f₁ + f₂)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : f₁ =o[l] f₂<GOAL>f₂ =Θ[l] (f₂ + f₁)
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>g : α → F<VAR>hΘ : f₁ =Θ[l] g<VAR>ho : f₂ =o[l] g<GOAL>(f₁ + f₂) =Θ[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>g : α → F<VAR>ho : f₁ =o[l] g<VAR>hΘ : f₂ =Θ[l] g<GOAL>(f₁ + f₂) =Θ[l] g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>Norm E<VAR>a : 𝕜<VAR>f : 𝕜 → E<VAR>h : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[≠] a) (norm ∘ f)<GOAL>f =o[𝓝[≠] a] fun x => (x - a)⁻¹
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p q : ℕ<GOAL>(fun x => x ^ p / x ^ q) =ᶠ[Filter.atTop] fun x => x ^ (↑p - ↑q)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p q : ℕ<GOAL>(fun x => x ^ p / x ^ q) =ᶠ[Filter.atBot] fun x => x ^ (↑p - ↑q)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p q : ℕ<VAR>hpq : q < p<GOAL>Filter.Tendsto (fun x => x ^ p / x ^ q) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>Filter.Tendsto (fun x => x ^ p / x ^ q) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>(fun x => x ^ p) =o[Filter.atTop] fun x => x ^ q
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>α : Type u_2<VAR>u v : α → 𝕜<VAR>l : Filter α<VAR>huv : u =O[l] v<VAR>hu : Filter.Tendsto (fun x => ‖u x‖) l Filter.atTop<GOAL>Filter.Tendsto (fun x => ‖v x‖) l Filter.atTop
<VAR>α : Type u_1<VAR>NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[Filter.atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, g i) Filter.atTop Filter.atTop<GOAL>(fun n => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun n => ∑ i ∈ Finset.range n, g i
<VAR>α : Type u_1<VAR>NormedAddCommGroup α<VAR>f : ℕ → α<VAR>h : Filter.Tendsto f Filter.atTop (𝓝 0)<GOAL>(fun n => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun n => ↑n
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>u : ℕ → E<VAR>l : E<VAR>h : Filter.Tendsto u Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) Filter.atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>h : Filter.Tendsto u Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun n => (↑n)⁻¹ * ∑ i ∈ Finset.range n, u i) Filter.atTop (𝓝 l)
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>Filter.Tendsto (fun c => ∫ (v : V), cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) Filter.atTop (𝓝 (∫ (v : V), f v))
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>FiniteDimensional ℝ V<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>CompleteSpace E<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>h'f : MeasureTheory.Integrable (𝓕 f) MeasureTheory.volume<VAR>v : V<GOAL>Filter.Tendsto (fun c => ∫ (w : V), ((↑π * ↑c) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) Filter.atTop (𝓝 (𝓕⁻ (𝓕 f) v))