ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Norm α<VAR>Norm β<VAR>hp : 0 < p.toReal<VAR>f : WithLp p (α × β)<GOAL>‖f‖ = (‖f.1‖ ^ p.toReal + ‖f.2‖ ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f g : WithLp ⊤ (α × β)<GOAL>edist f.1 g.1 ⊔ edist f.2 g.2 ≠ ⊤
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>LipschitzWith 1 ⇑(WithLp.equiv p (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>AntilipschitzWith (2 ^ (1 / p).toReal) ⇑(WithLp.equiv p (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>𝓤 (WithLp p (α × β)) = 𝓤 (α × β)
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<GOAL>Bornology.cobounded (WithLp p (α × β)) = Bornology.cobounded (α × β)
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<GOAL>Continuous ⇑(WithLp.equiv p (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<GOAL>Continuous ⇑(WithLp.equiv p (α × β)).symm
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous ⇑(WithLp.equiv p (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformContinuous ⇑(WithLp.equiv p (α × β)).symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Semiring 𝕜<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>Module 𝕜 α<VAR>Module 𝕜 β<GOAL>⇑(WithLp.prodContinuousLinearEquiv p 𝕜 α β).symm = ⇑(WithLp.equiv p (α × β)).symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Semiring 𝕜<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>Module 𝕜 α<VAR>Module 𝕜 β<GOAL>⇑(WithLp.prodContinuousLinearEquiv p 𝕜 α β) = ⇑(WithLp.equiv p (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<GOAL>p ≠ ⊤ → ∀ (x y : WithLp p (α × β)), nndist x y = (nndist x.1 y.1 ^ p.toReal + nndist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x y : WithLp ⊤ (α × β)<GOAL>nndist x y = nndist x.1 y.1 ⊔ nndist x.2 y.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>Isometry ⇑(WithLp.equiv ⊤ (α × β))
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>Norm α<VAR>Norm β<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : WithLp p (α × β)<GOAL>‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<GOAL>p ≠ ⊤ → ∀ (f : WithLp p (α × β)), ‖f‖₊ = (‖f.1‖₊ ^ p.toReal + ‖f.2‖₊ ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>f : WithLp ⊤ (α × β)<GOAL>‖f‖₊ = ‖f.1‖₊ ⊔ ‖f.2‖₊
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>f : WithLp ⊤ (α × β)<GOAL>‖(WithLp.equiv ⊤ (α × β)) f‖₊ = ‖f‖₊
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>f : α × β<GOAL>‖(WithLp.equiv ⊤ (α × β)).symm f‖₊ = ‖f‖₊
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>f : WithLp ⊤ (α × β)<GOAL>‖(WithLp.equiv ⊤ (α × β)) f‖ = ‖f‖
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>f : α × β<GOAL>‖(WithLp.equiv ⊤ (α × β)).symm f‖ = ‖f‖
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖ = √(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖₊ = NNReal.sqrt (‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖ ^ 2 = ‖x.1‖ ^ 2 + ‖x.2‖ ^ 2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>dist x y = √(dist x.1 y.1 ^ 2 + dist x.2 y.2 ^ 2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>nndist x y = NNReal.sqrt (nndist x.1 y.1 ^ 2 + nndist x.2 y.2 ^ 2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>edist x y = (edist x.1 y.1 ^ 2 + edist x.2 y.2 ^ 2) ^ (1 / 2)
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x : α<GOAL>‖(WithLp.equiv p (α × β)).symm (x, 0)‖₊ = ‖x‖₊
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>y : β<GOAL>‖(WithLp.equiv p (α × β)).symm (0, y)‖₊ = ‖y‖₊
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x : α<GOAL>‖(WithLp.equiv p (α × β)).symm (x, 0)‖ = ‖x‖
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>y : β<GOAL>‖(WithLp.equiv p (α × β)).symm (0, y)‖ = ‖y‖
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x₁ x₂ : α<GOAL>nndist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = nndist x₁ x₂
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>y₁ y₂ : β<GOAL>nndist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = nndist y₁ y₂
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x₁ x₂ : α<GOAL>dist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = dist x₁ x₂
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>y₁ y₂ : β<GOAL>dist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = dist y₁ y₂
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>x₁ x₂ : α<GOAL>edist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = edist x₁ x₂
<VAR>p : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>SeminormedAddCommGroup α<VAR>SeminormedAddCommGroup β<VAR>y₁ y₂ : β<GOAL>edist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = edist y₁ y₂
<VAR>E : Type u_1<VAR>i : SeminormedAddCommGroup E<VAR>r : ℝ<VAR>v : ↑(Metric.sphere 0 r)<GOAL>↑(-v) = -↑v
<VAR>E : Type u_1<VAR>i : SeminormedAddCommGroup E<VAR>r : ℝ<VAR>v : ↑(Metric.ball 0 r)<GOAL>↑(-v) = -↑v
<VAR>E : Type u_1<VAR>i : SeminormedAddCommGroup E<VAR>r : ℝ<VAR>v : ↑(Metric.closedBall 0 r)<GOAL>↑(-v) = -↑v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>A : E →L[𝕜] F<VAR>x : E<GOAL>((ContinuousLinearMap.toWOT 𝕜 E F) A) x = A x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>h : ∀ (x : E), A x = B x<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<GOAL>A = B ↔ ∀ (x : E), A x = B x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<GOAL>A = B ↔ ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<GOAL>0 x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E →WOT[𝕜]F<VAR>x : E<GOAL>(f + g) x = f x + g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f g : E →WOT[𝕜]F<VAR>x : E<GOAL>(f - g) x = f x - g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →WOT[𝕜]F<VAR>x : E<GOAL>(-f) x = -f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →WOT[𝕜]F<VAR>c : 𝕜<VAR>x : E<GOAL>(c • f) x = c • f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>Continuous ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 F<GOAL>Continuous fun A => y (A x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>g : α → E →WOT[𝕜]F<VAR>h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Continuous fun a => y ((g a) x)<GOAL>Continuous g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>Embedding ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<GOAL>Filter.Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Filter.Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>l : Filter (E →WOT[𝕜]F)<VAR>A : E →WOT[𝕜]F<GOAL>l ≤ 𝓝 A ↔ ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Filter.map (fun T => y (T x)) l ≤ 𝓝 (y (A x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>(𝓝 0).HasBasis (ContinuousLinearMapWOT.seminormFamily 𝕜 E F).basisSets id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>WithSeminorms (ContinuousLinearMapWOT.seminormFamily 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>Continuous ⇑(ContinuousLinearMap.toWOT 𝕜 E F)
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>Zero M₁<VAR>TopologicalSpace M₁<VAR>TopologicalSpace M₂<VAR>Zero M₂<GOAL>IsCompactOperator 0
<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>f : M₁ → M₂<GOAL>IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, ∃ K, IsCompact K ∧ f '' V ⊆ K
<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>f : M₁ → M₂<GOAL>IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsVonNBounded 𝕜₁ S<GOAL>∃ K, IsCompact K ∧ ⇑f '' S ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsVonNBounded 𝕜₁ S<GOAL>IsCompact (closure (⇑f '' S))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsBounded S<GOAL>∃ K, IsCompact K ∧ ⇑f '' S ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsBounded S<GOAL>IsCompact (closure (⇑f '' S))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>r : ℝ<GOAL>∃ K, IsCompact K ∧ ⇑f '' Metric.ball 0 r ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>r : ℝ<GOAL>∃ K, IsCompact K ∧ ⇑f '' Metric.closedBall 0 r ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>r : ℝ<GOAL>IsCompact (closure (⇑f '' Metric.ball 0 r))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>r : ℝ<GOAL>IsCompact (closure (⇑f '' Metric.closedBall 0 r))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>IsCompactOperator ⇑f ↔ ∃ K, IsCompact K ∧ ⇑f '' Metric.ball 0 r ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>IsCompactOperator ⇑f ↔ ∃ K, IsCompact K ∧ ⇑f '' Metric.closedBall 0 r ⊆ K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.ball 0 r))
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.closedBall 0 r))
<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>S : Type u_9<VAR>Monoid S<VAR>DistribMulAction S M₂<VAR>ContinuousConstSMul S M₂<VAR>f : M₁ → M₂<VAR>hf : IsCompactOperator f<VAR>c : S<GOAL>IsCompactOperator (c • f)
<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>ContinuousAdd M₂<VAR>f g : M₁ → M₂<VAR>hf : IsCompactOperator f<VAR>hg : IsCompactOperator g<GOAL>IsCompactOperator (f + g)
<VAR>M₁ : Type u_5<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₄<VAR>AddCommGroup M₄<VAR>ContinuousNeg M₄<VAR>f : M₁ → M₄<VAR>hf : IsCompactOperator f<GOAL>IsCompactOperator (-f)
<VAR>M₁ : Type u_5<VAR>M₄ : Type u_8<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>TopologicalSpace M₄<VAR>AddCommGroup M₄<VAR>TopologicalAddGroup M₄<VAR>f g : M₁ → M₄<VAR>hf : IsCompactOperator f<VAR>hg : IsCompactOperator g<GOAL>IsCompactOperator (f - g)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₁<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>f : M₂ → M₃<VAR>hf : IsCompactOperator f<VAR>g : M₁ →SL[σ₁₂] M₂<GOAL>IsCompactOperator (f ∘ ⇑g)
<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₁<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₁<VAR>f : M₁ → M₂<VAR>hf : IsCompactOperator f<VAR>g : M₂ → M₃<VAR>hg : Continuous g<GOAL>IsCompactOperator (g ∘ f)
<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>TopologicalSpace M₁<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>AddCommMonoid M₃<VAR>Module R₃ M₃<VAR>f : M₁ → M₂<VAR>hf : IsCompactOperator f<VAR>g : M₂ →SL[σ₂₃] M₃<GOAL>IsCompactOperator (⇑g ∘ f)
<VAR>R₂ : Type u_2<VAR>Semiring R₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>f : M₁ → M₂<VAR>hf : IsCompactOperator f<VAR>V : Submodule R₂ M₂<VAR>hV : ∀ (x : M₁), f x ∈ V<VAR>h_closed : IsClosed ↑V<GOAL>IsCompactOperator (Set.codRestrict f (↑V) hV)
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f : M₁ →ₗ[R₁] M₁<VAR>hf : IsCompactOperator ⇑f<VAR>V : Submodule R₁ M₁<VAR>hV : ∀ v ∈ V, f v ∈ V<VAR>h_closed : IsClosed ↑V<GOAL>IsCompactOperator ⇑(f.restrict hV)
<VAR>R₂ : Type u_2<VAR>Semiring R₂<VAR>M₂ : Type u_5<VAR>UniformSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>T0Space M₂<VAR>f : M₂ →ₗ[R₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>V : Submodule R₂ M₂<VAR>hV : ∀ v ∈ V, f v ∈ V<VAR>hcomplete : CompleteSpace ↥V<GOAL>IsCompactOperator ⇑(f.restrict hV)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>TopologicalAddGroup M₁<VAR>ContinuousConstSMul 𝕜₁ M₁<VAR>TopologicalAddGroup M₂<VAR>ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<GOAL>Continuous ⇑f
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>TopologicalAddGroup M₁<VAR>ContinuousConstSMul 𝕜₁ M₁<VAR>TopologicalAddGroup M₂<VAR>ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<GOAL>↑(ContinuousLinearMap.mkOfIsCompactOperator hf) = f
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>TopologicalAddGroup M₁<VAR>ContinuousConstSMul 𝕜₁ M₁<VAR>TopologicalAddGroup M₂<VAR>ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<GOAL>⇑(ContinuousLinearMap.mkOfIsCompactOperator hf) = ⇑f
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommGroup M₁<VAR>TopologicalSpace M₂<VAR>AddCommGroup M₂<VAR>Module 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>TopologicalAddGroup M₁<VAR>ContinuousConstSMul 𝕜₁ M₁<VAR>TopologicalAddGroup M₂<VAR>ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<GOAL>ContinuousLinearMap.mkOfIsCompactOperator hf ∈ compactOperator σ₁₂ M₁ M₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>AddCommGroup M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>UniformSpace M₂<VAR>UniformAddGroup M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>CompleteSpace M₂<GOAL>IsClosed {f | IsCompactOperator ⇑f}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>SeminormedAddCommGroup M₁<VAR>AddCommGroup M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>UniformSpace M₂<VAR>UniformAddGroup M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>CompleteSpace M₂<GOAL>(compactOperator σ₁₂ M₁ M₂).topologicalClosure = compactOperator σ₁₂ M₁ M₂
<VAR>ι : Type u_1<VAR>𝕜₁ : Type u_2<VAR>𝕜₂ : Type u_3<VAR>NontriviallyNormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>SeminormedAddCommGroup M₁<VAR>AddCommGroup M₂<VAR>NormedSpace 𝕜₁ M₁<VAR>Module 𝕜₂ M₂<VAR>UniformSpace M₂<VAR>UniformAddGroup M₂<VAR>ContinuousConstSMul 𝕜₂ M₂<VAR>T2Space M₂<VAR>CompleteSpace M₂<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → M₁ →SL[σ₁₂] M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf : Filter.Tendsto F l (𝓝 f)<VAR>hF : ∀ᶠ (i : ι) in l, IsCompactOperator ⇑(F i)<GOAL>IsCompactOperator ⇑f
<VAR>r : ℚ<GOAL>‖↑r‖ = ‖r‖