ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>v : V<VAR>h'f : ContinuousAt f 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))
<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<VAR>hv : ContinuousAt f v<GOAL>𝓕⁻ (𝓕 f) 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>h : Continuous f<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>h'f : MeasureTheory.Integrable (𝓕 f) MeasureTheory.volume<GOAL>𝓕⁻ (𝓕 f) = f
<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<VAR>hv : ContinuousAt f v<GOAL>𝓕 (𝓕⁻ f) 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>h : Continuous f<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<VAR>h'f : MeasureTheory.Integrable (𝓕 f) MeasureTheory.volume<GOAL>𝓕 (𝓕⁻ f) = f
<VAR>α : Type u_2<VAR>self : NormedOrderedAddGroup α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_2<VAR>self : NormedOrderedGroup α<VAR>x y : α<GOAL>dist x y = ‖x / y‖
<VAR>α : Type u_2<VAR>self : NormedLinearOrderedAddGroup α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_2<VAR>self : NormedLinearOrderedGroup α<VAR>x y : α<GOAL>dist x y = ‖x / y‖
<VAR>α : Type u_2<VAR>self : NormedLinearOrderedField α<VAR>x y : α<GOAL>‖x * y‖ = ‖x‖ * ‖y‖
<VAR>α : Type u_2<VAR>self : NormedLinearOrderedField α<VAR>x y : α<GOAL>dist x y = ‖x - y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hfg : f =ᶠ[l] g<GOAL>Asymptotics.SuperpolynomialDecay l k g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hfg : ∀ (x : α), f x = g x<GOAL>Asymptotics.SuperpolynomialDecay l k g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>l : Filter α<VAR>k : α → β<GOAL>Asymptotics.SuperpolynomialDecay l k 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousAdd β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hg : Asymptotics.SuperpolynomialDecay l k g<GOAL>Asymptotics.SuperpolynomialDecay l k (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousMul β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hg : Asymptotics.SuperpolynomialDecay l k g<GOAL>Asymptotics.SuperpolynomialDecay l k (f * g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousMul β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>c : β<GOAL>Asymptotics.SuperpolynomialDecay l k fun n => f n * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousMul β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>c : β<GOAL>Asymptotics.SuperpolynomialDecay l k fun n => c * f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<GOAL>Asymptotics.SuperpolynomialDecay l k (k * f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<GOAL>Asymptotics.SuperpolynomialDecay l k (f * k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>n : ℕ<GOAL>Asymptotics.SuperpolynomialDecay l k (k ^ n * f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>n : ℕ<GOAL>Asymptotics.SuperpolynomialDecay l k (f * k ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousAdd β<VAR>ContinuousMul β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>p : Polynomial β<GOAL>Asymptotics.SuperpolynomialDecay l k fun x => Polynomial.eval (k x) p * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>CommSemiring β<VAR>ContinuousAdd β<VAR>ContinuousMul β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>p : Polynomial β<GOAL>Asymptotics.SuperpolynomialDecay l k fun x => f x * Polynomial.eval (k x) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>TopologicalSpace β<VAR>OrderedCommSemiring β<VAR>OrderTopology β<VAR>hk : 0 ≤ᶠ[l] k<VAR>hg : Asymptotics.SuperpolynomialDecay l k g<VAR>hg' : Asymptotics.SuperpolynomialDecay l k g'<VAR>hfg : g ≤ᶠ[l] f<VAR>hfg' : f ≤ᶠ[l] g'<GOAL>Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedCommRing β<VAR>OrderTopology β<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun a => |k a ^ n * f a|) l (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedCommRing β<VAR>OrderTopology β<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ Asymptotics.SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedCommRing β<VAR>OrderTopology β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hfg : abs ∘ g ≤ᶠ[l] abs ∘ f<GOAL>Asymptotics.SuperpolynomialDecay l k g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedCommRing β<VAR>OrderTopology β<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>hfg : ∀ (x : α), |g x| ≤ |f x|<GOAL>Asymptotics.SuperpolynomialDecay l k g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>Field β<VAR>ContinuousMul β<VAR>c : β<VAR>hc0 : c ≠ 0<GOAL>(Asymptotics.SuperpolynomialDecay l k fun n => f n * c) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>Field β<VAR>ContinuousMul β<VAR>c : β<VAR>hc0 : c ≠ 0<GOAL>(Asymptotics.SuperpolynomialDecay l k fun n => c * f n) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Filter.Tendsto (fun a => k a ^ z * f a) l (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>z : ℤ<GOAL>Asymptotics.SuperpolynomialDecay l k fun a => k a ^ z * f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<VAR>z : ℤ<GOAL>Asymptotics.SuperpolynomialDecay l k fun a => f a * k a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<GOAL>Asymptotics.SuperpolynomialDecay l k (k⁻¹ * f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>hf : Asymptotics.SuperpolynomialDecay l k f<GOAL>Asymptotics.SuperpolynomialDecay l k (f * k⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k (k * f) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k (f * k) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>n : ℕ<GOAL>Asymptotics.SuperpolynomialDecay l k (k ^ n * f) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>TopologicalSpace β<VAR>LinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<VAR>n : ℕ<GOAL>Asymptotics.SuperpolynomialDecay l k (f * k ^ n) ↔ Asymptotics.SuperpolynomialDecay l k f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>NormedLinearOrderedField β<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun a => ‖k a ^ n * f a‖) l (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f : α → β<VAR>NormedLinearOrderedField β<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ Asymptotics.SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>NormedLinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k : α → β<VAR>f : α → β<VAR>NormedLinearOrderedField β<VAR>OrderTopology β<VAR>hk : Filter.Tendsto k l Filter.atTop<GOAL>Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun a => k a ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>r : α<VAR>x : β<GOAL>‖r • x‖ ≤ ‖r‖ * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>r : α<VAR>x : β<GOAL>‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>dist (s • x) (s • y) ≤ ‖s‖ * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>s : α<GOAL>LipschitzWith ‖s‖₊ fun x => s • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedAddGroup α<VAR>SeminormedAddGroup β<VAR>SMulZeroClass α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedRing α<VAR>SeminormedAddCommGroup β<VAR>Module α β<VAR>h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖<GOAL>BoundedSMul α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SeminormedRing α<VAR>SeminormedAddCommGroup β<VAR>Module α β<VAR>h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊<GOAL>BoundedSMul α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedDivisionRing α<VAR>SeminormedAddGroup β<VAR>MulActionWithZero α β<VAR>BoundedSMul α β<VAR>r : α<VAR>x : β<GOAL>‖r • x‖ = ‖r‖ * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedDivisionRing α<VAR>SeminormedAddGroup β<VAR>MulActionWithZero α β<VAR>BoundedSMul α β<VAR>r : α<VAR>x : β<GOAL>‖r • x‖₊ = ‖r‖₊ * ‖x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedDivisionRing α<VAR>SeminormedAddCommGroup β<VAR>Module α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>dist (s • x) (s • y) = ‖s‖ * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedDivisionRing α<VAR>SeminormedAddCommGroup β<VAR>Module α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>nndist (s • x) (s • y) = ‖s‖₊ * nndist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedDivisionRing α<VAR>SeminormedAddCommGroup β<VAR>Module α β<VAR>BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>edist (s • x) (s • y) = ‖s‖₊ • edist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>AddCommGroup F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>NontriviallyNormedField 𝕜<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>ContinuousSMul 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>h : ∃ V ∈ 𝓝 0, Bornology.IsVonNBounded 𝕜 (⇑f '' V)<GOAL>↑(f.clmOfExistsBoundedImage h) = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>AddCommGroup F<VAR>UniformSpace F<VAR>UniformAddGroup F<VAR>NontriviallyNormedField 𝕜<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>ContinuousSMul 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>h : ∃ V ∈ 𝓝 0, Bornology.IsVonNBounded 𝕜 (⇑f '' V)<VAR>x : E<GOAL>(f.clmOfExistsBoundedImage h) x = f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>AddCommGroup F<VAR>UniformSpace F<VAR>FirstCountableTopology E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>RCLike 𝕜'<VAR>Module 𝕜' F<VAR>ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)<GOAL>ContinuousAt (⇑f) 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>AddCommGroup F<VAR>UniformSpace F<VAR>FirstCountableTopology E<VAR>RCLike 𝕜<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>RCLike 𝕜'<VAR>Module 𝕜' F<VAR>ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>UniformAddGroup F<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)<GOAL>Continuous ⇑f
<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>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₂] F<VAR>g : E →SL[σ₁₃] G<VAR>h : ∀ (x : E), ‖f x‖ = ‖g x‖<GOAL>‖f‖ = ‖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>RingHomIsometric σ₂₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>C : ℝ<VAR>h0 : 0 ≤ C<VAR>hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<GOAL>‖f‖ ≤ C
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>x : E<VAR>y : F<GOAL>‖(f x) y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>x : E<VAR>y : F<VAR>a b c : ℝ<VAR>hf : ‖f‖ ≤ a<VAR>hx : ‖x‖ ≤ b<VAR>hy : ‖y‖ ≤ c<GOAL>‖(f x) y‖ ≤ a * b * c
<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>f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G<VAR>C : ℝ<VAR>h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<VAR>x : E<GOAL>‖(f x).mkContinuous (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖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>RingHomIsometric σ₂₃<VAR>f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G<VAR>C : ℝ<VAR>hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<VAR>x : E<VAR>y : F<GOAL>((f.mkContinuous₂ C hC) x) y = (f x) y
<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>RingHomIsometric σ₂₃<VAR>f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G<VAR>C : ℝ<VAR>hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<GOAL>‖f.mkContinuous₂ C hC‖ ≤ max C 0
<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>RingHomIsometric σ₂₃<VAR>f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G<VAR>C : ℝ<VAR>h0 : 0 ≤ C<VAR>hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖<GOAL>‖f.mkContinuous₂ C hC‖ ≤ C
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>‖f‖ ≤ ‖f.flip‖
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<VAR>x : E<VAR>y : F<GOAL>(f.flip y) x = (f x) y
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>f.flip.flip = f
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>‖f.flip‖ = ‖f‖
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>f g : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>(f + g).flip = f.flip + g.flip
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<VAR>c : 𝕜₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>(c • f).flip = c • f.flip
<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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<GOAL>(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃).symm = ContinuousLinearMap.flipₗᵢ' F E 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>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₁₃<GOAL>⇑(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃) = ContinuousLinearMap.flip
<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ₗ).symm = ContinuousLinearMap.flipₗᵢ 𝕜 Fₗ E Gₗ