ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y : P<GOAL>dist x y = ‖y -ᵥ x‖
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y : P<GOAL>nndist x y = ‖y -ᵥ x‖₊
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x y : P<GOAL>dist (v +ᵥ x) (v +ᵥ y) = dist x y
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x y : P<GOAL>nndist (v +ᵥ x) (v +ᵥ y) = nndist x y
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v₁ v₂ : V<VAR>x : P<GOAL>dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v₁ v₂ : V<VAR>x : P<GOAL>nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x : P<GOAL>dist (v +ᵥ x) x = ‖v‖
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x : P<GOAL>nndist (v +ᵥ x) x = ‖v‖₊
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x : P<GOAL>dist x (v +ᵥ x) = ‖v‖
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>x : P<GOAL>nndist x (v +ᵥ x) = ‖v‖₊
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x p' : P<GOAL>(IsometryEquiv.vaddConst x).invFun p' = p' -ᵥ x
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x p' : P<GOAL>(IsometryEquiv.vaddConst x).symm p' = p' -ᵥ x
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P<VAR>v : V<GOAL>(IsometryEquiv.vaddConst x) v = v +ᵥ x
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y z : P<GOAL>dist (x -ᵥ y) (x -ᵥ z) = dist y z
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y z : P<GOAL>nndist (x -ᵥ y) (x -ᵥ z) = nndist y z
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P<GOAL>∀ (x_1 : V), (IsometryEquiv.constVSub x).invFun x_1 = -x_1 +ᵥ x
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P<GOAL>∀ (x_1 : V), (IsometryEquiv.constVSub x).symm x_1 = -x_1 +ᵥ x
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P<GOAL>∀ (x_1 : P), (IsometryEquiv.constVSub x) x_1 = x -ᵥ x_1
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y z : P<GOAL>dist (x -ᵥ z) (y -ᵥ z) = dist x y
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>x y z : P<GOAL>nndist (x -ᵥ z) (y -ᵥ z) = nndist x y
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v v' : V<VAR>p p' : P<GOAL>dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v v' : V<VAR>p p' : P<GOAL>nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>v v' : V<VAR>p p' : P<GOAL>edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>PseudoEMetricSpace α<VAR>f : α → V<VAR>g : α → P<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) (f +ᵥ g)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>PseudoEMetricSpace α<VAR>f g : α → P<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) (f -ᵥ g)
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>UniformContinuous fun x => x.1 +ᵥ x.2
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>UniformContinuous fun x => x.1 -ᵥ x.2
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<GOAL>Continuous fun x => x.1 -ᵥ x.2
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>l : Filter α<VAR>f g : α → P<VAR>x y : P<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y))
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>TopologicalSpace α<VAR>f g : α → P<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (f -ᵥ g)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>TopologicalSpace α<VAR>f g : α → P<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (f -ᵥ g) x
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>TopologicalSpace α<VAR>f g : α → P<VAR>x : α<VAR>s : Set α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (f -ᵥ g) s x
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>TopologicalSpace α<VAR>f g : α → P<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (f -ᵥ g) s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>R : Type u_6<VAR>Ring R<VAR>TopologicalSpace R<VAR>Module R V<VAR>ContinuousSMul R V<VAR>l : Filter α<VAR>f₁ f₂ : α → P<VAR>g : α → R<VAR>p₁ p₂ : P<VAR>c : R<VAR>h₁ : Filter.Tendsto f₁ l (𝓝 p₁)<VAR>h₂ : Filter.Tendsto f₂ l (𝓝 p₂)<VAR>hg : Filter.Tendsto g l (𝓝 c)<GOAL>Filter.Tendsto (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) l (𝓝 ((AffineMap.lineMap p₁ p₂) c))
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>R : Type u_6<VAR>Ring R<VAR>TopologicalSpace R<VAR>Module R V<VAR>ContinuousSMul R V<VAR>Invertible 2<VAR>l : Filter α<VAR>f₁ f₂ : α → P<VAR>p₁ p₂ : P<VAR>h₁ : Filter.Tendsto f₁ l (𝓝 p₁)<VAR>h₂ : Filter.Tendsto f₂ l (𝓝 p₂)<GOAL>Filter.Tendsto (fun x => midpoint R (f₁ x) (f₂ x)) l (𝓝 (midpoint R p₁ p₂))
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<GOAL>IsClosed (s +ᵥ t)
<VAR>M N : SemiNormedGrp<VAR>f₁ f₂ : M ⟶ N<VAR>h : ∀ (x : ↑M), f₁ x = f₂ x<GOAL>f₁ = f₂
<VAR>V : Type u<VAR>SeminormedAddCommGroup V<GOAL>↑(SemiNormedGrp.of V) = V
<VAR>V : SemiNormedGrp<GOAL>⇑(𝟙 V) = id
<VAR>M N K : SemiNormedGrp<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>V W : SemiNormedGrp<VAR>x : ↑V<GOAL>0 x = 0
<VAR>V : SemiNormedGrp<VAR>Subsingleton ↑V<GOAL>CategoryTheory.Limits.IsZero V
<VAR>V W : SemiNormedGrp<VAR>i : V ≅ W<VAR>h1 : NormedAddGroupHom.NormNoninc i.hom<VAR>h2 : NormedAddGroupHom.NormNoninc i.inv<GOAL>Isometry ⇑i.hom
<VAR>M N : SemiNormedGrp₁<VAR>f g : M ⟶ N<VAR>w : ⇑f = ⇑g<GOAL>f = g
<VAR>M N : SemiNormedGrp<VAR>f : M ⟶ N<VAR>i : NormedAddGroupHom.NormNoninc f<VAR>x : ↑(SemiNormedGrp₁.of ↑M)<GOAL>(SemiNormedGrp₁.mkHom f i) x = f x
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>(SemiNormedGrp₁.mkIso f i i').hom = SemiNormedGrp₁.mkHom f.hom i
<VAR>M N : SemiNormedGrp<VAR>f : M ≅ N<VAR>i : NormedAddGroupHom.NormNoninc f.hom<VAR>i' : NormedAddGroupHom.NormNoninc f.inv<GOAL>(SemiNormedGrp₁.mkIso f i i').inv = SemiNormedGrp₁.mkHom f.inv i'
<VAR>V : Type u<VAR>SeminormedAddCommGroup V<GOAL>↑(SemiNormedGrp₁.of V) = V
<VAR>V : SemiNormedGrp₁<GOAL>⇑(𝟙 V) = id
<VAR>M N K : SemiNormedGrp₁<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>V W : SemiNormedGrp₁<VAR>x : ↑V<GOAL>0 x = 0
<VAR>V : SemiNormedGrp₁<VAR>Subsingleton ↑V<GOAL>CategoryTheory.Limits.IsZero V
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>Function.Surjective ⇑(SemiNormedGrp.explicitCokernelπ f)
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>f ≫ SemiNormedGrp.explicitCokernelπ f = 0
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>(SemiNormedGrp.explicitCokernelπ f) (f x) = 0
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>SemiNormedGrp.explicitCokernelπ f ≫ SemiNormedGrp.explicitCokernelDesc w = g
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>cond : f ≫ g = 0<VAR>x : ↑Y<GOAL>(SemiNormedGrp.explicitCokernelDesc cond) ((SemiNormedGrp.explicitCokernelπ f) x) = g x
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<VAR>e : SemiNormedGrp.explicitCokernel f ⟶ Z<VAR>he : SemiNormedGrp.explicitCokernelπ f ≫ e = g<GOAL>e = SemiNormedGrp.explicitCokernelDesc w
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond' : f ≫ g = 0<GOAL>SemiNormedGrp.explicitCokernelDesc cond' ≫ h = SemiNormedGrp.explicitCokernelDesc ⋯
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>SemiNormedGrp.explicitCokernelDesc ⋯ = 0
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e₁ e₂ : SemiNormedGrp.explicitCokernel f ⟶ Z<VAR>h : SemiNormedGrp.explicitCokernelπ f ≫ e₁ = SemiNormedGrp.explicitCokernelπ f ≫ e₂<GOAL>e₁ = e₂
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>NormedAddGroupHom.IsQuotient (SemiNormedGrp.explicitCokernelπ f)
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>NormedAddGroupHom.NormNoninc (SemiNormedGrp.explicitCokernelπ f)
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<VAR>c : NNReal<VAR>h : ‖g‖ ≤ ↑c<GOAL>‖SemiNormedGrp.explicitCokernelDesc w‖ ≤ ↑c
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>cond : f ≫ g = 0<VAR>hg : NormedAddGroupHom.NormNoninc g<GOAL>NormedAddGroupHom.NormNoninc (SemiNormedGrp.explicitCokernelDesc cond)
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond : f ≫ g = 0<VAR>cond2 : g ≫ h = 0<GOAL>SemiNormedGrp.explicitCokernelDesc cond ≫ h = 0
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>‖SemiNormedGrp.explicitCokernelDesc w‖ ≤ ‖g‖
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>SemiNormedGrp.explicitCokernelπ f ≫ (SemiNormedGrp.explicitCokernelIso f).hom = CategoryTheory.Limits.cokernel.π f
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.cokernel.π f ≫ (SemiNormedGrp.explicitCokernelIso f).inv = SemiNormedGrp.explicitCokernelπ f
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>(SemiNormedGrp.explicitCokernelIso f).hom ≫ CategoryTheory.Limits.cokernel.desc f g w = SemiNormedGrp.explicitCokernelDesc w
<VAR>A B C D B' D' : SemiNormedGrp<VAR>fab : A ⟶ B<VAR>fbd : B ⟶ D<VAR>fac : A ⟶ C<VAR>fcd : C ⟶ D<VAR>h : fab ≫ fbd = fac ≫ fcd<VAR>fbb' : B ⟶ B'<VAR>fdd' : D ⟶ D'<VAR>condb : fab ≫ fbb' = 0<VAR>condd : fcd ≫ fdd' = 0<VAR>g : B' ⟶ D'<VAR>h' : fbb' ≫ g = fbd ≫ fdd'<GOAL>SemiNormedGrp.explicitCokernelDesc condb ≫ g = SemiNormedGrp.explicitCokernel.map h ≫ SemiNormedGrp.explicitCokernelDesc condd
<VAR>x : PUnit.{u_5 + 1}<GOAL>‖x‖ = 0
<VAR>E : Type u_2<VAR>Norm E<VAR>x : ULift.{u_5, u_2} E<GOAL>‖x‖ = ‖x.down‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : E<GOAL>‖{ down := x }‖ = ‖x‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : ULift.{u_5, u_2} E<GOAL>‖x.down‖ = ‖x‖
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : ULift.{u_5, u_2} E<GOAL>‖x‖₊ = ‖x.down‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : E<GOAL>‖{ down := x }‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : ULift.{u_5, u_2} E<GOAL>‖x.down‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>Norm E<VAR>x : Additive E<GOAL>‖Additive.toMul x‖ = ‖x‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : E<GOAL>‖Additive.ofMul x‖ = ‖x‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : Multiplicative E<GOAL>‖Multiplicative.toAdd x‖ = ‖x‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : E<GOAL>‖Multiplicative.ofAdd x‖ = ‖x‖
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : Additive E<GOAL>‖Additive.toMul x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : E<GOAL>‖Additive.ofMul x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : Multiplicative E<GOAL>‖Multiplicative.toAdd x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : E<GOAL>‖Multiplicative.ofAdd x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>Norm E<VAR>x : E<GOAL>‖OrderDual.toDual x‖ = ‖x‖
<VAR>E : Type u_2<VAR>Norm E<VAR>x : Eᵒᵈ<GOAL>‖OrderDual.ofDual x‖ = ‖x‖
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : E<GOAL>‖OrderDual.toDual x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>NNNorm E<VAR>x : Eᵒᵈ<GOAL>‖OrderDual.ofDual x‖₊ = ‖x‖₊
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Norm E<VAR>Norm F<VAR>x : E × F<GOAL>‖x‖ = max ‖x.1‖ ‖x.2‖
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Norm E<VAR>Norm F<VAR>x : E × F<GOAL>‖x.1‖ ≤ ‖x‖
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Norm E<VAR>Norm F<VAR>x : E × F<GOAL>‖x.2‖ ≤ ‖x‖
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Norm E<VAR>Norm F<VAR>x : E × F<VAR>r : ℝ<GOAL>‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>x : E × F<GOAL>‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>x : E × F<GOAL>‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<GOAL>‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊)
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<GOAL>‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊)
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<GOAL>‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<GOAL>‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ≥0<GOAL>‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ≥0<GOAL>‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<VAR>r : ℝ<VAR>Nonempty ι<GOAL>‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<VAR>r : ℝ<VAR>Nonempty ι<GOAL>‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>x : (i : ι) → π i<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>‖f i‖ ≤ ‖f‖
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>‖f i‖ ≤ ‖f‖
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>‖f i‖₊ ≤ ‖f‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<GOAL>‖f i‖₊ ≤ ‖f‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖fun x => a‖ ≤ ‖a‖
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖fun x => a‖ ≤ ‖a‖
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖fun x => a‖₊ ≤ ‖a‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖fun x => a‖₊ ≤ ‖a‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedGroup E<VAR>Nonempty ι<VAR>a : E<GOAL>‖fun _i => a‖ = ‖a‖
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedAddGroup E<VAR>Nonempty ι<VAR>a : E<GOAL>‖fun _i => a‖ = ‖a‖
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedGroup E<VAR>Nonempty ι<VAR>a : E<GOAL>‖fun _i => a‖₊ = ‖a‖₊
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>SeminormedAddGroup E<VAR>Nonempty ι<VAR>a : E<GOAL>‖fun _i => a‖₊ = ‖a‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<GOAL>∑ i : ι, ‖f i‖ ≤ Fintype.card ι • ‖f‖
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<GOAL>∑ i : ι, ‖f i‖ ≤ Fintype.card ι • ‖f‖
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddGroup (π i)<VAR>f : (i : ι) → π i<GOAL>∑ i : ι, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedGroup (π i)<VAR>f : (i : ι) → π i<GOAL>∑ i : ι, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → NormedAddCommGroup (π i)<VAR>i : ι<VAR>y : π i<GOAL>‖Pi.single i y‖₊ = ‖y‖₊
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → NormedAddCommGroup (π i)<VAR>i : ι<VAR>y : π i<GOAL>‖Pi.single i y‖ = ‖y‖
<VAR>E : Type u_2<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖MulOpposite.op a‖ = ‖a‖
<VAR>E : Type u_2<VAR>SeminormedAddGroup E<VAR>a : Eᵐᵒᵖ<GOAL>‖MulOpposite.unop a‖ = ‖a‖
<VAR>E : Type u_2<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖MulOpposite.op a‖₊ = ‖a‖₊
<VAR>E : Type u_2<VAR>SeminormedAddGroup E<VAR>a : Eᵐᵒᵖ<GOAL>‖MulOpposite.unop a‖₊ = ‖a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>‖WeakDual.toNormedDual ↑φ‖ ≤ ‖1‖
<VAR>E : Type u_9<VAR>self : SeminormedAddGroup E<VAR>x y : E<GOAL>dist x y = ‖x - y‖
<VAR>E : Type u_9<VAR>self : SeminormedGroup E<VAR>x y : E<GOAL>dist x y = ‖x / y‖
<VAR>E : Type u_9<VAR>self : NormedAddGroup E<VAR>x y : E<GOAL>dist x y = ‖x - y‖
<VAR>E : Type u_9<VAR>self : NormedGroup E<VAR>x y : E<GOAL>dist x y = ‖x / y‖
<VAR>E : Type u_9<VAR>self : SeminormedAddCommGroup E<VAR>x y : E<GOAL>dist x y = ‖x - y‖
<VAR>E : Type u_9<VAR>self : SeminormedCommGroup E<VAR>x y : E<GOAL>dist x y = ‖x / y‖
<VAR>E : Type u_9<VAR>self : NormedAddCommGroup E<VAR>x y : E<GOAL>dist x y = ‖x - y‖
<VAR>E : Type u_9<VAR>self : NormedCommGroup E<VAR>x y : E<GOAL>dist x y = ‖x / y‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist a b = ‖a - b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist a b = ‖a / b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist a b = ‖b / a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist a b = ‖b - a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>r : ℝ<VAR>hpos : 0 < r<VAR>hr : ∀ (x : E), x ≠ 0 → r ≤ ‖x‖<GOAL>DiscreteTopology E
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>r : ℝ<VAR>hpos : 0 < r<VAR>hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖<GOAL>DiscreteTopology E
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>dist a 0 = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>dist a 1 = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>Inseparable a 0 ↔ ‖a‖ = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>Inseparable a 1 ↔ ‖a‖ = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>dist 1 = norm
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>dist 0 = norm
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a - b‖ = ‖b - a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a / b‖ = ‖b / a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖-a‖ = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖a⁻¹‖ = ‖a‖
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>dist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a + b‖ ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a * b‖ ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a₁ a₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : ‖a₁‖ ≤ r₁<VAR>h₂ : ‖a₂‖ ≤ r₂<GOAL>‖a₁ + a₂‖ ≤ r₁ + r₂
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a₁ a₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : ‖a₁‖ ≤ r₁<VAR>h₂ : ‖a₂‖ ≤ r₂<GOAL>‖a₁ * a₂‖ ≤ r₁ + r₂
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b c : E<GOAL>‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b c : E<GOAL>‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b c : E<GOAL>‖a - c‖ ≤ ‖a - b‖ + ‖b - c‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b c : E<GOAL>‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>0 ≤ ‖a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>0 ≤ ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>z : E<GOAL>|‖z‖| = ‖z‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>z : E<GOAL>|‖z‖| = ‖z‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>‖1‖ = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>‖0‖ = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖a‖ ≠ 0 → a ≠ 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖a‖ ≠ 0 → a ≠ 1
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>Subsingleton E<VAR>a : E<GOAL>‖a‖ = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>Subsingleton E<VAR>a : E<GOAL>‖a‖ = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>0 < 1 + ‖x‖ ^ 2
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>0 < 1 + ‖x‖ ^ 2
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a - b‖ ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a / b‖ ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a₁ a₂ : E<VAR>r₁ r₂ : ℝ<VAR>H₁ : ‖a₁‖ ≤ r₁<VAR>H₂ : ‖a₂‖ ≤ r₂<GOAL>‖a₁ / a₂‖ ≤ r₁ + r₂
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a₁ a₂ : E<VAR>r₁ r₂ : ℝ<VAR>H₁ : ‖a₁‖ ≤ r₁<VAR>H₂ : ‖a₂‖ ≤ r₂<GOAL>‖a₁ - a₂‖ ≤ r₁ + r₂