ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>f : E → F<VAR>hf : IsLinearMap 𝕜 f<GOAL>StarConvex 𝕜 (f x) (f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>s : Set F<VAR>f : E →ₗ[𝕜] F<VAR>hs : StarConvex 𝕜 (f x) s<GOAL>StarConvex 𝕜 x (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>s : Set F<VAR>f : E → F<VAR>hs : StarConvex 𝕜 (f x) s<VAR>hf : IsLinearMap 𝕜 f<GOAL>StarConvex 𝕜 x (f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x + y) (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<GOAL>StarConvex 𝕜 (z + x) ((fun x => z + x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<GOAL>StarConvex 𝕜 (x + z) ((fun x => x + z) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 (z + x) s<GOAL>StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 (x + z) s<GOAL>StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>s : Set (E × E)<VAR>hs : StarConvex 𝕜 (x, y) s<GOAL>StarConvex 𝕜 (x - y) ((fun x => x.1 - x.2) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>c : 𝕜<GOAL>StarConvex 𝕜 (c • x) (c • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>c : 𝕜<VAR>hs : StarConvex 𝕜 (c • x) s<GOAL>StarConvex 𝕜 x ((fun z => c • z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<VAR>c : 𝕜<GOAL>StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>SMulWithZero 𝕜 E<VAR>s : Set E<GOAL>StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 0 s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>t • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • (y - x) ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hs : StarConvex 𝕜 (f x) s<GOAL>StarConvex 𝕜 x (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x : E<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 (f x) (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 (-x) (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x - y) (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x y : E<VAR>h : x < y<GOAL>StarConvex 𝕜 y (Set.Iic x)ᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>OrderedAddCommGroup E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x y : E<VAR>h : x < y<GOAL>StarConvex 𝕜 x (Set.Ici y)ᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 0 s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : 1 ≤ t<GOAL>x ∈ t • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>hx : x ∈ s<VAR>h : ∀ y ∈ s, x ≤ y ∨ y ≤ x<GOAL>StarConvex 𝕜 x s
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s ↔ s.OrdConnected
<VAR>𝕜 : Type u_13<VAR>E : Type u_14<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>self : Seminorm 𝕜 E<VAR>a : 𝕜<VAR>x : E<GOAL>self.toFun (a • x) = ‖a‖ * self.toFun x
<VAR>F : Type u_13<VAR>𝕜 : outParam (Type u_14)<VAR>E : outParam (Type u_15)<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>FunLike F E ℝ<VAR>self : SeminormClass F 𝕜 E<VAR>f : F<VAR>a : 𝕜<VAR>x : E<GOAL>f (a • x) = ‖a‖ * f x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>h : ∀ (x : E), p x = q x<GOAL>p = q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<GOAL>⇑0 = 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>x : E<GOAL>0 x = 0
<VAR>R : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : Seminorm 𝕜 E<GOAL>⇑(r • p) = r • ⇑p
<VAR>R : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : Seminorm 𝕜 E<VAR>x : E<GOAL>(r • p) x = r • p x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>⇑(p + q) = ⇑p + ⇑q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x : E<GOAL>(p + q) x = p x + q x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<GOAL>∀ (a : Seminorm 𝕜 E) (a_1 : E), (Seminorm.coeFnAddMonoidHom 𝕜 E) a a_1 = a a_1
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<GOAL>Function.Injective ⇑(Seminorm.coeFnAddMonoidHom 𝕜 E)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>R : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : Seminorm 𝕜 E<GOAL>r • (p ⊔ q) = r • p ⊔ r • q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>p ≤ q ↔ ∀ (x : E), p x ≤ q x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<GOAL>p < q ↔ p ≤ q ∧ ∃ x, p x < q x
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<GOAL>⇑(p.comp f) = ⇑p ∘ ⇑f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>x : E<GOAL>(p.comp f) x = p (f x)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<GOAL>p.comp LinearMap.id = p
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<GOAL>p.comp 0 = 0
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<GOAL>Seminorm.comp 0 f = 0
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomIsometric σ₁₃<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>AddCommGroup E₃<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>Module 𝕜₃ E₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p : Seminorm 𝕜₃ E₃<VAR>g : E₂ →ₛₗ[σ₂₃] E₃<VAR>f : E →ₛₗ[σ₁₂] E₂<GOAL>p.comp (g.comp f) = (p.comp g).comp f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p q : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<GOAL>(p + q).comp f = p.comp f + q.comp f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f g : E →ₛₗ[σ₁₂] E₂<GOAL>p.comp (f + g) ≤ p.comp f + p.comp g
<VAR>R : Type u_1<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>c : R<GOAL>(c • p).comp f = c • p.comp f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p q : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>hp : p ≤ q<GOAL>p.comp f ≤ q.comp f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>p : Seminorm 𝕜₂ E₂<GOAL>(Seminorm.pullback f) p = p.comp f
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>⇑⊥ = 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>⊥ = 0
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>a b : ℝ≥0<VAR>hpq : p ≤ q<VAR>hab : a ≤ b<GOAL>a • p ≤ b • q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<GOAL>(s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>x : E<GOAL>∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<GOAL>(s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>C : ℝ≥0<GOAL>s.sup (C • p) = C • s.sup p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<GOAL>s.sup p ≤ ∑ i ∈ s, p i
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>h : ∀ i ∈ s, (p i) x ≤ a<GOAL>(s.sup p) x ≤ a
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(p i) x ≤ (s.sup p) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ<VAR>ha : 0 < a<VAR>h : ∀ i ∈ s, (p i) x < a<GOAL>(s.sup p) x < a
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x y : E<GOAL>‖p x - p y‖ ≤ p (x - y)
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedCommRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>c : 𝕜₂<GOAL>p.comp (c • f) = ‖c‖₊ • p.comp f
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>SeminormedCommRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>AddCommGroup E<VAR>AddCommGroup E₂<VAR>Module 𝕜 E<VAR>Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>c : 𝕜₂<VAR>x : E<GOAL>(p.comp (c • f)) x = ‖c‖ * p (f x)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x : E<GOAL>BddBelow (Set.range fun u => p u + q (x - u))
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x : E<GOAL>(p ⊓ q) x = ⨅ u, p u + q (x - u)
<VAR>R : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : Seminorm 𝕜 E<GOAL>r • (p ⊓ q) = r • p ⊓ r • q
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs : BddAbove (DFunLike.coe '' s)<GOAL>⇑(sSup s) = ⨆ p, ⇑↑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set (Seminorm 𝕜 E)<GOAL>BddAbove s ↔ BddAbove (DFunLike.coe '' s)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<GOAL>BddAbove (Set.range p) ↔ ∀ (x : E), BddAbove (Set.range fun i => (p i) x)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs : BddAbove s<GOAL>⇑(sSup s) = ⨆ p, ⇑↑p
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (Set.range p)<GOAL>⇑(⨆ i, p i) = ⨆ i, ⇑(p i)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hp : BddAbove s<VAR>x : E<GOAL>(sSup s) x = ⨆ p, ↑p x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>hp : BddAbove (Set.range p)<VAR>x : E<GOAL>(⨆ i, p i) x = ⨆ i, (p i) x
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<GOAL>sSup ∅ = ⊥
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set (Seminorm 𝕜 E)<VAR>hs₁ : BddAbove s<VAR>hs₂ : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>y ∈ p.ball x r ↔ p (y - x) < r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>y ∈ p.closedBall x r ↔ p (y - x) ≤ r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>x ∈ p.ball x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>x ∈ p.closedBall x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>y : E<VAR>r : ℝ<GOAL>y ∈ p.ball 0 r ↔ p y < r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>y : E<VAR>r : ℝ<GOAL>y ∈ p.closedBall 0 r ↔ p y ≤ r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.ball 0 r = {y | p y < r}
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.closedBall 0 r = {y | p y ≤ r}
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>p.ball x r ⊆ p.closedBall x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>Seminorm.ball 0 x r = Set.univ
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>Seminorm.closedBall 0 x r = Set.univ
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>r : ℝ<VAR>x : E<GOAL>(c • p).ball x r = p.ball x (r / ↑c)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>r : ℝ<VAR>x : E<GOAL>(c • p).closedBall x r = p.closedBall x (r / ↑c)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>e : E<VAR>r : ℝ<GOAL>(p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>e : E<VAR>r : ℝ<GOAL>(p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>e : E<VAR>r : ℝ<GOAL>(s.sup' H p).ball e r = s.inf' H fun i => (p i).ball e r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>e : E<VAR>r : ℝ<GOAL>(s.sup' H p).closedBall e r = s.inf' H fun i => (p i).closedBall e r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>h : r₁ ≤ r₂<GOAL>p.ball x r₁ ⊆ p.ball x r₂
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>h : r₁ ≤ r₂<GOAL>p.closedBall x r₁ ⊆ p.closedBall x r₂
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>p q : Seminorm 𝕜 E<VAR>h : q ≤ p<GOAL>p.ball x r ⊆ q.ball x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>p q : Seminorm 𝕜 E<VAR>h : q ≤ p<GOAL>p.closedBall x r ⊆ q.closedBall x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ : E<GOAL>p.ball x₁ r₁ + p.ball x₂ r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ : E<GOAL>p.closedBall x₁ r₁ + p.closedBall x₂ r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x₁ x₂ y : E<VAR>r : ℝ<GOAL>x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<GOAL>x +ᵥ p.ball y r = p.ball (x +ᵥ y) r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>SMul 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<GOAL>x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>SeminormedRing 𝕜₂<VAR>AddCommGroup E₂<VAR>Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>(p.comp f).ball x r = ⇑f ⁻¹' p.ball (f x) r
<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>SeminormedRing 𝕜₂<VAR>AddCommGroup E₂<VAR>Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>(p.comp f).closedBall x r = ⇑f ⁻¹' p.closedBall (f x) r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>⇑p ⁻¹' Metric.ball 0 r = {x | p x < r}
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>⇑p ⁻¹' Metric.closedBall 0 r = {x | p x ≤ r}
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>⊥.ball x r = Set.univ
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>⊥.closedBall x r = Set.univ
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>Balanced 𝕜 (p.ball 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>Balanced 𝕜 (p.closedBall 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(s.sup p).ball x r = ⋂ i ∈ s, (p i).ball x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r
<VAR>𝕜 : Type u_3<VAR>E : Type u_7<VAR>ι : Type u_12<VAR>SeminormedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(s.sup p).ball x r = s.inf fun i => (p i).ball x r