ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NormedAddCommGroup W₂<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>NormedSpace 𝕜 W₂<VAR>f : V →ᴬ[𝕜] W<VAR>g : W₂ →ᴬ[𝕜] V<GOAL>‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<GOAL>((ContinuousAffineMap.toConstProdContinuousLinearMap 𝕜 V W) f).1 = f 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<GOAL>((ContinuousAffineMap.toConstProdContinuousLinearMap 𝕜 V W) f).2 = f.contLinear
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Module ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>fr.extendTo𝕜' x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Module ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>RCLike.re (fr.extendTo𝕜' x) = fr x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Module ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>‖fr.extendTo𝕜' x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendTo𝕜' x) • x)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →L[ℝ] ℝ<VAR>x : F<GOAL>‖(↑fr).extendTo𝕜' x‖ ≤ ‖fr‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →L[ℝ] ℝ<VAR>x : F<GOAL>fr.extendTo𝕜' x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace ℝ F<VAR>IsScalarTower ℝ 𝕜 F<VAR>fr : F →L[ℝ] ℝ<GOAL>‖fr.extendTo𝕜'‖ = ‖fr‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>fr.extendTo𝕜 x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ<VAR>x : F<GOAL>fr.extendTo𝕜 x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_2<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ<GOAL>‖fr.extendTo𝕜‖ = ‖fr‖
<VAR>N : ℕ<VAR>NeZero N<VAR>Φ : ZMod N → ℂ<VAR>k : ZMod N<GOAL>𝓕 Φ k = ∑ j : ZMod N, ZMod.toCircle (-(j * k)) • Φ j
<VAR>N : ℕ<VAR>NeZero N<VAR>Φ : ZMod N → ℂ<GOAL>𝓕 Φ = fun k => ∑ j : ZMod N, ZMod.toCircle (-(j * k)) • Φ j
<VAR>N : ℕ<VAR>NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k : ZMod N<GOAL>𝓕 (⇑χ) k = gaussSum χ (ZMod.stdAddChar.mulShift (-k))
<VAR>N : ℕ<VAR>NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k : ZMod N<VAR>hχ : χ.IsPrimitive<GOAL>𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ ZMod.stdAddChar
<VAR>r : ℝ<GOAL>NormedSpace.exp ℝ ↑r = ↑(NormedSpace.exp ℝ r)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>((NormedSpace.expSeries ℝ ℍ (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>((NormedSpace.expSeries ℝ ℍ (2 * n + 1)) fun x => q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hc : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!) c<VAR>hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s<GOAL>HasSum (fun n => (NormedSpace.expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
<VAR>q : ℍ<VAR>hq : q.re = 0<GOAL>NormedSpace.exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
<VAR>q : ℍ<GOAL>NormedSpace.exp ℝ q = NormedSpace.exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
<VAR>q : ℍ<GOAL>(NormedSpace.exp ℝ q).re = NormedSpace.exp ℝ q.re * Real.cos ‖q - ↑q.re‖
<VAR>q : ℍ<GOAL>(NormedSpace.exp ℝ q).im = (NormedSpace.exp ℝ q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im
<VAR>q : ℍ<GOAL>Quaternion.normSq (NormedSpace.exp ℝ q) = NormedSpace.exp ℝ q.re ^ 2
<VAR>q : ℍ<GOAL>‖NormedSpace.exp ℝ q‖ = ‖NormedSpace.exp ℝ q.re‖
<VAR>R : Type u_1<VAR>𝕜₁ : Type u_2<VAR>𝕜₂ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>OrderedSemiring R<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>Module 𝕜₁ E<VAR>Module 𝕜₂ F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>Module R F<VAR>ContinuousConstSMul R F<VAR>LocallyConvexSpace R F<VAR>SMulCommClass 𝕜₂ R F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hD : D ∈ 𝓝 x<GOAL>oscillationWithin f D x = oscillation f x
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>x : E<GOAL>oscillationWithin f Set.univ x = oscillation f x
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hf : ContinuousWithinAt f D x<GOAL>oscillationWithin f D x = 0
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>x : E<VAR>hf : ContinuousAt f x<GOAL>oscillation f x = 0
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<GOAL>oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>TopologicalSpace E<VAR>f : E → F<VAR>x : E<GOAL>oscillation f x = 0 ↔ ContinuousAt f x
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>D : Set E<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f D x < ε<GOAL>∃ δ > 0, ∀ x ∈ K, EMetric.diam (f '' (EMetric.ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>PseudoEMetricSpace F<VAR>PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillation f x < ε<GOAL>∃ δ > 0, ∀ x ∈ K, EMetric.diam (f '' EMetric.ball x (ENNReal.ofReal δ)) ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>TopologicalSpace E<VAR>self : BarrelledSpace 𝕜 E<VAR>p : Seminorm 𝕜 E<GOAL>LowerSemicontinuous ⇑p → Continuous ⇑p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>SeminormedRing 𝕜<VAR>TopologicalSpace E<VAR>BarrelledSpace 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>hp : LowerSemicontinuous ⇑p<GOAL>Continuous ⇑p
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>BarrelledSpace 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>bdd : BddAbove (Set.range p)<GOAL>Continuous (⨆ i, ⇑(p i))
<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>𝕜₁ : Type u_4<VAR>𝕜₂ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>Nonempty κ<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜₁ E<VAR>Module 𝕜₂ F<VAR>UniformSpace E<VAR>UniformSpace F<VAR>UniformAddGroup E<VAR>UniformAddGroup F<VAR>ContinuousSMul 𝕜₁ E<VAR>BarrelledSpace 𝕜₁ E<VAR>𝓕 : ι → E →SL[σ₁₂] F<VAR>q : SeminormFamily 𝕜₂ F κ<VAR>hq : WithSeminorms q<VAR>H : ∀ (k : κ) (x : E), BddAbove (Set.range fun i => (q k) ((𝓕 i) x))<GOAL>UniformEquicontinuous (DFunLike.coe ∘ 𝓕)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>𝓕 : Type u_10<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>FunLike 𝓕 E F<VAR>SemilinearMapClass 𝓕 σ₁₂ E F<VAR>f : 𝓕<VAR>hf : Continuous ⇑f<VAR>x : E<VAR>hx : ‖x‖ = 0<GOAL>‖f x‖ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>𝓕 : Type u_10<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>FunLike 𝓕 E F<VAR>RingHomIsometric σ₁₂<VAR>SemilinearMapClass 𝓕 σ₁₂ E F<VAR>f : 𝓕<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>‖f x‖ ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>𝓕 : Type u_10<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>FunLike 𝓕 E F<VAR>RingHomIsometric σ₁₂<VAR>SemilinearMapClass 𝓕 σ₁₂ E F<VAR>f : 𝓕<VAR>hf : Continuous ⇑f<GOAL>∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
<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>f : E →SL[σ₁₂] F<GOAL>∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>a : 𝕜<GOAL>(LinearIsometry.toSpanSingleton 𝕜 E hv) a = a • v
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>hv : ‖v‖ = 1<GOAL>(LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v
<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>f : E →SL[σ₁₂] F<GOAL>‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
<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>f : E →SL[σ₁₂] F<GOAL>∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
<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>f : E →SL[σ₁₂] F<GOAL>BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}
<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>f : E →SL[σ₁₂] F<GOAL>IsLeast {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖
<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>f : E →SL[σ₁₂] F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖<GOAL>‖f‖ ≤ M
<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>f : E →SL[σ₁₂] F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖<GOAL>‖f‖ ≤ M
<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>f : E →SL[σ₁₂] F<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K ⇑f<GOAL>‖f‖ ≤ ↑K
<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>φ : E →SL[σ₁₂] F<VAR>M : ℝ<VAR>M_nonneg : 0 ≤ M<VAR>h_above : ∀ (x : E), ‖φ x‖ ≤ M * ‖x‖<VAR>h_below : ∀ N ≥ 0, (∀ (x : E), ‖φ x‖ ≤ N * ‖x‖) → M ≤ N<GOAL>‖φ‖ = M
<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>f : E →SL[σ₁₂] F<GOAL>‖-f‖ = ‖f‖
<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>f : E →SL[σ₁₂] F<GOAL>0 ≤ ‖f‖
<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>σ₁₂ : 𝕜 →+* 𝕜₂<GOAL>‖0‖ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1
<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>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<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>f : E →SL[σ₁₂] F<VAR>x y : E<GOAL>dist (f x) (f y) ≤ ‖f‖ * dist x y
<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>f : E →SL[σ₁₂] F<VAR>x : E<VAR>a b : ℝ<VAR>hf : ‖f‖ ≤ a<VAR>hx : ‖x‖ ≤ b<GOAL>‖f x‖ ≤ a * b
<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>f : E →SL[σ₁₂] F<VAR>c : ℝ<VAR>x : E<VAR>h : ‖x‖ ≤ c<GOAL>‖f x‖ ≤ ‖f‖ * c
<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>f : E →SL[σ₁₂] F<VAR>c : ℝ<VAR>h : ‖f‖ ≤ c<VAR>x : E<GOAL>‖f x‖ ≤ c * ‖x‖
<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>f : E →SL[σ₁₂] F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<GOAL>‖f‖ ≤ M ↔ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
<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>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖f x‖ / ‖x‖ ≤ ‖f‖
<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>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖
<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>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖<GOAL>‖f‖ ≤ C
<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>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>hf : ∀ x ∈ Metric.ball 0 ε, ‖f x‖ ≤ C * ‖x‖<GOAL>‖f‖ ≤ C
<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>f : E →SL[σ₁₂] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ᶠ (x : E) in 𝓝 0, ‖f x‖ ≤ C * ‖x‖<GOAL>‖f‖ ≤ C
<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>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>c : 𝕜<VAR>hc : ‖c‖ < 1<VAR>hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖<GOAL>‖f‖ ≤ C
<VAR>E : Type u_4<VAR>F : Type u_6<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<GOAL>‖f‖ ≤ C
<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>f g : E →SL[σ₁₂] F<GOAL>‖f + g‖ ≤ ‖f‖ + ‖g‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>h : ∃ x, ‖x‖ ≠ 0<GOAL>‖ContinuousLinearMap.id 𝕜 E‖ = 1
<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>𝕜' : Type u_11<VAR>NormedField 𝕜'<VAR>NormedSpace 𝕜' F<VAR>SMulCommClass 𝕜₂ 𝕜' F<VAR>c : 𝕜'<VAR>f : E →SL[σ₁₂] F<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<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 σ₁₂<GOAL>𝓤 (E →SL[σ₁₂] F) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖f.1 - f.2‖ < r}
<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>h : F →SL[σ₂₃] G<VAR>f : E →SL[σ₁₂] F<GOAL>‖h.comp f‖ ≤ ‖h‖ * ‖f‖
<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>f : E →SL[σ₁₂] F<VAR>Subsingleton E<GOAL>‖f‖ = 0
<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>𝕜' : Type u_11<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜' 𝕜 E<VAR>NormedSpace 𝕜' Fₗ<VAR>IsScalarTower 𝕜' 𝕜 Fₗ<VAR>f : E →L[𝕜] Fₗ<GOAL>‖ContinuousLinearMap.restrictScalars 𝕜' f‖ = ‖f‖
<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>𝕜' : Type u_11<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜' 𝕜 E<VAR>NormedSpace 𝕜' Fₗ<VAR>IsScalarTower 𝕜' 𝕜 Fₗ<VAR>𝕜'' : Type u_12<VAR>Ring 𝕜''<VAR>Module 𝕜'' Fₗ<VAR>ContinuousConstSMul 𝕜'' Fₗ<VAR>SMulCommClass 𝕜 𝕜'' Fₗ<VAR>SMulCommClass 𝕜' 𝕜'' Fₗ<GOAL>⇑(ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'
<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>𝕜' : Type u_11<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜' 𝕜 E<VAR>NormedSpace 𝕜' Fₗ<VAR>IsScalarTower 𝕜' 𝕜 Fₗ<VAR>𝕜'' : Type u_12<VAR>Ring 𝕜''<VAR>Module 𝕜'' Fₗ<VAR>ContinuousConstSMul 𝕜'' Fₗ<VAR>SMulCommClass 𝕜 𝕜'' Fₗ<VAR>SMulCommClass 𝕜' 𝕜'' Fₗ<GOAL>(ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toLinearMap = ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''
<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>𝕜' : Type u_11<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜' 𝕜 E<VAR>NormedSpace 𝕜' Fₗ<VAR>IsScalarTower 𝕜' 𝕜 Fₗ<VAR>𝕜'' : Type u_12<VAR>Ring 𝕜''<VAR>Module 𝕜'' Fₗ<VAR>ContinuousConstSMul 𝕜'' Fₗ<VAR>SMulCommClass 𝕜 𝕜'' Fₗ<VAR>SMulCommClass 𝕜' 𝕜'' Fₗ<GOAL>↑(ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''
<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>𝕜' : Type u_11<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜' 𝕜<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜' 𝕜 E<VAR>NormedSpace 𝕜' Fₗ<VAR>IsScalarTower 𝕜' 𝕜 Fₗ<VAR>𝕜'' : Type u_12<VAR>Ring 𝕜''<VAR>Module 𝕜'' Fₗ<VAR>ContinuousConstSMul 𝕜'' Fₗ<VAR>SMulCommClass 𝕜 𝕜'' Fₗ<VAR>SMulCommClass 𝕜' 𝕜'' Fₗ<GOAL>⇑(ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>SeminormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_11<VAR>Fintype ι<VAR>M : ι → Type u_12<VAR>(i : ι) → SeminormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>C : ℝ<VAR>L : (i : ι) → E →L[𝕜] M i<VAR>hL : ∀ (i : ι), ‖L i‖ ≤ C<VAR>hC : 0 ≤ C<GOAL>‖ContinuousLinearMap.pi L‖ ≤ C
<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>f : E →ₛₗ[σ₁₂] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>‖f.mkContinuous C h‖ ≤ C
<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>f : E →ₛₗ[σ₁₂] F<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>‖f.mkContinuous C h‖ ≤ max C 0