ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>m n : ℕ<VAR>u : ℕ → α<VAR>hu : MonotoneOn u (Set.Icc m n)<VAR>us : ∀ i ∈ Set.Icc m n, u i ∈ s<GOAL>∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : MonotoneOn u (Set.Iic n)<VAR>us : ∀ i ≤ n, u i ∈ s<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>hst : t ⊆ s<GOAL>eVariationOn f t ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>t : Set α<VAR>ht : t ⊆ s<GOAL>BoundedVariationOn f t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn f s<GOAL>LocallyBoundedVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>edist (f x) (f y) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<GOAL>eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : (f '' s).Subsingleton<GOAL>eVariationOn f s = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>eVariationOn f s = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>ι : Type u_3<VAR>F : ι → α → E<VAR>p : Filter ι<VAR>f : α → E<VAR>s : Set α<VAR>Ffs : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) p (𝓝 (f x))<VAR>v : ℝ≥0∞<VAR>hv : v < eVariationOn f s<GOAL>∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>s : Set α<GOAL>LowerSemicontinuous fun f => eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_3<VAR>PseudoMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist (f x) (f y) ≤ (eVariationOn f s).toReal
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x - f y ≤ (eVariationOn f s).toReal
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Set.Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y<GOAL>eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>x : α<VAR>hs : IsGreatest s x<VAR>ht : IsLeast t x<GOAL>eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<VAR>hb : b ∈ s<GOAL>eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>φst : Set.MapsTo φ t s<GOAL>eVariationOn (f ∘ φ) t ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : Set.MapsTo φ t s<GOAL>eVariationOn (f ∘ φ) t ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<GOAL>eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<GOAL>eVariationOn (f ∘ φ) (t ∩ Set.Icc x y) = eVariationOn f (φ '' t ∩ Set.Icc (φ x) (φ y))
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<GOAL>eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<GOAL>eVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) = eVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>a b : α<VAR>as : a ∈ s<VAR>bs : b ∈ s<GOAL>eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (f b - f a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : MonotoneOn f s<GOAL>LocallyBoundedVariationOn f s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a : α<GOAL>variationOnFromTo f s a a = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : a ≤ b<GOAL>0 ≤ variationOnFromTo f s a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<GOAL>variationOnFromTo f s a b = -variationOnFromTo f s b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : b ≤ a<GOAL>variationOnFromTo f s a b ≤ 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : a ≤ b<GOAL>variationOnFromTo f s a b = (eVariationOn f (s ∩ Set.Icc a b)).toReal
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : b ≤ a<GOAL>variationOnFromTo f s a b = -(eVariationOn f (s ∩ Set.Icc b a)).toReal
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b c : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hc : c ∈ s<GOAL>variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : variationOnFromTo f s a b = 0<GOAL>edist (f a) (f b) = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b c : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hc : c ∈ s<GOAL>variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ab : a ≤ b<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc a b → edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ba : b ≤ a<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc b a → edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.uIcc a b → edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<GOAL>MonotoneOn (variationOnFromTo f s a) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>b : α<VAR>bs : b ∈ s<GOAL>AntitoneOn (fun a => variationOnFromTo f s a b) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<GOAL>MonotoneOn (variationOnFromTo f s a - f) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>β : Type u_3<VAR>LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>x y : β<VAR>hx : x ∈ t<VAR>hy : y ∈ t<GOAL>variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : LocallyBoundedVariationOn f s<GOAL>∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>F : Type u_3<VAR>PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>h : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : Set.MapsTo g s t<GOAL>eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>F : Type u_3<VAR>PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>hf : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : Set.MapsTo g s t<VAR>h : BoundedVariationOn g s<GOAL>BoundedVariationOn (f ∘ g) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>F : Type u_3<VAR>PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>hf : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : Set.MapsTo g s t<VAR>h : LocallyBoundedVariationOn g s<GOAL>LocallyBoundedVariationOn (f ∘ g) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>F : Type u_3<VAR>PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>hf : LipschitzWith C f<VAR>g : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn g s<GOAL>BoundedVariationOn (f ∘ g) s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>F : Type u_3<VAR>PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>hf : LipschitzWith C f<VAR>g : α → E<VAR>s : Set α<VAR>h : LocallyBoundedVariationOn g s<GOAL>LocallyBoundedVariationOn (f ∘ g) s
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>C : ℝ≥0<VAR>s : Set ℝ<VAR>hf : LipschitzOnWith C f s<GOAL>LocallyBoundedVariationOn f s
<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>C : ℝ≥0<VAR>hf : LipschitzWith C f<VAR>s : Set ℝ<GOAL>LocallyBoundedVariationOn f s
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>ι : Type u_4<VAR>Fintype ι<VAR>f : ℝ → ι → ℝ<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LocallyBoundedVariationOn f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>h : LocallyBoundedVariationOn f Set.univ<GOAL>∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>C : ℝ≥0<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LipschitzOnWith C f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>C : ℝ≥0<VAR>f : ℝ → V<VAR>s : Set ℝ<VAR>h : LipschitzOnWith C f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>C : ℝ≥0<VAR>f : ℝ → V<VAR>h : LipschitzWith C f<GOAL>∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
<VAR>V : SemiNormedGrp<GOAL>SemiNormedGrp.completion.obj V = SemiNormedGrp.of (UniformSpace.Completion ↑V)
<GOAL>∀ {X Y : SemiNormedGrp} (f : X ⟶ Y), SemiNormedGrp.completion.map f = NormedAddGroupHom.completion f
<VAR>V : SemiNormedGrp<VAR>v : ↑V<GOAL>SemiNormedGrp.completion.incl v = ↑↑V v
<VAR>V : SemiNormedGrp<VAR>v : ↑V<GOAL>‖SemiNormedGrp.completion.incl v‖ = ‖v‖
<VAR>V W : SemiNormedGrp<VAR>f : V ⟶ W<VAR>hf : NormedAddGroupHom.NormNoninc f<GOAL>NormedAddGroupHom.NormNoninc (SemiNormedGrp.completion.map f)
<VAR>V W : SemiNormedGrp<GOAL>SemiNormedGrp.completion.map 0 = 0
<VAR>V W : SemiNormedGrp<VAR>CompleteSpace ↑W<VAR>T0Space ↑W<VAR>f : V ⟶ W<GOAL>SemiNormedGrp.completion.incl ≫ SemiNormedGrp.completion.lift f = f
<VAR>V W : SemiNormedGrp<VAR>CompleteSpace ↑W<VAR>T0Space ↑W<VAR>f : V ⟶ W<VAR>g : SemiNormedGrp.completion.obj V ⟶ W<GOAL>SemiNormedGrp.completion.incl ≫ g = f → g = SemiNormedGrp.completion.lift f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>Ring 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>s : Submodule 𝕜 E<VAR>x : ↥s<GOAL>‖x‖ = ‖↑x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>Ring 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>s : Submodule 𝕜 E<VAR>x : ↥s<GOAL>‖↑x‖ = ‖x‖
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<GOAL>(CauchySeq fun s => ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<GOAL>Summable f ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ι) in Filter.cofinite, ‖f i‖ ≤ g i<GOAL>CauchySeq fun s => ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>CauchySeq fun s => ∑ i ∈ s, f i
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg : CauchySeq fun n => ∑ i ∈ Finset.range n, g i<VAR>hf : ∀ (i : ℕ), ‖f i‖ ≤ g i<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, f i
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>hf : Summable fun a => ‖f a‖<GOAL>CauchySeq fun s => ∑ a ∈ s, f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>hf : Summable fun a => ‖f a‖<VAR>s : α → Finset ι<VAR>p : Filter α<VAR>p.NeBot<VAR>hs : Filter.Tendsto s p Filter.atTop<VAR>a : E<VAR>ha : Filter.Tendsto (fun b => ∑ i ∈ s b, f i) p (𝓝 a)<GOAL>HasSum f a
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ℕ → E<VAR>a : E<VAR>hf : Summable fun i => ‖f i‖<GOAL>HasSum f a ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 a)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>a : E<VAR>b : ℝ<VAR>hf : HasSum f a<VAR>hg : HasSum g b<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>‖a‖ ≤ b
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>a : ℝ<VAR>hg : HasSum g a<VAR>h : ∀ (i : ι), ‖f i‖ ≤ g i<GOAL>‖∑' (i : ι), f i‖ ≤ a
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>hf : Summable fun i => ‖f i‖<GOAL>‖∑' (i : ι), f i‖ ≤ ∑' (i : ι), ‖f i‖
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>g : ι → ℝ≥0<VAR>a : ℝ≥0<VAR>hg : HasSum g a<VAR>h : ∀ (i : ι), ‖f i‖₊ ≤ g i<GOAL>‖∑' (i : ι), f i‖₊ ≤ a
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>f : ι → E<VAR>hf : Summable fun i => ‖f i‖₊<GOAL>‖∑' (i : ι), f i‖₊ ≤ ∑' (i : ι), ‖f i‖₊
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ι) in Filter.cofinite, ‖f i‖ ≤ g i<GOAL>Summable f
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg : Summable g<VAR>h : ∀ᶠ (i : ℕ) in Filter.atTop, ‖f i‖ ≤ g i<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ≥0<VAR>hg : Summable g<VAR>h : ∀ (i : ι), ‖f i‖₊ ≤ g i<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>hf : Summable fun a => ‖f a‖<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>hf : Summable fun a => ‖f a‖₊<GOAL>Summable f
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>‖x‖ = sInf (norm '' {m | ↑m = x})
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>‖x‖ = Metric.infDist 0 {m | ↑m = x}
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M<GOAL>‖↑x‖ = Metric.infDist x ↑S
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>(norm '' {m | (QuotientAddGroup.mk' S) m = x}).Nonempty
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>s : Set M<GOAL>BddBelow (norm '' s)
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>IsGLB (norm '' {m | (QuotientAddGroup.mk' S) m = x}) ‖x‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>‖-x‖ = ‖x‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x y : M ⧸ S<GOAL>‖x - y‖ = ‖y - x‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖(QuotientAddGroup.mk' S) m‖ ≤ ‖m‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖↑m‖ ≤ ‖m‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖(QuotientAddGroup.mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>0 ≤ ‖x‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>0 ≤ ‖(QuotientAddGroup.mk' S) m‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖(QuotientAddGroup.mk' S) m‖ = 0 ↔ m ∈ closure ↑S
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<VAR>r : ℝ<GOAL>‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ m, (QuotientAddGroup.mk' S) m = x ∧ ‖m‖ < ‖x‖ + ε
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ s ∈ S, ‖m + s‖ < ‖(QuotientAddGroup.mk' S) m‖ + ε
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>x y : M ⧸ S<GOAL>‖x + y‖ ≤ ‖x‖ + ‖y‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>‖0‖ = 0
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>hS : IsClosed ↑S<VAR>m : M<VAR>h : ‖(QuotientAddGroup.mk' S) m‖ = 0<GOAL>m ∈ S
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>m : M<GOAL>S.normedMk m = (QuotientAddGroup.mk' S) m
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>Function.Surjective ⇑S.normedMk
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>S.normedMk.ker = S
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>‖S.normedMk‖ ≤ 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ x ∈ S, f x = 0<VAR>x : M ⧸ S<GOAL>‖(QuotientAddGroup.lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure ≠ Set.univ<GOAL>‖S.normedMk‖ = 1
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure = Set.univ<GOAL>‖S.normedMk‖ = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>self : f.IsQuotient<GOAL>Function.Surjective ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>self : f.IsQuotient<VAR>x : M<GOAL>‖f x‖ = sInf ((fun m => ‖x + m‖) '' ↑f.ker)
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>N : Type u_3<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>m : M<GOAL>(NormedAddGroupHom.lift S f hf) (S.normedMk m) = f m
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>N : Type u_3<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>g : NormedAddGroupHom (M ⧸ S) N<VAR>h : g.comp S.normedMk = f<GOAL>g = NormedAddGroupHom.lift S f hf
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>S : AddSubgroup M<GOAL>S.normedMk.IsQuotient
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>n : N<GOAL>∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>SeminormedAddCommGroup M<VAR>SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>m : M<GOAL>‖f m‖ ≤ ‖m‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>N : Type u_3<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<GOAL>‖NormedAddGroupHom.lift S f hf‖ ≤ ‖f‖
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>N : Type u_3<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>c : ℝ≥0<VAR>fb : ‖f‖ ≤ ↑c<GOAL>‖NormedAddGroupHom.lift S f hf‖ ≤ ↑c
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>N : Type u_3<VAR>SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>f : NormedAddGroupHom M N<VAR>hf : ∀ s ∈ S, f s = 0<VAR>fb : f.NormNoninc<GOAL>(NormedAddGroupHom.lift S f hf).NormNoninc
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>R : Type u_3<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>x : M ⧸ S<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ m, Submodule.Quotient.mk m = x ∧ ‖m‖ < ‖x‖ + ε
<VAR>M : Type u_1<VAR>SeminormedAddCommGroup M<VAR>R : Type u_3<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>m : M<GOAL>‖Submodule.Quotient.mk m‖ ≤ ‖m‖
<VAR>R : Type u_3<VAR>SeminormedCommRing R<VAR>I : Ideal R<VAR>x : R ⧸ I<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ r, (Ideal.Quotient.mk I) r = x ∧ ‖r‖ < ‖x‖ + ε
<VAR>R : Type u_3<VAR>SeminormedCommRing R<VAR>I : Ideal R<VAR>r : R<GOAL>‖(Ideal.Quotient.mk I) r‖ ≤ ‖r‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_5<VAR>ι : Type u_8<VAR>NormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<GOAL>U ∈ p.basisSets ↔ ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r