ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsClosed s<VAR>hs' : BddBelow s<GOAL>IsClosed ↑(upperClosure s)
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<GOAL>IsClosed ↑(lowerClosure s)
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsClopen s<VAR>hs' : BddBelow s<GOAL>IsClopen ↑(upperClosure s)
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsClopen s<VAR>hs' : BddAbove s<GOAL>IsClopen ↑(lowerClosure s)
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : BddBelow s<GOAL>closure ↑(upperClosure s) = ↑(upperClosure (closure s))
<VAR>ι : Type u_2<VAR>Finite ι<VAR>s : Set (ι → ℝ)<VAR>hs : BddAbove s<GOAL>closure ↑(lowerClosure s) = ↑(lowerClosure (closure s))
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>n : ℕ<GOAL>(∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>n : ℕ<VAR>hn : Even n<GOAL>(∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>m : ℤ<GOAL>(∑ i ∈ s, w i * z i) ^ m ≤ ∑ i ∈ s, w i * z i ^ m
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>n : ℕ<GOAL>(∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>w₁ w₂ z₁ z₂ : ℝ≥0<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>z₁ z₂ : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hab : a + b ≤ 1<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ 1
<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<GOAL>(a ^ p + b ^ p) ^ (1 / p) ≤ a + b
<VAR>p q : ℝ<VAR>a b : ℝ≥0<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ≥0∞<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>w₁ w₂ z₁ z₂ : ℝ≥0∞<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>z₁ z₂ : ℝ≥0∞<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<GOAL>(a ^ p + b ^ p) ^ (1 / p) ≤ a + b
<VAR>p q : ℝ<VAR>a b : ℝ≥0∞<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C<GOAL>∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤<GOAL>⨆ i, ↑‖g i‖₊ < ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' : NormedSpace.Dual 𝕜 E<GOAL>NormedSpace.Dual.toWeakDual x' = x'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' y' : NormedSpace.Dual 𝕜 E<GOAL>NormedSpace.Dual.toWeakDual x' = NormedSpace.Dual.toWeakDual y' ↔ x' = y'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>Continuous fun x' => NormedSpace.Dual.toWeakDual x'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : WeakDual 𝕜 E<VAR>y : E<GOAL>(WeakDual.toNormedDual x) y = x y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' : WeakDual 𝕜 E<GOAL>WeakDual.toNormedDual x' = x'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' y' : WeakDual 𝕜 E<GOAL>WeakDual.toNormedDual x' = WeakDual.toNormedDual y' ↔ x' = y'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' : NormedSpace.Dual 𝕜 E<VAR>r : ℝ<GOAL>IsClosed (⇑WeakDual.toNormedDual ⁻¹' Metric.closedBall x' r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>WeakDual.polar 𝕜 s = {f | ∀ x ∈ s, ‖f x‖ ≤ 1}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (WeakDual.polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set (WeakDual 𝕜 E)<VAR>hb : Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s)<VAR>hc : IsClosed s<GOAL>IsClosed (DFunLike.coe '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ProperSpace 𝕜<VAR>s : Set (WeakDual 𝕜 E)<VAR>hb : Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s)<VAR>hc : IsClosed s<GOAL>IsCompact s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<GOAL>IsClosed (DFunLike.coe '' WeakDual.polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<GOAL>IsClosed (DFunLike.coe '' NormedSpace.polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ProperSpace 𝕜<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<GOAL>IsCompact (WeakDual.polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ProperSpace 𝕜<VAR>x' : NormedSpace.Dual 𝕜 E<VAR>r : ℝ<GOAL>IsCompact (⇑WeakDual.toNormedDual ⁻¹' Metric.closedBall x' r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>f : E →L[𝕜] F<VAR>FiniteDimensional 𝕜 ↥(LinearMap.range f)<GOAL>(LinearMap.ker f).ClosedComplemented
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace E<VAR>CompleteSpace (F × G)<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<VAR>hf : LinearMap.range f = ⊤<VAR>hg : LinearMap.range g = ⊤<VAR>hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)<GOAL>↑↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = ↑(f.prod g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace E<VAR>CompleteSpace (F × G)<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<VAR>hf : LinearMap.range f = ⊤<VAR>hg : LinearMap.range g = ⊤<VAR>hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)<GOAL>(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg).toLinearEquiv = (↑f).equivProdOfSurjectiveOfIsCompl (↑g) hf hg hfg
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace E<VAR>CompleteSpace (F × G)<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<VAR>hf : LinearMap.range f = ⊤<VAR>hg : LinearMap.range g = ⊤<VAR>hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)<VAR>x : E<GOAL>(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>h : IsCompl p q<VAR>hp : IsClosed ↑p<VAR>hq : IsClosed ↑q<GOAL>⇑(Submodule.prodEquivOfClosedCompl p q h hp hq) = ⇑(Submodule.prodEquivOfIsCompl p q h)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>h : IsCompl p q<VAR>hp : IsClosed ↑p<VAR>hq : IsClosed ↑q<GOAL>⇑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm = ⇑(Submodule.prodEquivOfIsCompl p q h).symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>h : IsCompl p q<VAR>hp : IsClosed ↑p<VAR>hq : IsClosed ↑q<GOAL>↑(Submodule.linearProjOfClosedCompl p q h hp hq) = Submodule.linearProjOfIsCompl p q h
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>h : IsCompl p q<VAR>hp : IsClosed ↑p<VAR>hq : IsClosed ↑q<GOAL>⇑(Submodule.linearProjOfClosedCompl p q h hp hq) = ⇑(Submodule.linearProjOfIsCompl p q h)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>h : IsCompl p q<VAR>hp : IsClosed ↑p<VAR>hq : IsClosed ↑q<GOAL>Submodule.ClosedComplemented p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p : Subspace 𝕜 E<GOAL>Submodule.ClosedComplemented p ↔ IsClosed ↑p ∧ ∃ q, IsClosed ↑q ∧ IsCompl p q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>p : Subspace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 (E ⧸ p)<VAR>hp : IsClosed ↑p<GOAL>Submodule.ClosedComplemented p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>f : NormedSpace.Dual 𝕜 E<GOAL>((NormedSpace.inclusionInDoubleDual 𝕜 E) x) f = f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>‖NormedSpace.inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (NormedSpace.Dual 𝕜 E)‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>‖NormedSpace.inclusionInDoubleDual 𝕜 E‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>‖(NormedSpace.inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : NormedSpace.Dual 𝕜 E<VAR>x : E<GOAL>((NormedSpace.dualPairing 𝕜 E) v) x = v x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>(NormedSpace.dualPairing 𝕜 E).SeparatingLeft
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (f : NormedSpace.Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖<GOAL>‖x‖ ≤ M
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : ∀ (f : NormedSpace.Dual 𝕜 E), f x = 0<GOAL>x = 0
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>x = 0 ↔ ∀ (g : NormedSpace.Dual 𝕜 E), g x = 0
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x y : E<GOAL>x = y ↔ ∀ (g : NormedSpace.Dual 𝕜 E), g x = g y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x' : NormedSpace.Dual 𝕜 E<VAR>s : Set E<GOAL>x' ∈ NormedSpace.polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>NormedSpace.polar 𝕜 Set.univ = {0}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (NormedSpace.polar 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>NormedSpace.polar 𝕜 (closure s) = NormedSpace.polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x' : NormedSpace.Dual 𝕜 E<VAR>c : 𝕜<VAR>hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖<GOAL>c⁻¹ • x' ∈ NormedSpace.polar 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>NormedSpace.polar 𝕜 (Metric.ball 0 r) ⊆ Metric.closedBall 0 (‖c‖ / r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<GOAL>Metric.closedBall 0 r⁻¹ ⊆ NormedSpace.polar 𝕜 (Metric.closedBall 0 r)
<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>NormedSpace.polar 𝕜 (Metric.closedBall 0 r) = Metric.closedBall 0 r⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>s_nhd : s ∈ 𝓝 0<GOAL>Bornology.IsBounded (NormedSpace.polar 𝕜 s)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Finite α<VAR>f : (i : α) → E i<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Finite α<VAR>f : ↥(lp E p)<GOAL>Equiv.lpPiLp f = ↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Finite α<VAR>f : PiLp p E<GOAL>↑(Equiv.lpPiLp.symm f) = f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Finite α<VAR>f : ↥(lp E p)<GOAL>AddEquiv.lpPiLp f = ↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Finite α<VAR>f : PiLp p E<GOAL>↑(AddEquiv.lpPiLp.symm f) = f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Fintype α<VAR>f : ↥(lp E p)<GOAL>‖Equiv.lpPiLp f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Fintype α<VAR>𝕜 : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>(i : α) → NormedSpace 𝕜 (E i)<VAR>Fact (1 ≤ p)<VAR>f : ↥(lp E p)<GOAL>(lpPiLpₗᵢ E 𝕜) f = ↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>Fintype α<VAR>𝕜 : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>(i : α) → NormedSpace 𝕜 (E i)<VAR>Fact (1 ≤ p)<VAR>f : PiLp p E<GOAL>↑((lpPiLpₗᵢ E 𝕜).symm f) = f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NormedAddCommGroup E<VAR>f : ↥(lp (fun x => E) ⊤)<GOAL>⇑(AddEquiv.lpBCF f) = ↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NormedAddCommGroup E<VAR>f : BoundedContinuousFunction α E<GOAL>↑(AddEquiv.lpBCF.symm f) = ⇑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_5<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : ↥(lp (fun x => E) ⊤)<GOAL>⇑((lpBCFₗᵢ E 𝕜) f) = ↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_5<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : BoundedContinuousFunction α E<GOAL>↑((lpBCFₗᵢ E 𝕜).symm f) = ⇑f
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NonUnitalNormedRing R<VAR>f : ↥(lp (fun x => R) ⊤)<GOAL>⇑((RingEquiv.lpBCF R) f) = ↑f
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NonUnitalNormedRing R<VAR>f : BoundedContinuousFunction α R<GOAL>↑((RingEquiv.lpBCF R).symm f) = ⇑f
<VAR>α : Type u_1<VAR>A : Type u_4<VAR>𝕜 : Type u_5<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NormedRing A<VAR>NormOneClass A<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 A<VAR>f : ↥(lp (fun x => A) ⊤)<GOAL>⇑((AlgEquiv.lpBCF α A 𝕜) f) = ↑f
<VAR>α : Type u_1<VAR>A : Type u_4<VAR>𝕜 : Type u_5<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>NormedRing A<VAR>NormOneClass A<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 A<VAR>f : BoundedContinuousFunction α A<GOAL>↑((AlgEquiv.lpBCF α A 𝕜).symm f) = ⇑f
<VAR>𝕜 : Type u_6<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>self : NormedSpace 𝕜 E<VAR>a : 𝕜<VAR>b : E<GOAL>‖a • b‖ ≤ ‖a‖ * ‖b‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℤ<VAR>x : E<GOAL>‖n • x‖ = ‖↑n‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>ε : ℝ<VAR>h : 0 < ε<GOAL>∀ᶠ (y : E) in 𝓝 x, ‖c • (y - x)‖ < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>α : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : α → E<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l (𝓝 0)<VAR>hg : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g)<GOAL>Filter.Tendsto (fun x => f x • g x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>α : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : α → E<VAR>l : Filter α<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>hg : Filter.Tendsto g l (𝓝 0)<GOAL>Filter.Tendsto (fun x => f x • g x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<VAR>c : ℝ<GOAL>∃ x, c < ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<GOAL>¬Bornology.IsBounded Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<GOAL>(Bornology.cobounded E).NeBot
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>NormedField 𝕜<VAR>Infinite 𝕜<VAR>NormedAddCommGroup E<VAR>Nontrivial E<VAR>NormedSpace 𝕜 E<GOAL>NoncompactSpace E
<VAR>𝕜 : Type u_6<VAR>𝕜' : Type u_7<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>self : NormedAlgebra 𝕜 𝕜'<VAR>r : 𝕜<VAR>x : 𝕜'<GOAL>‖r • x‖ ≤ ‖r‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊ * ‖1‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊
<VAR>𝕜' : Type u_2<VAR>SeminormedRing 𝕜'<VAR>NormOneClass 𝕜'<VAR>NormedAlgebra ℝ 𝕜'<VAR>x : ℝ≥0<GOAL>‖(algebraMap ℝ≥0 𝕜') x‖ = ↑x
<VAR>𝕜' : Type u_2<VAR>SeminormedRing 𝕜'<VAR>NormOneClass 𝕜'<VAR>NormedAlgebra ℝ 𝕜'<VAR>x : ℝ≥0<GOAL>‖(algebraMap ℝ≥0 𝕜') x‖₊ = x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜<VAR>SeminormedRing 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormOneClass 𝕜'<GOAL>Isometry ⇑(algebraMap 𝕜 𝕜')
<VAR>𝕜 : Type u_6<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Norm E<VAR>Module 𝕜 E<VAR>self : SeminormedAddCommGroup.Core 𝕜 E<VAR>c : 𝕜<VAR>x : E<GOAL>‖c • x‖ = ‖c‖ * ‖x‖
<VAR>𝕜 : Type u_6<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Norm E<VAR>Module 𝕜 E<VAR>self : SeminormedAddCommGroup.Core 𝕜 E<VAR>x : E<GOAL>0 ≤ ‖x‖
<VAR>𝕜 : Type u_6<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Norm E<VAR>Module 𝕜 E<VAR>self : SeminormedAddCommGroup.Core 𝕜 E<VAR>x y : E<GOAL>‖x + y‖ ≤ ‖x‖ + ‖y‖
<VAR>𝕜 : Type u_6<VAR>E : Type u_7<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Norm E<VAR>self : NormedSpace.Core 𝕜 E<VAR>x : E<GOAL>‖x‖ = 0 ↔ x = 0
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>m : (i : Fin n.succ) → Ei i<GOAL>‖(f (m 0)) (Fin.tail m)‖ ≤ ‖f‖ * ∏ i : Fin n.succ, ‖m i‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (Fin.last n) →L[𝕜] G)<VAR>m : (i : Fin n.succ) → Ei i<GOAL>‖(f (Fin.init m)) (m (Fin.last n))‖ ≤ ‖f‖ * ∏ i : Fin n.succ, ‖m i‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>x : Ei 0<VAR>m : (i : Fin n) → Ei i.succ<GOAL>‖f (Fin.cons x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (Fin.last n)<GOAL>‖f (Fin.snoc m x)‖ ≤ (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>m : (i : Fin n.succ) → Ei i<GOAL>f.uncurryLeft m = (f (m 0)) (Fin.tail m)
<VAR>𝕜 : Type u<VAR>n : ℕ<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>(i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>x : Ei 0<VAR>m : (i : Fin n) → Ei i.succ<GOAL>(f.curryLeft x) m = f (Fin.cons x m)