ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<GOAL>⇑(ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ) = ContinuousLinearMap.flip
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>v : E<VAR>f : E →SL[σ₁₂] F<GOAL>((ContinuousLinearMap.apply' F σ₁₂) v) f = f v
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>v : E<VAR>f : E →L[𝕜] Fₗ<GOAL>((ContinuousLinearMap.apply 𝕜 Fₗ) v) f = f v
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>RingHomIsometric σ₁₂<GOAL>‖ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>RingHomIsometric σ₁₂<VAR>f : F →SL[σ₂₃] G<VAR>g : E →SL[σ₁₂] F<GOAL>((ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃) f) g = f.comp g
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>RingHomIsometric σ₁₂<VAR>X : Type u_11<VAR>TopologicalSpace X<VAR>f : X → E →SL[σ₁₂] F<VAR>hf : Continuous f<VAR>g : F →SL[σ₂₃] G<GOAL>Continuous fun x => g.comp (f x)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>RingHomIsometric σ₁₂<VAR>X : Type u_11<VAR>TopologicalSpace X<VAR>g : X → F →SL[σ₂₃] G<VAR>hg : Continuous g<VAR>f : E →SL[σ₁₂] F<GOAL>Continuous fun x => (g x).comp f
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<GOAL>‖ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>f : Fₗ →L[𝕜] Gₗ<VAR>g : E →L[𝕜] Fₗ<GOAL>((ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ) f) g = f.comp g
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Eₗ<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Eₗ<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>∀ (a : E), (ContinuousLinearMap.precompR Eₗ L) a = (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) (L a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Eₗ<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Eₗ<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<VAR>u : Eₗ →L[𝕜] E<VAR>f : Fₗ<VAR>g : Eₗ<GOAL>(((ContinuousLinearMap.precompL Eₗ L) u) f) g = (L (u g)) f
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Eₗ<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Eₗ<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>‖ContinuousLinearMap.precompR Eₗ L‖ ≤ ‖L‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Eₗ<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Eₗ<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>L : E →L[𝕜] Fₗ →L[𝕜] Gₗ<GOAL>‖ContinuousLinearMap.precompL Eₗ L‖ ≤ ‖L‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>E' : Type u_11<VAR>F' : Type u_12<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>𝕜₁' : Type u_13<VAR>𝕜₂' : Type u_14<VAR>NontriviallyNormedField 𝕜₁'<VAR>NontriviallyNormedField 𝕜₂'<VAR>NormedSpace 𝕜₁' E'<VAR>NormedSpace 𝕜₂' F'<VAR>σ₁' : 𝕜₁' →+* 𝕜<VAR>σ₁₃' : 𝕜₁' →+* 𝕜₃<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>RingHomCompTriple σ₁' σ₁₃ σ₁₃'<VAR>RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃'<VAR>RingHomIsometric σ₂₃'<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>gE : E' →SL[σ₁'] E<VAR>gF : F' →SL[σ₂'] F<VAR>x : E'<VAR>y : F'<GOAL>((f.bilinearComp gE gF) x) y = (f (gE x)) (gF y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>f : E →L[𝕜] Fₗ →L[𝕜] Gₗ<VAR>p : E × Fₗ<GOAL>⇑(f.deriv₂ p) = fun q => (f p.1) q.2 + (f q.1) p.2
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>Gₗ : Type u_9<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup Fₗ<VAR>SeminormedAddCommGroup Gₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>NormedSpace 𝕜 Gₗ<VAR>f : E →L[𝕜] Fₗ →L[𝕜] Gₗ<VAR>x x' : E<VAR>y y' : Fₗ<GOAL>(f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f x') y'
<VAR>α : Type u_1<VAR>NormedAddCommGroup α<VAR>Lattice α<VAR>self : HasSolidNorm α<VAR>x y : α<GOAL>|x| ≤ |y| → ‖x‖ ≤ ‖y‖
<VAR>α : Type u_1<VAR>NormedAddCommGroup α<VAR>Lattice α<VAR>HasSolidNorm α<VAR>a b : α<VAR>h : |a| ≤ |b|<GOAL>‖a‖ ≤ ‖b‖
<VAR>α : Type u_1<VAR>NormedAddCommGroup α<VAR>Lattice α<VAR>HasSolidNorm α<VAR>r : ℝ<GOAL>LatticeOrderedAddCommGroup.IsSolid (Metric.ball 0 r)
<VAR>α : Type u_1<VAR>self : NormedLatticeAddCommGroup α<VAR>a b : α<GOAL>a ≤ b → ∀ (c : α), c + a ≤ c + b
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>‖a‖ ≤ ‖b‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>a : α<GOAL>‖|a|‖ = ‖a‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>x y : α<GOAL>‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>x y : α<GOAL>‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>a b : α<GOAL>‖|a| - |b|‖ ≤ ‖a - b‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>x y z : α<GOAL>‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>x y z : α<GOAL>‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<VAR>z : α<GOAL>LipschitzWith 1 fun x => x ⊔ z
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<GOAL>LipschitzWith 1 posPart
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<GOAL>LipschitzWith 1 negPart
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<GOAL>Continuous posPart
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<GOAL>Continuous negPart
<VAR>α : Type u_1<VAR>NormedLatticeAddCommGroup α<GOAL>IsClosed {x | 0 ≤ x}
<VAR>G : Type u_2<VAR>OrderedAddCommGroup G<VAR>TopologicalSpace G<VAR>ContinuousSub G<VAR>h : IsClosed {x | 0 ≤ x}<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>(u - v) =o[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>u =O[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>v =O[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>u =Θ[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>v =Θ[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u : α → β<VAR>l : Filter α<GOAL>u ~[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>h : u ~[l] v<GOAL>v ~[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>l : Filter α<VAR>u v w : α → β<VAR>huv : u ~[l] v<VAR>hvw : v ~[l] w<GOAL>u ~[l] w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>huw : u =ᶠ[l] w<GOAL>w ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>hvw : v =ᶠ[l] w<GOAL>u ~[l] w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u : α → β<VAR>l : Filter α<GOAL>u ~[l] 0 ↔ u =ᶠ[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u : α → β<VAR>l : Filter α<GOAL>u ~[l] 0 ↔ u =O[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u : α → β<VAR>l : Filter α<VAR>c : β<VAR>h : c ≠ 0<GOAL>u ~[l] Function.const α c ↔ Filter.Tendsto u l (nhds c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u : α → β<VAR>l : Filter α<VAR>c : β<VAR>hu : u ~[l] Function.const α c<GOAL>Filter.Tendsto u l (nhds c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>c : β<VAR>huv : u ~[l] v<VAR>hu : Filter.Tendsto u l (nhds c)<GOAL>Filter.Tendsto v l (nhds c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>c : β<VAR>huv : u ~[l] v<GOAL>Filter.Tendsto u l (nhds c) ↔ Filter.Tendsto v l (nhds c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>hwv : w =o[l] v<GOAL>u + w ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>hwv : w =o[l] v<GOAL>u - w ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>hu : u =o[l] w<VAR>hv : v ~[l] w<GOAL>u + v ~[l] w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>huv : (u - v) =o[l] v<GOAL>u ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>u v : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<GOAL>(fun x => -u x) ~[l] fun x => -v x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<GOAL>u ~[l] v ↔ ∃ φ, ∃ (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<GOAL>∃ φ, ∃ (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0<VAR>huv : Filter.Tendsto (u / v) l (nhds 1)<GOAL>u ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>hz : ∀ (x : α), v x = 0 → u x = 0<VAR>huv : Filter.Tendsto (u / v) l (nhds 1)<GOAL>u ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>hz : ∀ᶠ (x : α) in l, v x ≠ 0<GOAL>u ~[l] v ↔ Filter.Tendsto (u / v) l (nhds 1)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : α → 𝕜<VAR>u v : α → E<VAR>l : Filter α<VAR>hab : a ~[l] b<VAR>huv : u ~[l] v<GOAL>(fun x => a x • u x) ~[l] fun x => b x • v x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>htu : t ~[l] u<VAR>hvw : v ~[l] w<GOAL>t * v ~[l] u * w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<GOAL>(fun x => (u x)⁻¹) ~[l] fun x => (v x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>htu : t ~[l] u<VAR>hvw : v ~[l] w<GOAL>(fun x => t x / v x) ~[l] fun x => u x / w x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>OrderTopology β<VAR>huv : u ~[l] v<VAR>hu : Filter.Tendsto u l Filter.atTop<GOAL>Filter.Tendsto v l Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>OrderTopology β<VAR>huv : u ~[l] v<GOAL>Filter.Tendsto u l Filter.atTop ↔ Filter.Tendsto v l Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>OrderTopology β<VAR>huv : u ~[l] v<VAR>hu : Filter.Tendsto u l Filter.atBot<GOAL>Filter.Tendsto v l Filter.atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>OrderTopology β<VAR>huv : u ~[l] v<GOAL>Filter.Tendsto u l Filter.atBot ↔ Filter.Tendsto v l Filter.atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>l : Filter α<VAR>u v : α → β<VAR>h : u =ᶠ[l] v<GOAL>u ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>l : Filter α<VAR>f g₁ g₂ : α → β<VAR>h : f =ᶠ[l] g₁<VAR>h₂ : g₁ ~[l] g₂<GOAL>f ~[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>l : Filter α<VAR>f g₁ g₂ : α → β<VAR>h : f ~[l] g₁<VAR>h₂ : g₁ =ᶠ[l] g₂<GOAL>f ~[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f g₁ : α → β<VAR>g₂ : α → β₂<VAR>h : f ~[l] g₁<VAR>h₂ : g₁ =O[l] g₂<GOAL>f =O[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f : α → β₂<VAR>g₁ g₂ : α → β<VAR>h : f =O[l] g₁<VAR>h₂ : g₁ ~[l] g₂<GOAL>f =O[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f g₁ : α → β<VAR>g₂ : α → β₂<VAR>h : f ~[l] g₁<VAR>h₂ : g₁ =o[l] g₂<GOAL>f =o[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f : α → β₂<VAR>g₁ g₂ : α → β<VAR>h : f =o[l] g₁<VAR>h₂ : g₁ ~[l] g₂<GOAL>f =o[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f g₁ : α → β<VAR>g₂ : α → β₂<VAR>h : f ~[l] g₁<VAR>h₂ : g₁ =Θ[l] g₂<GOAL>f =Θ[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>NormedAddCommGroup β<VAR>Norm β₂<VAR>l : Filter α<VAR>f : α → β₂<VAR>g₁ g₂ : α → β<VAR>h : f =Θ[l] g₁<VAR>h₂ : g₁ ~[l] g₂<GOAL>f =Θ[l] g₂
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>h : SameRay ℝ x y<GOAL>‖x + y‖ = ‖x‖ + ‖y‖
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>h : SameRay ℝ x y<GOAL>‖x - y‖ = |‖x‖ - ‖y‖|
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y : E<VAR>h : SameRay ℝ x y<GOAL>‖x‖ • y = ‖y‖ • x
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x : F<VAR>hx : x ≠ 0<GOAL>Set.InjOn norm {y | SameRay ℝ x y}
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>y : F<VAR>hy : y ≠ 0<GOAL>Set.InjOn norm {x | SameRay ℝ x y}
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<GOAL>SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<VAR>h : ‖x‖ = ‖y‖<GOAL>SameRay ℝ x y ↔ x = y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<VAR>h : ‖x‖ = ‖y‖<GOAL>¬SameRay ℝ x y ↔ x ≠ y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<VAR>h : SameRay ℝ x y<VAR>hn : ‖x‖ = ‖y‖<GOAL>x = y
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x y : F<VAR>h : SameRay ℝ x y<GOAL>‖x‖ = ‖y‖ ↔ x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>x : E<VAR>c : 𝕜<GOAL>‖(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<VAR>c : 𝕜<GOAL>‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>⇑(ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h).symm = ⇑(ContinuousLinearEquiv.coord 𝕜 x h)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<VAR>c : 𝕜<GOAL>(ContinuousLinearEquiv.coord 𝕜 x h) ((ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) c) = c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<VAR>y : ↥(Submodule.span 𝕜 {x})<GOAL>(ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) ((ContinuousLinearEquiv.coord 𝕜 x h) y) = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>(ContinuousLinearEquiv.coord 𝕜 x h) ⟨x, ⋯⟩ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>x : E<VAR>hx : ‖x‖ = 1<VAR>r : 𝕜<GOAL>(LinearIsometryEquiv.toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>⇑UniformSpace.Completion.toComplₗᵢ = ↑E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>⇑UniformSpace.Completion.toComplL = ↑E
<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<GOAL>‖UniformSpace.Completion.toComplL‖ = 1
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<GOAL>(WithLp.equiv p V) 0 = 0
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<GOAL>(WithLp.equiv p V).symm 0 = 0
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x y : WithLp p V<GOAL>(WithLp.equiv p V) (x + y) = (WithLp.equiv p V) x + (WithLp.equiv p V) y
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x' y' : V<GOAL>(WithLp.equiv p V).symm (x' + y') = (WithLp.equiv p V).symm x' + (WithLp.equiv p V).symm y'
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x y : WithLp p V<GOAL>(WithLp.equiv p V) (x - y) = (WithLp.equiv p V) x - (WithLp.equiv p V) y
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x' y' : V<GOAL>(WithLp.equiv p V).symm (x' - y') = (WithLp.equiv p V).symm x' - (WithLp.equiv p V).symm y'
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x : WithLp p V<GOAL>(WithLp.equiv p V) (-x) = -(WithLp.equiv p V) x
<VAR>p : ℝ≥0∞<VAR>V : Type uV<VAR>AddCommGroup V<VAR>x' : V<GOAL>(WithLp.equiv p V).symm (-x') = -(WithLp.equiv p V).symm x'
<VAR>p : ℝ≥0∞<VAR>K : Type uK<VAR>V : Type uV<VAR>Semiring K<VAR>AddCommGroup V<VAR>Module K V<VAR>c : K<VAR>x : WithLp p V<GOAL>(WithLp.equiv p V) (c • x) = c • (WithLp.equiv p V) x
<VAR>p : ℝ≥0∞<VAR>K : Type uK<VAR>V : Type uV<VAR>Semiring K<VAR>AddCommGroup V<VAR>Module K V<VAR>c : K<VAR>x' : V<GOAL>(WithLp.equiv p V).symm (c • x') = c • (WithLp.equiv p V).symm x'
<VAR>p : ℝ≥0∞<VAR>K : Type uK<VAR>V : Type uV<VAR>Semiring K<VAR>AddCommGroup V<VAR>Module K V<GOAL>⇑(WithLp.linearEquiv p K V).symm = ⇑(WithLp.equiv p V).symm
<VAR>p : ℝ≥0∞<VAR>K : Type uK<VAR>V : Type uV<VAR>Semiring K<VAR>AddCommGroup V<VAR>Module K V<GOAL>⇑(WithLp.linearEquiv p K V) = ⇑(WithLp.equiv p V)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (Metric.thickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (Metric.thickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (Metric.thickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (Metric.thickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (Metric.cthickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (Metric.cthickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (Metric.cthickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (Metric.cthickening ε s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<GOAL>↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<GOAL>↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)
<VAR>α : Type u_1<VAR>NormedOrderedAddGroup α<VAR>s : Set α<GOAL>↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>NormedOrderedGroup α<VAR>s : Set α<GOAL>↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure s)
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<GOAL>y ∈ interior s
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<GOAL>y ∈ interior s
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>x y : ι → ℝ<GOAL>dist (x ⊓ y) (x ⊔ y) = dist x y
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>y : ι → ℝ<GOAL>MonotoneOn (fun x => dist x y) (Set.Ici y)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>x : ι → ℝ<GOAL>MonotoneOn (dist x) (Set.Ici x)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>y : ι → ℝ<GOAL>AntitoneOn (fun x => dist x y) (Set.Iic y)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>x : ι → ℝ<GOAL>AntitoneOn (dist x) (Set.Iic x)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>a₁ a₂ b₁ b₂ : ι → ℝ<VAR>ha : a₂ ≤ a₁<VAR>h₁ : a₁ ≤ b₁<VAR>hb : b₁ ≤ b₂<GOAL>dist a₁ b₁ ≤ dist a₂ b₂
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s