ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(i.sup p).ball 0 r ∈ p.basisSets
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(p i).ball 0 r ∈ p.basisSets
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>Nonempty ι<GOAL>p.basisSets.Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U V : Set E<VAR>hU : U ∈ p.basisSets<VAR>hV : V ∈ p.basisSets<GOAL>∃ z ∈ p.basisSets, z ⊆ U ∩ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>0 ∈ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ p.basisSets, V + V ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU' : U ∈ p.basisSets<GOAL>∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>Nonempty ι<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>Nonempty ι<VAR>x : 𝕜<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<GOAL>AddGroupFilterBasis.toFilterBasis.filter = ⨅ i, Filter.comap (⇑(p i)) (𝓝 0)
<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>ι : Type u_12<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>ι' : Type u_10<VAR>Nonempty ι'<VAR>p : ι → Seminorm 𝕜 E<VAR>q : Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>Seminorm.IsBounded p (fun x => q) f ↔ ∃ s C, q.comp f ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>ι : Type u_10<VAR>Nonempty ι<VAR>p : Seminorm 𝕜 E<VAR>q : ι' → Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>Seminorm.IsBounded (fun x => p) q f ↔ ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>p : ι → Seminorm 𝕜 E<VAR>q : ι' → Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<VAR>hf : Seminorm.IsBounded p q f<VAR>s' : Finset ι'<GOAL>∃ C s, (s'.sup q).comp f ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>topology : TopologicalSpace E<VAR>self : WithSeminorms p<GOAL>topology = p.moduleFilterBasis.topology
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>t = p.moduleFilterBasis.topology
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>TopologicalAddGroup E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>ContinuousSMul 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>(𝓝 0).HasBasis (fun s => s ∈ p.basisSets) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>(𝓝 0).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>U : Set E<GOAL>U ∈ 𝓝 x ↔ ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>U : Set E<GOAL>IsOpen U ↔ ∀ x ∈ U, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<GOAL>T1Space E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<GOAL>∃ i, (p i) x ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>(∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0) ↔ T1Space E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>f : Filter F<VAR>y₀ : E<GOAL>Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>f : Filter F<VAR>y₀ : E<GOAL>Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>SemilatticeSup F<VAR>Nonempty F<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>y₀ : E<GOAL>Filter.Tendsto u Filter.atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter<GOAL>WithSeminorms p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : (𝓝 0).HasBasis (fun s => s ∈ p.basisSets) id<GOAL>WithSeminorms p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ 𝓝 0 = ⨅ i, Filter.comap (⇑(p i)) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ t = ⨅ i, UniformSpace.toTopologicalSpace
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>i : ι<GOAL>Continuous ⇑(p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>u : UniformSpace E<VAR>UniformAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace
<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>WithSeminorms fun x => normSeminorm 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>f : G → E<VAR>s : Set G<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>f : G → E<VAR>s : Set G<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r
<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>AddCommGroup E<VAR>NormedField 𝕝<VAR>Module 𝕝 E<VAR>AddCommGroup F<VAR>NormedField 𝕝₂<VAR>Module 𝕝₂ F<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>RingHomIsometric τ₁₂<VAR>Nonempty ι'<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι'), Continuous ⇑((q i).comp f)<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NontriviallyNormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>Nonempty ι'<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>Continuous ⇑f ↔ ∀ (i : ι'), Continuous ⇑((q i).comp f)
<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>AddCommGroup E<VAR>NormedField 𝕝<VAR>Module 𝕝 E<VAR>AddCommGroup F<VAR>NormedField 𝕝₂<VAR>Module 𝕝₂ F<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>RingHomIsometric τ₁₂<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<GOAL>∀ {x : TopologicalSpace E}, WithSeminorms p → ∀ {x_1 : TopologicalSpace F}, WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Seminorm.IsBounded p q f → Continuous ⇑f
<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>AddCommGroup E<VAR>NormedField 𝕝<VAR>Module 𝕝 E<VAR>NormedField 𝕝₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>RingHomIsometric τ₁₂<VAR>Nonempty ι<VAR>F : Type u_10<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕝₂ F<VAR>TopologicalSpace E<VAR>p : ι → Seminorm 𝕝 E<VAR>hp : WithSeminorms p<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p<GOAL>Continuous ⇑f
<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕝<VAR>AddCommGroup F<VAR>NormedField 𝕝₂<VAR>Module 𝕝₂ F<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>RingHomIsometric τ₁₂<VAR>Nonempty ι<VAR>E : Type u_10<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕝 E<VAR>TopologicalSpace F<VAR>q : ι → Seminorm 𝕝₂ F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NontriviallyNormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<GOAL>[EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NontriviallyNormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<GOAL>UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι' : Type u_9<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NontriviallyNormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>UniformSpace E<VAR>UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<GOAL>UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>q : SeminormFamily 𝕜 E ι'<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>hpq : Seminorm.IsBounded p q LinearMap.id<VAR>hqp : Seminorm.IsBounded q p LinearMap.id<GOAL>WithSeminorms q
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>Nonempty ι<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>WithSeminorms fun s => s.sup p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>Nonempty ι<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Preorder ι<VAR>LocallyFiniteOrderBot ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>WithSeminorms fun i => (Finset.Iic i).sup p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>e : ι' ≃ ι<GOAL>WithSeminorms (p ∘ ⇑e)
<VAR>𝕜 : Type u_1<VAR>F : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<VAR>x : F<VAR>hx : ‖x‖ = 0<GOAL>q x = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>q : Seminorm 𝕜 F<VAR>hq : Continuous ⇑q<GOAL>∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>Nonempty ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>q : Seminorm 𝕜 E<VAR>hq : Continuous ⇑q<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>Nonempty ι<VAR>NormedField 𝕜<VAR>NormedSpace ℝ 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<VAR>TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>LocallyConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>NormedField 𝕜<VAR>NormedSpace ℝ 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Module ℝ E<VAR>IsScalarTower ℝ 𝕜 E<GOAL>LocallyConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>i : ι<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>q.comp f i = (q i).comp f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>s : Finset ι<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>(s.sup q).comp f = s.sup (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NormedField 𝕜₂<VAR>AddCommGroup F<VAR>Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>TopologicalSpace E<VAR>f : E →ₛₗ[σ₁₂] F<VAR>hf : Inducing ⇑f<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>κ : ι → Type u_10<VAR>Nonempty ((i : ι) × κ i)<VAR>∀ (i : ι), Nonempty (κ i)<VAR>p : (i : ι) → SeminormFamily 𝕜 E (κ i)<VAR>t : ι → TopologicalSpace E<VAR>∀ (i : ι), TopologicalAddGroup E<VAR>hp : ∀ (i : ι), WithSeminorms (p i)<GOAL>WithSeminorms (SeminormFamily.sigma p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nonempty ι<VAR>Countable ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>FirstCountableTopology E
<VAR>p : ℝ≥0∞<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>x y : PiLp p α<VAR>h : ∀ (i : ι), x i = y i<GOAL>x = y
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>i : ι<GOAL>0 i = 0
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp p β<VAR>i : ι<GOAL>(x + y) i = x i + y i
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp p β<VAR>i : ι<GOAL>(x - y) i = x i - y i
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>SeminormedRing 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>x : PiLp p β<VAR>i : ι<GOAL>(c • x) i = c • x i
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp p β<VAR>i : ι<GOAL>(-x) i = -x i
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>x : PiLp p α<VAR>i : ι<GOAL>(WithLp.equiv p ((i : ι) → α i)) x i = x i
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>x : (i : ι) → α i<VAR>i : ι<GOAL>(WithLp.equiv p ((i : ι) → α i)).symm x i = x i
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → EDist (β i)<VAR>f g : PiLp 0 β<GOAL>edist f g = ↑⋯.toFinset.card
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → EDist (β i)<VAR>p : ℝ≥0∞<VAR>hp : 0 < p.toReal<VAR>f g : PiLp p β<GOAL>edist f g = (∑ i : ι, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → EDist (β i)<VAR>f g : PiLp ⊤ β<GOAL>edist f g = ⨆ i, edist (f i) (g i)
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>f : PiLp p β<GOAL>edist f f = 0
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>f g : PiLp p β<GOAL>edist f g = edist g f
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → Dist (α i)<VAR>f g : PiLp 0 α<GOAL>dist f g = ↑⋯.toFinset.card
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → Dist (α i)<VAR>p : ℝ≥0∞<VAR>hp : 0 < p.toReal<VAR>f g : PiLp p α<GOAL>dist f g = (∑ i : ι, dist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>Fintype ι<VAR>(i : ι) → Dist (α i)<VAR>f g : PiLp ⊤ α<GOAL>dist f g = ⨆ i, dist (f i) (g i)
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → Norm (β i)<VAR>f : PiLp 0 β<GOAL>‖f‖ = ↑⋯.toFinset.card
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → Norm (β i)<VAR>f : PiLp ⊤ β<GOAL>‖f‖ = ⨆ i, ‖f i‖
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → Norm (β i)<VAR>hp : 0 < p.toReal<VAR>f : PiLp p β<GOAL>‖f‖ = (∑ i : ι, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)
<VAR>ι : Type u_5<VAR>Finite ι<VAR>α : ι → Type u_6<VAR>(i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<GOAL>⨆ i, edist (f i) (g i) ≠ ⊤
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>Fintype ι<GOAL>LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>Fintype ι<GOAL>AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>Fintype ι<GOAL>𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>Fact (1 ≤ p)<VAR>(i : ι) → PseudoMetricSpace (α i)<VAR>Fintype ι<GOAL>Bornology.cobounded (PiLp p α) = Bornology.cobounded ((i : ι) → α i)
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → UniformSpace (β i)<GOAL>UniformContinuous ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → UniformSpace (β i)<GOAL>UniformContinuous ⇑(WithLp.equiv p ((i : ι) → β i)).symm
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → UniformSpace (β i)<GOAL>Continuous ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>(i : ι) → UniformSpace (β i)<GOAL>Continuous ⇑(WithLp.equiv p ((i : ι) → β i)).symm
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>(i : ι) → PseudoMetricSpace (β i)<VAR>hp : p ≠ ⊤<VAR>x y : PiLp p β<GOAL>nndist x y = (∑ i : ι, nndist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal)