ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → PseudoMetricSpace (β i)<VAR>x y : PiLp ⊤ β<GOAL>nndist x y = ⨆ i, nndist (x i) (y i)
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → PseudoEMetricSpace (β i)<GOAL>LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → PseudoEMetricSpace (β i)<GOAL>AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → PseudoEMetricSpace (β i)<GOAL>Isometry ⇑(WithLp.equiv ⊤ ((i : ι) → β i))
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>hp : p ≠ ⊤<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp p β<GOAL>‖f‖₊ = (∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal)
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp ⊤ β<GOAL>‖f‖₊ = ⨆ i, ‖f i‖₊
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp ⊤ β<GOAL>‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖₊ = ‖f‖₊
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : (i : ι) → β i<GOAL>‖(WithLp.equiv ⊤ ((i : ι) → β i)).symm f‖₊ = ‖f‖₊
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp ⊤ β<GOAL>‖(WithLp.equiv ⊤ ((i : ι) → β i)) f‖ = ‖f‖
<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>f : (i : ι) → β i<GOAL>‖(WithLp.equiv ⊤ ((i : ι) → β i)).symm f‖ = ‖f‖
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : PiLp p β<GOAL>‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖₊ = NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>dist x y = √(∑ i : ι, dist (x i) (y i) ^ 2)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>nndist x y = NNReal.sqrt (∑ i : ι, nndist (x i) (y i) ^ 2)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>β : ι → Type u_5<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>ι' : Type u_5<VAR>Fintype ι'<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>e : ι ≃ ι'<VAR>v : PiLp p fun x => E<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) v = (Equiv.piCongrLeft' (fun x => E) e) v
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>ι' : Type u_5<VAR>Fintype ι'<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>e : ι ≃ ι'<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm = LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>ι' : Type u_5<VAR>Fintype ι'<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>e : ι ≃ ι'<VAR>i : ι<VAR>v : E<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) = (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (α i)<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (α i)<VAR>(i : ι) → Module 𝕜 (β i)<VAR>e : (i : ι) → α i ≃ₗᵢ[𝕜] β i<VAR>x : PiLp p α<GOAL>(LinearIsometryEquiv.piLpCongrRight p e) x = (WithLp.equiv p ((i : ι) → β i)).symm fun i => (e i) (x i)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (α i)<VAR>(i : ι) → Module 𝕜 (α i)<GOAL>(LinearIsometryEquiv.piLpCongrRight p fun i => LinearIsometryEquiv.refl 𝕜 (α i)) = LinearIsometryEquiv.refl 𝕜 (PiLp p α)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (α i)<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (α i)<VAR>(i : ι) → Module 𝕜 (β i)<VAR>e : (i : ι) → α i ≃ₗᵢ[𝕜] β i<GOAL>(LinearIsometryEquiv.piLpCongrRight p e).symm = LinearIsometryEquiv.piLpCongrRight p fun i => (e i).symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (α i)<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (α i)<VAR>(i : ι) → Module 𝕜 (β i)<VAR>e : (i : ι) → α i ≃ₗᵢ[𝕜] β i<VAR>DecidableEq ι<VAR>i : ι<VAR>v : α i<GOAL>(LinearIsometryEquiv.piLpCongrRight p e) ((WithLp.equiv p ((i : ι) → α i)).symm (Pi.single i v)) = (WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i ((e i) v))
<VAR>𝕜 : Type u_1<VAR>Semiring 𝕜<VAR>ι : Type u_5<VAR>κ : ι → Type u_6<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → Fintype (κ i)<VAR>α : (i : ι) → κ i → Type u_7<VAR>(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)<VAR>(i : ι) → (k : κ i) → Module 𝕜 (α i k)<VAR>f : PiLp p fun i => α i.fst i.snd<GOAL>(LinearIsometryEquiv.piLpCurry 𝕜 p α) f = (WithLp.equiv p ((i : ι) → WithLp p ((y : κ i) → α i y))).symm fun i => (WithLp.equiv p ((y : κ i) → α i y)).symm (Sigma.curry ((WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)) f) i)
<VAR>𝕜 : Type u_1<VAR>Semiring 𝕜<VAR>ι : Type u_5<VAR>κ : ι → Type u_6<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → Fintype (κ i)<VAR>α : (i : ι) → κ i → Type u_7<VAR>(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)<VAR>(i : ι) → (k : κ i) → Module 𝕜 (α i k)<VAR>f : PiLp p fun i => PiLp p (α i)<GOAL>(LinearIsometryEquiv.piLpCurry 𝕜 p α).symm f = (WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)).symm (Sigma.uncurry fun i j => f i j)
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>DecidableEq ι<VAR>hp : Fact (1 ≤ p)<VAR>i : ι<VAR>b : β i<GOAL>‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b : β i<GOAL>‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖ = ‖b‖
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>nndist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = nndist b₁ b₂
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>dist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = dist b₁ b₂
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>DecidableEq ι<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>edist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = edist b₁ b₂
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>b : β<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>Nonempty ι<VAR>b : β<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>b : β<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>Nonempty ι<VAR>b : β<GOAL>‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>One β<GOAL>‖(WithLp.equiv p (ι → β)).symm 1‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖₊
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fact (1 ≤ p)<VAR>Fintype ι<VAR>β : Type u_5<VAR>SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>One β<GOAL>‖(WithLp.equiv p (ι → β)).symm 1‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (β i)<GOAL>⇑(PiLp.continuousLinearEquiv p 𝕜 β).symm = ⇑(WithLp.equiv p ((i : ι) → β i)).symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_4<VAR>Semiring 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (β i)<VAR>(i : ι) → Module 𝕜 (β i)<GOAL>⇑(PiLp.continuousLinearEquiv p 𝕜 β) = ⇑(WithLp.equiv p ((i : ι) → β i))
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Finite ι<VAR>Ring 𝕜<VAR>DecidableEq ι<VAR>i : ι<GOAL>(PiLp.basisFun p 𝕜 ι) i = (WithLp.equiv p (ι → 𝕜)).symm (Pi.single i 1)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Finite ι<VAR>Ring 𝕜<VAR>x : PiLp p fun x => 𝕜<VAR>i : ι<GOAL>((PiLp.basisFun p 𝕜 ι).repr x) i = x i
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Finite ι<VAR>Ring 𝕜<GOAL>(PiLp.basisFun p 𝕜 ι).equivFun = WithLp.linearEquiv p 𝕜 (ι → 𝕜)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Finite ι<VAR>Ring 𝕜<GOAL>PiLp.basisFun p 𝕜 ι = (Pi.basisFun 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>Finite ι<VAR>Ring 𝕜<GOAL>(PiLp.basisFun p 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) = Pi.basisFun 𝕜 ι
<VAR>p : ℝ≥0∞<VAR>ι : Type u_2<VAR>Fintype ι<VAR>𝕜 : Type u_5<VAR>SeminormedCommRing 𝕜<VAR>b : Basis ι 𝕜 (PiLp p fun x => 𝕜)<VAR>A : Matrix ι ι 𝕜<GOAL>b.toMatrix ⇑(PiLp.basisFun p 𝕜 ι) * A = Matrix.of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (A.transpose j))) i
<VAR>x : ℝ<GOAL>‖↑x‖ = |x|
<VAR>p : ℝ<VAR>x : ℝ<GOAL>‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
<VAR>p : ℝ<VAR>x : AddCircle p<VAR>hp : p ≠ 0<GOAL>‖x‖ ≤ |p| / 2
<VAR>p : ℝ<VAR>x : ℝ<VAR>hp : p ≠ 0<GOAL>‖↑x‖ = |x| ↔ |x| ≤ |p| / 2
<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>x : AddCircle p<VAR>ε : ℝ<VAR>hε : |p| / 2 ≤ ε<GOAL>Metric.closedBall x ε = Set.univ
<VAR>x ε : ℝ<GOAL>QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = Metric.closedBall x ε
<VAR>p x ε : ℝ<GOAL>QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = ⋃ z, Metric.closedBall (x + z • p) ε
<VAR>p : ℝ<VAR>x ε : ℝ<VAR>s : Set ℝ<VAR>hs : s ⊆ Metric.closedBall x (|p| / 2)<GOAL>QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε ∩ s = if ε < |p| / 2 then Metric.closedBall x ε ∩ s else s
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<GOAL>∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>SeminormedAddGroup E<VAR>SeminormedAddCommGroup F<VAR>FunLike 𝓕 E F<VAR>ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>f : 𝓕<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>SeminormedAddGroup E<VAR>SeminormedAddCommGroup F<VAR>ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<GOAL>Filter.Tendsto f (Filter.cocompact E) (𝓝 0)
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : AddGroupSeminorm G<GOAL>self.toFun 0 = 0
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : AddGroupSeminorm G<VAR>r : G<GOAL>self.toFun (-r) = self.toFun r
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : AddGroupSeminorm G<VAR>r s : G<GOAL>self.toFun (r + s) ≤ self.toFun r + self.toFun s
<VAR>G : Type u_7<VAR>Group G<VAR>self : GroupSeminorm G<VAR>x : G<GOAL>self.toFun x⁻¹ = self.toFun x
<VAR>G : Type u_7<VAR>Group G<VAR>self : GroupSeminorm G<VAR>x y : G<GOAL>self.toFun (x * y) ≤ self.toFun x + self.toFun y
<VAR>G : Type u_7<VAR>Group G<VAR>self : GroupSeminorm G<GOAL>self.toFun 1 = 0
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : NonarchAddGroupSeminorm G<VAR>r : G<GOAL>self.toFun (-r) = self.toFun r
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : NonarchAddGroupSeminorm G<VAR>r s : G<GOAL>self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : AddGroupNorm G<VAR>x : G<GOAL>self.toFun x = 0 → x = 0
<VAR>G : Type u_7<VAR>Group G<VAR>self : GroupNorm G<VAR>x : G<GOAL>self.toFun x = 0 → x = 1
<VAR>G : Type u_7<VAR>AddGroup G<VAR>self : NonarchAddGroupNorm G<VAR>x : G<GOAL>self.toFun x = 0 → x = 0
<VAR>F : Type u_7<VAR>α : outParam (Type u_8)<VAR>AddGroup α<VAR>FunLike F α ℝ<VAR>self : NonarchAddGroupSeminormClass F α<VAR>f : F<VAR>a : α<GOAL>f (-a) = f a
<VAR>F : Type u_7<VAR>α : outParam (Type u_8)<VAR>AddGroup α<VAR>FunLike F α ℝ<VAR>self : NonarchAddGroupSeminormClass F α<VAR>f : F<GOAL>f 0 = 0
<VAR>F : Type u_7<VAR>α : outParam (Type u_8)<VAR>AddGroup α<VAR>FunLike F α ℝ<VAR>self : NonarchAddGroupNormClass F α<VAR>f : F<VAR>a : α<GOAL>f a = 0 → a = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>FunLike F E ℝ<VAR>NonarchAddGroupSeminormClass F E<VAR>f : F<VAR>x y : E<GOAL>f (x - y) ≤ max (f x) (f y)
<VAR>E : Type u_4<VAR>Group E<VAR>p : GroupSeminorm E<GOAL>p.toFun = ⇑p
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p : AddGroupSeminorm E<GOAL>p.toFun = ⇑p
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>Group E<GOAL>⇑0 = 0
<VAR>E : Type u_4<VAR>AddGroup E<GOAL>⇑0 = 0
<VAR>E : Type u_4<VAR>Group E<VAR>x : E<GOAL>0 x = 0
<VAR>E : Type u_4<VAR>AddGroup E<VAR>x : E<GOAL>0 x = 0
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>⇑(p + q) = ⇑p + ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>⇑(p + q) = ⇑p + ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<VAR>x : E<GOAL>(p + q) x = p x + q x
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<VAR>x : E<GOAL>(p + q) x = p x + q x
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupSeminorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupSeminorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>p : AddGroupSeminorm E<VAR>f : F →+ E<GOAL>⇑(p.comp f) = ⇑p ∘ ⇑f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>p : GroupSeminorm E<VAR>f : F →* E<GOAL>⇑(p.comp f) = ⇑p ∘ ⇑f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>p : GroupSeminorm E<VAR>f : F →* E<VAR>x : F<GOAL>(p.comp f) x = p (f x)
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>p : AddGroupSeminorm E<VAR>f : F →+ E<VAR>x : F<GOAL>(p.comp f) x = p (f x)
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p : AddGroupSeminorm E<GOAL>p.comp (AddMonoidHom.id E) = p
<VAR>E : Type u_4<VAR>Group E<VAR>p : GroupSeminorm E<GOAL>p.comp (MonoidHom.id E) = p
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>p : AddGroupSeminorm E<GOAL>p.comp 0 = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>p : GroupSeminorm E<GOAL>p.comp 1 = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>f : F →* E<GOAL>GroupSeminorm.comp 0 f = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>f : F →+ E<GOAL>AddGroupSeminorm.comp 0 f = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>Group E<VAR>Group F<VAR>Group G<VAR>p : GroupSeminorm E<VAR>g : F →* E<VAR>f : G →* F<GOAL>p.comp (g.comp f) = (p.comp g).comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>AddGroup E<VAR>AddGroup F<VAR>AddGroup G<VAR>p : AddGroupSeminorm E<VAR>g : F →+ E<VAR>f : G →+ F<GOAL>p.comp (g.comp f) = (p.comp g).comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>p q : GroupSeminorm E<VAR>f : F →* E<GOAL>(p + q).comp f = p.comp f + q.comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>p q : AddGroupSeminorm E<VAR>f : F →+ E<GOAL>(p + q).comp f = p.comp f + q.comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddGroup E<VAR>AddGroup F<VAR>p q : AddGroupSeminorm E<VAR>f : F →+ E<VAR>hp : p ≤ q<GOAL>p.comp f ≤ q.comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>Group E<VAR>Group F<VAR>p q : GroupSeminorm E<VAR>f : F →* E<VAR>hp : p ≤ q<GOAL>p.comp f ≤ q.comp f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>p : AddGroupSeminorm E<VAR>f g : F →+ E<GOAL>p.comp (f + g) ≤ p.comp f + p.comp g
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>CommGroup E<VAR>CommGroup F<VAR>p : GroupSeminorm E<VAR>f g : F →* E<GOAL>p.comp (f * g) ≤ p.comp f + p.comp g
<VAR>E : Type u_4<VAR>CommGroup E<VAR>p q : GroupSeminorm E<VAR>x : E<GOAL>BddBelow (Set.range fun y => p y + q (x / y))
<VAR>E : Type u_4<VAR>AddCommGroup E<VAR>p q : AddGroupSeminorm E<VAR>x : E<GOAL>BddBelow (Set.range fun y => p y + q (x - y))
<VAR>E : Type u_4<VAR>AddCommGroup E<VAR>p q : AddGroupSeminorm E<VAR>x : E<GOAL>(p ⊓ q) x = ⨅ y, p y + q (x - y)
<VAR>E : Type u_4<VAR>CommGroup E<VAR>p q : GroupSeminorm E<VAR>x : E<GOAL>(p ⊓ q) x = ⨅ y, p y + q (x / y)
<VAR>E : Type u_4<VAR>AddGroup E<VAR>DecidableEq E<VAR>x : E<GOAL>1 x = if x = 0 then 0 else 1
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : AddGroupSeminorm E<GOAL>⇑(r • p) = r • ⇑p
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : AddGroupSeminorm E<VAR>x : E<GOAL>(r • p) x = r • p x
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : AddGroupSeminorm E<GOAL>r • (p ⊔ q) = r • p ⊔ r • q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p : NonarchAddGroupSeminorm E<GOAL>⇑p.toZeroHom = ⇑p
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupSeminorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>E : Type u_4<VAR>AddCommGroup E<VAR>p q : NonarchAddGroupSeminorm E<VAR>x : E<GOAL>BddBelow (Set.range fun y => p y + q (x - y))
<VAR>E : Type u_4<VAR>Group E<VAR>DecidableEq E<VAR>x : E<GOAL>1 x = if x = 1 then 0 else 1
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>Group E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : GroupSeminorm E<GOAL>⇑(r • p) = r • ⇑p
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>Group E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : GroupSeminorm E<VAR>x : E<GOAL>(r • p) x = r • p x
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>Group E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : GroupSeminorm E<GOAL>r • (p ⊔ q) = r • p ⊔ r • q
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : NonarchAddGroupSeminorm E<GOAL>⇑(r • p) = r • ⇑p
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p : NonarchAddGroupSeminorm E<VAR>x : E<GOAL>(r • p) x = r • p x
<VAR>R : Type u_2<VAR>E : Type u_4<VAR>AddGroup E<VAR>SMul R ℝ<VAR>SMul R ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : NonarchAddGroupSeminorm E<GOAL>r • (p ⊔ q) = r • p ⊔ r • q
<VAR>E : Type u_4<VAR>Group E<VAR>p : GroupNorm E<GOAL>⇑p.toGroupSeminorm = ⇑p
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p : AddGroupNorm E<GOAL>⇑p.toAddGroupSeminorm = ⇑p
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>⇑(p + q) = ⇑p + ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>⇑(p + q) = ⇑p + ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<VAR>x : E<GOAL>(p + q) x = p x + q x
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<VAR>x : E<GOAL>(p + q) x = p x + q x
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : AddGroupNorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>E : Type u_4<VAR>Group E<VAR>p q : GroupNorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p : NonarchAddGroupNorm E<GOAL>⇑p.toNonarchAddGroupSeminorm = ⇑p
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>(∀ (x : E), p x = q x) → p = q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>p ≤ q ↔ ⇑p ≤ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>p < q ↔ ⇑p < ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>⇑p ≤ ⇑q ↔ p ≤ q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>⇑p < ⇑q ↔ p < q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<GOAL>⇑(p ⊔ q) = ⇑p ⊔ ⇑q
<VAR>E : Type u_4<VAR>AddGroup E<VAR>p q : NonarchAddGroupNorm E<VAR>x : E<GOAL>(p ⊔ q) x = p x ⊔ q x
<VAR>V : outParam (Type u_1)<VAR>P : Type u_2<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>self : NormedAddTorsor V P<VAR>x y : P<GOAL>dist x y = ‖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 : P<GOAL>dist x y = ‖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 : P<GOAL>nndist x y = ‖x -ᵥ y‖₊