ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>‖PiTensorProduct.mapL f‖ ≤ ∏ i : ι, ‖f i‖
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>∀ (a : ⨂[𝕜] (i : ι), E i), ((PiTensorProduct.mapLMultilinear 𝕜 E E') f) a = (PiTensorProduct.liftAux ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) a
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<GOAL>‖PiTensorProduct.mapLMultilinear 𝕜 E E'‖ ≤ 1
<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_7<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>self : IsBoundedLinearMap 𝕜 f<GOAL>∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : IsLinearMap 𝕜 f<VAR>M : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖<GOAL>IsBoundedLinearMap 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<GOAL>IsBoundedLinearMap 𝕜 ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>IsBoundedLinearMap 𝕜 fun x => 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>IsBoundedLinearMap 𝕜 fun x => x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>IsBoundedLinearMap 𝕜 fun x => x.1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>IsBoundedLinearMap 𝕜 fun x => x.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>c : 𝕜<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 (c • f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 fun e => -f e
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<VAR>hg : IsBoundedLinearMap 𝕜 g<GOAL>IsBoundedLinearMap 𝕜 fun e => f e + g e
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<VAR>hg : IsBoundedLinearMap 𝕜 g<GOAL>IsBoundedLinearMap 𝕜 fun e => f e - g e
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : F → G<VAR>hg : IsBoundedLinearMap 𝕜 g<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>Filter.Tendsto f (𝓝 x) (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<GOAL>Filter.Tendsto f (𝓝 0) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>h : IsBoundedLinearMap 𝕜 f<VAR>l : Filter E<GOAL>f =O[l] fun x => x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>E : Type u_5<VAR>g : F → G<VAR>hg : IsBoundedLinearMap 𝕜 g<VAR>f : E → F<VAR>l : Filter E<GOAL>(fun x' => g (f x')) =O[l] f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>h : IsBoundedLinearMap 𝕜 f<VAR>l : Filter E<VAR>x : E<GOAL>(fun x' => f (x' - x)) =O[l] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>ι : Type u_5<VAR>Fintype ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>IsBoundedLinearMap 𝕜 fun p => p.1.prod p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>ι : Type u_5<VAR>Fintype ι<VAR>g : G →L[𝕜] E<GOAL>IsBoundedLinearMap 𝕜 fun f => f.compContinuousLinearMap fun x => g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>NontriviallyNormedField 𝕜'<VAR>NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜₂ G'<VAR>NormedSpace 𝕜' G'<VAR>SMulCommClass 𝕜₂ 𝕜' G'<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x x' : M<VAR>y : F<GOAL>(f (x + x')) y = (f x) y + (f x') y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>NontriviallyNormedField 𝕜'<VAR>NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜₂ G'<VAR>NormedSpace 𝕜' G'<VAR>SMulCommClass 𝕜₂ 𝕜' G'<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>y : F<GOAL>(f 0) y = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>NontriviallyNormedField 𝕜'<VAR>NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜₂ G'<VAR>NormedSpace 𝕜' G'<VAR>SMulCommClass 𝕜₂ 𝕜' G'<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>c : R<VAR>x : M<VAR>y : F<GOAL>(f (c • x)) y = ρ₁₂ c • (f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>NontriviallyNormedField 𝕜'<VAR>NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜₂ G'<VAR>NormedSpace 𝕜' G'<VAR>SMulCommClass 𝕜₂ 𝕜' G'<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x x' : M<VAR>y : F<GOAL>(f (x - x')) y = (f x) y - (f x') y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>NontriviallyNormedField 𝕜'<VAR>NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜₂ G'<VAR>NormedSpace 𝕜' G'<VAR>SMulCommClass 𝕜₂ 𝕜' G'<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x : M<VAR>y : F<GOAL>(f (-x)) y = -(f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>c : 𝕜<VAR>x : E<VAR>y : F<GOAL>(f (c • x)) y = c • (f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>self : IsBoundedBilinearMap 𝕜 f<VAR>x : E<VAR>y₁ y₂ : F<GOAL>f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>self : IsBoundedBilinearMap 𝕜 f<VAR>c : 𝕜<VAR>x : E<VAR>y : F<GOAL>f (c • x, y) = c • f (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>self : IsBoundedBilinearMap 𝕜 f<VAR>c : 𝕜<VAR>x : E<VAR>y : F<GOAL>f (x, c • y) = c • f (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>self : IsBoundedBilinearMap 𝕜 f<GOAL>∃ C > 0, ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>self : IsBoundedBilinearMap 𝕜 f<VAR>x₁ x₂ : E<VAR>y : F<GOAL>f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<GOAL>IsBoundedBilinearMap 𝕜 fun x => (f x.1) x.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<GOAL>f =O[⊤] fun p => ‖p.1‖ * ‖p.2‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>α : Type u_5<VAR>H : IsBoundedBilinearMap 𝕜 f<VAR>g : α → E<VAR>h : α → F<VAR>l : Filter α<GOAL>(fun x => f (g x, h x)) =O[l] fun x => ‖g x‖ * ‖h x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<GOAL>f =O[⊤] fun p => ‖p‖ * ‖p‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x y : E<VAR>z : F<GOAL>f (x - y, z) = f (x, z) - f (y, z)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E<VAR>y z : F<GOAL>f (x, y - z) = f (x, y) - f (x, z)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>e₂ : F<GOAL>Continuous fun e₁ => f (e₁, e₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>e₁ : E<GOAL>Continuous fun e₂ => f (e₁, e₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<GOAL>Continuous (Function.uncurry fun x y => (f x) y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>y : F<GOAL>IsBoundedLinearMap 𝕜 fun x => f (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E<GOAL>IsBoundedLinearMap 𝕜 fun y => f (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_5<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1.comp p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F →L[𝕜] G<GOAL>IsBoundedLinearMap 𝕜 fun f => g.comp f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F<GOAL>IsBoundedLinearMap 𝕜 fun g => g.comp f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1.smulRight p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>ι : Type u_5<VAR>E : ι → Type u_6<VAR>Fintype ι<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1.compContinuousMultilinearMap p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>p q : E × F<GOAL>(h.deriv p) q = f (p.1, q.2) + f (q.1, p.2)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_5<VAR>NormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<GOAL>IsBoundedBilinearMap 𝕜 fun p => ((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') p.1) p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<GOAL>IsBoundedLinearMap 𝕜 fun p => h.deriv p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>g : X → F →L[𝕜] G<VAR>f : X → E →L[𝕜] F<VAR>hg : Continuous g<VAR>hf : Continuous f<GOAL>Continuous fun x => (g x).comp (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>g : X → F →L[𝕜] G<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>hg : ContinuousOn g s<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => (g x).comp (f x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>f : X → E →L[𝕜] F<VAR>g : X → E<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => (f x) (g x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>f : X → E →L[𝕜] F<VAR>g : X → E<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => (f x) (g x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<GOAL>IsOpen (Set.range ContinuousLinearEquiv.toContinuousLinearMap)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace E<VAR>e : E ≃L[𝕜] F<GOAL>Set.range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 ↑e
<VAR>α : Type u_5<VAR>self : NonUnitalSeminormedRing α<VAR>a b : α<GOAL>‖a * b‖ ≤ ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : NonUnitalSeminormedRing α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : SeminormedRing α<VAR>a b : α<GOAL>‖a * b‖ ≤ ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : SeminormedRing α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : NonUnitalNormedRing α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : NonUnitalNormedRing α<VAR>a b : α<GOAL>‖a * b‖ ≤ ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : NormedRing α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : NormedRing α<VAR>a b : α<GOAL>‖a * b‖ ≤ ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : NormedDivisionRing α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_5<VAR>self : NormedDivisionRing α<VAR>a b : α<GOAL>‖a * b‖ = ‖a‖ * ‖b‖
<VAR>α : Type u_5<VAR>self : NonUnitalSeminormedCommRing α<VAR>x y : α<GOAL>x * y = y * x
<VAR>α : Type u_5<VAR>self : NonUnitalNormedCommRing α<VAR>x y : α<GOAL>x * y = y * x
<VAR>α : Type u_5<VAR>self : SeminormedCommRing α<VAR>x y : α<GOAL>x * y = y * x
<VAR>α : Type u_5<VAR>self : NormedCommRing α<VAR>x y : α<GOAL>x * y = y * x
<VAR>α : Type u_5<VAR>Norm α<VAR>One α<VAR>self : NormOneClass α<GOAL>‖1‖ = 1
<VAR>α : Type u_1<VAR>SeminormedAddCommGroup α<VAR>One α<VAR>NormOneClass α<GOAL>‖1‖₊ = 1
<VAR>α : Type u_5<VAR>SeminormedAddCommGroup α<VAR>One α<VAR>NormOneClass α<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>NonUnitalSeminormedRing α<VAR>a b : α<GOAL>‖a * b‖ ≤ ‖a‖ * ‖b‖
<VAR>α : Type u_1<VAR>NonUnitalSeminormedRing α<VAR>a b : α<GOAL>‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
<VAR>β : Type u_5<VAR>NormedRing β<VAR>Nontrivial β<GOAL>1 ≤ ‖1‖
<VAR>β : Type u_5<VAR>NormedRing β<VAR>Nontrivial β<GOAL>1 ≤ ‖1‖₊
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>NonUnitalSeminormedRing α<VAR>f g : ι → α<VAR>l : Filter ι<VAR>hf : Filter.Tendsto f l (𝓝 0)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l ((fun x => ‖x‖) ∘ g)<GOAL>Filter.Tendsto (fun x => f x * g x) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>NonUnitalSeminormedRing α<VAR>f g : ι → α<VAR>l : Filter ι<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>hg : Filter.Tendsto g l (𝓝 0)<GOAL>Filter.Tendsto (fun x => f x * g x) l (𝓝 0)
<VAR>α : Type u_1<VAR>NonUnitalSeminormedRing α<VAR>x y : α<GOAL>‖(AddMonoidHom.mulLeft x) y‖ ≤ ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>NonUnitalSeminormedRing α<VAR>x y : α<GOAL>‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>n : ℕ<GOAL>‖↑n‖ ≤ ↑n * ‖1‖
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>l : List α<GOAL>l ≠ [] → ‖l.prod‖ ≤ (List.map norm l).prod
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>l : List α<VAR>hl : l ≠ []<GOAL>‖l.prod‖₊ ≤ (List.map nnnorm l).prod
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>NormOneClass α<VAR>l : List α<GOAL>‖l.prod‖ ≤ (List.map norm l).prod
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>NormOneClass α<VAR>l : List α<GOAL>‖l.prod‖₊ ≤ (List.map nnnorm l).prod
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>NormedCommRing α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<GOAL>‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>NormedCommRing α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<GOAL>‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>NormedCommRing α<VAR>NormOneClass α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>NormedCommRing α<VAR>NormOneClass α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>a : α<VAR>n : ℕ<GOAL>0 < n → ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>NormOneClass α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>a : α<VAR>n : ℕ<VAR>h : 0 < n<GOAL>‖a ^ n‖ ≤ ‖a‖ ^ n
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>NormOneClass α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ n‖ ≤ ‖a‖ ^ n
<VAR>α : Type u_1<VAR>SeminormedRing α<VAR>a : α<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n
<VAR>α : Type u_1<VAR>NormedRing α<VAR>Nontrivial α<VAR>x : αˣ<GOAL>0 < ‖↑x‖