ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>NormedAddCommGroup V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>w : V<VAR>hw : w ≠ 0<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f (v + (fun w => (1 / (2 * ‖w‖ ^ 2)) • w) w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>NormedAddCommGroup V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : MeasureTheory.Integrable f MeasureTheory.volume<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v = (1 / 2) • ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • (f v - f (v + (fun w => (1 / (2 * ‖w‖ ^ 2)) • w) w))
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>NormedAddCommGroup V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<GOAL>Filter.Tendsto (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) (Filter.cocompact V) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>NormedAddCommGroup V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<GOAL>Filter.Tendsto (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) (Filter.cocompact V) (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<GOAL>Filter.Tendsto (fun w => ∫ (v : ℝ), 𝐞 (-(v * w)) • f v) (Filter.cocompact ℝ) (𝓝 0)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : ℝ → E<GOAL>Filter.Tendsto (𝓕 f) (Filter.cocompact ℝ) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>NormedAddCommGroup V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<GOAL>Filter.Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (Filter.cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalAddGroup V<VAR>T2Space V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>Module ℝ V<VAR>ContinuousSMul ℝ V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<GOAL>Filter.Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (Filter.cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : V → E<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalAddGroup V<VAR>T2Space V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>Module ℝ V<VAR>ContinuousSMul ℝ V<VAR>FiniteDimensional ℝ V<VAR>μ : MeasureTheory.Measure V<VAR>μ.IsAddHaarMeasure<GOAL>Filter.Tendsto (VectorFourier.fourierIntegral 𝐞 μ (topDualPairing ℝ V).flip f) (Filter.cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>NormedAddCommGroup G<VAR>CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Filter.Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>Filter.Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>ProperSpace F<VAR>f : 𝓕<VAR>FunLike 𝓕 E F<VAR>CocompactMapClass 𝓕 E F<VAR>ε : ℝ<GOAL>∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>Filter.Tendsto f (Filter.cocompact E) (Filter.cocompact F)
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>ProperSpace E<VAR>FunLike 𝓕 E F<VAR>ContinuousMapClass 𝓕 E F<VAR>h : ∀ (f : 𝓕) (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>CocompactMapClass 𝓕 E F
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>x : UniformSpace.Completion G<GOAL>f.completion x = UniformSpace.Completion.map (⇑f) x
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>⇑f.completion = UniformSpace.Completion.map ⇑f
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>g : G<GOAL>f.completion (↑G g) = ↑H (f g)
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>g : G<GOAL>UniformSpace.Completion.map (⇑f) (↑G g) = ↑H (f g)
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>normedAddGroupHomCompletionHom f = f.completion
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<GOAL>(NormedAddGroupHom.id G).completion = NormedAddGroupHom.id (UniformSpace.Completion G)
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>g : NormedAddGroupHom H K<GOAL>g.completion.comp f.completion = (g.comp f).completion
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>(-f).completion = -f.completion
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f g : NormedAddGroupHom G H<GOAL>(f + g).completion = f.completion + g.completion
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f g : NormedAddGroupHom G H<GOAL>(f - g).completion = f.completion - g.completion
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<GOAL>NormedAddGroupHom.completion 0 = 0
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<GOAL>∀ (a : G), NormedAddCommGroup.toCompl a = ↑G a
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>x : G<GOAL>‖NormedAddCommGroup.toCompl x‖ = ‖x‖
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<GOAL>DenseRange ⇑NormedAddCommGroup.toCompl
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>f.completion.comp NormedAddCommGroup.toCompl = NormedAddCommGroup.toCompl.comp f
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>‖f.completion‖ = ‖f‖
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<GOAL>(NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range ≤ f.completion.ker
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<GOAL>↑f.completion.ker = closure ↑(NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>T0Space H<VAR>CompleteSpace H<VAR>f : NormedAddGroupHom G H<VAR>v : G<GOAL>f.extension (↑G v) = UniformSpace.Completion.extension (⇑f) (↑G v)
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>T0Space H<VAR>CompleteSpace H<VAR>f : NormedAddGroupHom G H<VAR>v : G<GOAL>f.extension (↑G v) = f v
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>T0Space H<VAR>CompleteSpace H<VAR>f : NormedAddGroupHom G H<GOAL>⇑f.extension = UniformSpace.Completion.extension ⇑f
<VAR>G : Type u_1<VAR>SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>SeminormedAddCommGroup H<VAR>T0Space H<VAR>CompleteSpace H<VAR>f : NormedAddGroupHom G H<VAR>g : NormedAddGroupHom (UniformSpace.Completion G) H<VAR>hg : ∀ (v : G), f v = g (↑G v)<GOAL>f.extension = g
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (𝓝 a)<GOAL>CompleteSpace E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>u : ℕ → E<VAR>hu : Summable fun x => ‖u x‖<GOAL>∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (𝓝 a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<GOAL>(∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (𝓝 a)) ↔ CompleteSpace E
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>hi : Isometry f<VAR>h₁ : f 0 = 0<VAR>x : E<GOAL>‖f x‖ = ‖x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>hi : Isometry f<VAR>h₁ : f 1 = 1<VAR>x : E<GOAL>‖f x‖ = ‖x‖
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist b (a + b) = ‖a‖
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist b (a * b) = ‖a‖
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist (a + b) b = ‖a‖
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist (a * b) b = ‖a‖
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>a b c : E<GOAL>dist (a / b) c = dist a (c * b)
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>a b c : E<GOAL>dist (a - b) c = dist a (c + b)
<VAR>E : Type u_3<VAR>SeminormedGroup E<VAR>a b c : E<GOAL>dist a (b / c) = dist (a * c) b
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<VAR>a b c : E<GOAL>dist a (b - c) = dist (a + c) b
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>LipschitzWith C.toNNReal ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>LipschitzWith C.toNNReal ⇑f
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>s : Set E<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>s : Set E<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>s : Set E<VAR>a b : E<VAR>r : ℝ<VAR>f : E → F<VAR>C : ℝ≥0<VAR>h : LipschitzOnWith C f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hr : ‖a - b‖ ≤ r<GOAL>‖f a - f b‖ ≤ ↑C * r
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>s : Set E<VAR>a b : E<VAR>r : ℝ<VAR>f : E → F<VAR>C : ℝ≥0<VAR>h : LipschitzOnWith C f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hr : ‖a / b‖ ≤ r<GOAL>‖f a / f b‖ ≤ ↑C * r
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzWith C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>a b : E<VAR>r : ℝ<VAR>f : E → F<VAR>C : ℝ≥0<VAR>h : LipschitzWith C f<VAR>hr : ‖a / b‖ ≤ r<GOAL>‖f a / f b‖ ≤ ↑C * r
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>a b : E<VAR>r : ℝ<VAR>f : E → F<VAR>C : ℝ≥0<VAR>h : LipschitzWith C f<VAR>hr : ‖a - b‖ ≤ r<GOAL>‖f a - f b‖ ≤ ↑C * r
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>Continuous ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>Continuous ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>UniformContinuous ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<GOAL>UniformContinuous ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<GOAL>Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<GOAL>Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ≥0<VAR>h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊<GOAL>LipschitzWith C ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ≥0<VAR>h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊<GOAL>LipschitzWith C ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>AddMonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>K : ℝ≥0<VAR>h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖<GOAL>AntilipschitzWith K ⇑f
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>K : ℝ≥0<VAR>h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖<GOAL>AntilipschitzWith K ⇑f
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>hf : f 0 = 0<VAR>x : E<GOAL>‖f x‖ ≤ ↑K * ‖x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖f x‖ ≤ ↑K * ‖x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>hf : f 0 = 0<VAR>x : E<GOAL>‖f x‖₊ ≤ K * ‖x‖₊
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖f x‖₊ ≤ K * ‖x‖₊
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K f<VAR>hf : f 0 = 0<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K f<VAR>hf : f 0 = 0<VAR>x : E<GOAL>‖x‖₊ ≤ K * ‖f x‖₊
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K f<VAR>hf : f 1 = 1<VAR>x : E<GOAL>‖x‖₊ ≤ K * ‖f x‖₊
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>FunLike 𝓕 E F<VAR>ZeroHomClass 𝓕 E F<VAR>f : 𝓕<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K ⇑f<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>𝓕 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>FunLike 𝓕 E F<VAR>OneHomClass 𝓕 E F<VAR>f : 𝓕<VAR>K : ℝ≥0<VAR>h : AntilipschitzWith K ⇑f<VAR>x : E<GOAL>‖x‖ ≤ ↑K * ‖f x‖
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>hi : Isometry f<VAR>h₁ : f 0 = 0<VAR>x : E<GOAL>‖f x‖₊ = ‖x‖₊
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>hi : Isometry f<VAR>h₁ : f 1 = 1<VAR>x : E<GOAL>‖f x‖₊ = ‖x‖₊
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>LipschitzWith 1 norm
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>LipschitzWith 1 norm
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>LipschitzWith 1 nnnorm
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>LipschitzWith 1 nnnorm
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>UniformContinuous norm
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>UniformContinuous norm
<VAR>E : Type u_3<VAR>SeminormedGroup E<GOAL>UniformContinuous fun a => ‖a‖₊
<VAR>E : Type u_3<VAR>SeminormedAddGroup E<GOAL>UniformContinuous fun a => ‖a‖₊
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a b : E<GOAL>dist a (a * b) = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a b : E<GOAL>dist a (a + b) = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a b : E<GOAL>dist (a * b) a = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a b : E<GOAL>dist (a + b) a = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a b : E<GOAL>dist a (a / b) = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a b : E<GOAL>dist a (a - b) = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a b : E<GOAL>dist (a / b) a = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a b : E<GOAL>dist (a - b) a = ‖b‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ + a₂) (b₁ + b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : dist a₁ b₁ ≤ r₁<VAR>h₂ : dist a₂ b₂ ≤ r₂<GOAL>dist (a₁ + a₂) (b₁ + b₂) ≤ r₁ + r₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : dist a₁ b₁ ≤ r₁<VAR>h₂ : dist a₂ b₂ ≤ r₂<GOAL>dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ - a₂) (b₁ - b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : dist a₁ b₁ ≤ r₁<VAR>h₂ : dist a₂ b₂ ≤ r₂<GOAL>dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<VAR>r₁ r₂ : ℝ<VAR>h₁ : dist a₁ b₁ ≤ r₁<VAR>h₂ : dist a₂ b₂ ≤ r₂<GOAL>dist (a₁ - a₂) (b₁ - b₂) ≤ r₁ + r₂
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>|dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ + a₂) (b₁ + b₂)
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>|dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>nndist (a₁ + a₂) (b₁ + b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>a₁ a₂ b₁ b₂ : E<GOAL>edist (a₁ + a₂) (b₁ + b₂) ≤ edist a₁ b₁ + edist a₂ b₂
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<GOAL>LipschitzWith K f⁻¹ ↔ LipschitzWith K f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<GOAL>LipschitzWith K (-f) ↔ LipschitzWith K f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<GOAL>AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<GOAL>AntilipschitzWith K (-f) ↔ AntilipschitzWith K f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<VAR>s : Set α<GOAL>LipschitzOnWith K (-f) s ↔ LipschitzOnWith K f s
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → E<VAR>s : Set α<GOAL>LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>f : α → E<GOAL>LocallyLipschitz (-f) ↔ LocallyLipschitz f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>f : α → E<GOAL>LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) fun x => f x + g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) fun x => f x * g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) fun x => f x / g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) fun x => f x - g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x + g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg (g - f)<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>PseudoEMetricSpace α<VAR>Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg (g / f)<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
<VAR>F : Type u_4<VAR>SeminormedAddCommGroup F<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>K : ℝ≥0<VAR>f : E → F<VAR>hf : AntilipschitzWith K f<VAR>x y : E<GOAL>‖x - y‖ ≤ ↑K * ‖f x - f y‖
<VAR>F : Type u_4<VAR>SeminormedCommGroup F<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>K : ℝ≥0<VAR>f : E → F<VAR>hf : AntilipschitzWith K f<VAR>x y : E<GOAL>‖x / y‖ ≤ ↑K * ‖f x / f y‖
<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), v k<GOAL>CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
<VAR>E : Type u_3<VAR>SeminormedCommGroup E<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), v k<GOAL>CauchySeq fun n => ∏ k ∈ Finset.range (n + 1), u k
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>x : E<GOAL>‖↑E x‖ = ‖x‖
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>x : E<GOAL>‖↑E x‖₊ = ‖x‖₊
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f f' : α → E<VAR>s : Set α<VAR>h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0<GOAL>eVariationOn f s = eVariationOn f' s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f f' : α → E<VAR>s : Set α<VAR>h : Set.EqOn f f' s<GOAL>eVariationOn f s = eVariationOn f' s