ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_6<VAR>F : Type u_7<VAR>SeminormedCommGroup E<VAR>SeminormedCommGroup F<VAR>j : E →* F<VAR>b : F<VAR>hb : b ∈ closure ↑j.range<VAR>f : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < f n<GOAL>∃ a, Filter.Tendsto (fun n => ∏ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (𝓝 b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>m : Multiset E<GOAL>‖m.sum‖₊ ≤ (Multiset.map (fun x => ‖x‖₊) m).sum
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>m : Multiset E<GOAL>‖m.prod‖₊ ≤ (Multiset.map (fun x => ‖x‖₊) m).sum
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<VAR>n : ι → ℝ≥0<VAR>h : ∀ b ∈ s, ‖f b‖₊ ≤ n b<GOAL>‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<VAR>n : ι → ℝ≥0<VAR>h : ∀ b ∈ s, ‖f b‖₊ ≤ n b<GOAL>‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b
<VAR>r : ℝ<GOAL>‖r‖ = |r|
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖r‖ = r
<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>‖r‖ = -r
<VAR>r : ℝ<GOAL>r ≤ ‖r‖
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖r‖₊ = ⟨r, hr⟩
<VAR>r : ℝ<GOAL>‖|r|‖₊ = ‖r‖₊
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>↑‖r‖₊ = ENNReal.ofReal r
<VAR>r : ℝ<GOAL>↑‖r‖₊ = ENNReal.ofReal |r|
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>r.toNNReal = ‖r‖₊
<VAR>r : ℝ<GOAL>ENNReal.ofReal r ≤ ↑‖r‖₊
<VAR>x : ℝ≥0<GOAL>‖x‖₊ = x
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>‖a‖ = 0 ↔ a = 0
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>‖a‖ = 0 ↔ a = 1
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>‖a‖ ≠ 0 ↔ a ≠ 1
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>‖a‖ ≠ 0 ↔ a ≠ 0
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>0 < ‖a‖ ↔ a ≠ 0
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>0 < ‖a‖ ↔ a ≠ 1
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>‖a‖ ≤ 0 ↔ a = 0
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>‖a‖ ≤ 0 ↔ a = 1
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a b : E<GOAL>‖a / b‖ = 0 ↔ a = b
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a b : E<GOAL>‖a - b‖ = 0 ↔ a = b
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a b : E<GOAL>0 < ‖a / b‖ ↔ a ≠ b
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a b : E<GOAL>0 < ‖a - b‖ ↔ a ≠ b
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a b : E<VAR>h : ‖a / b‖ ≤ 0<GOAL>a = b
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a b : E<VAR>h : ‖a - b‖ ≤ 0<GOAL>a = b
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>‖a‖₊ = 0 ↔ a = 1
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>‖a‖₊ = 0 ↔ a = 0
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>‖a‖₊ ≠ 0 ↔ a ≠ 0
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>‖a‖₊ ≠ 0 ↔ a ≠ 1
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>0 < ‖a‖₊ ↔ a ≠ 0
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>0 < ‖a‖₊ ↔ a ≠ 1
<VAR>E : Type u_6<VAR>NormedGroup E<VAR>a : E<GOAL>Filter.Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)
<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>a : E<GOAL>Filter.Tendsto (fun x => ‖x - a‖) (𝓝[≠] a) (𝓝[>] 0)
<VAR>E : Type u_6<VAR>NormedAddGroup E<GOAL>Filter.Tendsto norm (𝓝[≠] 0) (𝓝[>] 0)
<VAR>E : Type u_6<VAR>NormedGroup E<GOAL>Filter.Tendsto norm (𝓝[≠] 1) (𝓝[>] 0)
<VAR>E : Type u_6<VAR>NormedGroup E<GOAL>⇑(normGroupNorm E) = norm
<VAR>E : Type u_6<VAR>NormedGroup E<GOAL>Filter.comap norm (𝓝[>] 0) = 𝓝[≠] 1
<VAR>E : Type u_6<VAR>NormedAddGroup E<GOAL>Filter.comap norm (𝓝[>] 0) = 𝓝[≠] 0
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>NormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>(HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s : Subgroup E<VAR>x : ↥s<GOAL>‖x‖ = ‖↑x‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s : AddSubgroup E<VAR>x : ↥s<GOAL>‖x‖ = ‖↑x‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s : Subgroup E<VAR>x : ↥s<GOAL>‖↑x‖ = ‖x‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s : AddSubgroup E<VAR>x : ↥s<GOAL>‖↑x‖ = ‖x‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>S : Type u_9<VAR>SetLike S E<VAR>AddSubgroupClass S E<VAR>s : S<VAR>x : ↥s<GOAL>‖x‖ = ‖↑x‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>S : Type u_9<VAR>SetLike S E<VAR>SubgroupClass S E<VAR>s : S<VAR>x : ↥s<GOAL>‖x‖ = ‖↑x‖
<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>CompleteSpace G<VAR>H : Type u_2<VAR>NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : AddSubgroup H<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : f.SurjectiveOnWith K C<GOAL>f.SurjectiveOnWith K.topologicalClosure (C + ε)
<VAR>G : Type u_1<VAR>NormedAddCommGroup G<VAR>CompleteSpace G<VAR>H : Type u_2<VAR>NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : Type u_3<VAR>SeminormedAddCommGroup K<VAR>j : NormedAddGroupHom K H<VAR>hj : ∀ (x : K), ‖j x‖ = ‖x‖<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : ∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖<GOAL>f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
<VAR>E : Type u_1<VAR>SeminormedGroup E<VAR>s t : Set E<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s * t)
<VAR>E : Type u_1<VAR>SeminormedAddGroup E<VAR>s t : Set E<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s + t)
<VAR>E : Type u_1<VAR>SeminormedAddGroup E<VAR>s t : Set E<VAR>hst : Bornology.IsBounded (s + t)<GOAL>Bornology.IsBounded s ∨ Bornology.IsBounded t
<VAR>E : Type u_1<VAR>SeminormedGroup E<VAR>s t : Set E<VAR>hst : Bornology.IsBounded (s * t)<GOAL>Bornology.IsBounded s ∨ Bornology.IsBounded t
<VAR>E : Type u_1<VAR>SeminormedAddGroup E<VAR>s : Set E<GOAL>Bornology.IsBounded s → Bornology.IsBounded (-s)
<VAR>E : Type u_1<VAR>SeminormedGroup E<VAR>s : Set E<GOAL>Bornology.IsBounded s → Bornology.IsBounded s⁻¹
<VAR>E : Type u_1<VAR>SeminormedGroup E<VAR>s t : Set E<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s / t)
<VAR>E : Type u_1<VAR>SeminormedAddGroup E<VAR>s t : Set E<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s - t)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>x : E<VAR>s : Set E<GOAL>EMetric.infEdist (-x) (-s) = EMetric.infEdist x s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>x : E<VAR>s : Set E<GOAL>EMetric.infEdist x⁻¹ s⁻¹ = EMetric.infEdist x s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>x : E<VAR>s : Set E<GOAL>EMetric.infEdist (-x) s = EMetric.infEdist x (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>x : E<VAR>s : Set E<GOAL>EMetric.infEdist x⁻¹ s = EMetric.infEdist x s⁻¹
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>x y : Set E<GOAL>EMetric.diam (x * y) ≤ EMetric.diam x + EMetric.diam y
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>x y : Set E<GOAL>EMetric.diam (x + y) ≤ EMetric.diam x + EMetric.diam y
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>-Metric.thickening δ s = Metric.thickening δ (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>(Metric.thickening δ s)⁻¹ = Metric.thickening δ s⁻¹
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>-Metric.cthickening δ s = Metric.cthickening δ (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>(Metric.cthickening δ s)⁻¹ = Metric.cthickening δ s⁻¹
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>(Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>-Metric.ball x δ = Metric.ball (-x) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>-Metric.closedBall x δ = Metric.closedBall (-x) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>(Metric.closedBall x δ)⁻¹ = Metric.closedBall x⁻¹ δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} + Metric.ball y δ = Metric.ball (x + y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} * Metric.ball y δ = Metric.ball (x * y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} - Metric.ball y δ = Metric.ball (x - y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} / Metric.ball y δ = Metric.ball (x / y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.ball x δ + {y} = Metric.ball (x + y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.ball x δ * {y} = Metric.ball (x * y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.ball x δ / {y} = Metric.ball (x / y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.ball x δ - {y} = Metric.ball (x - y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} + Metric.ball 0 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} * Metric.ball 1 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} / Metric.ball 1 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} - Metric.ball 0 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.ball 1 δ * {x} = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.ball 0 δ + {x} = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.ball 0 δ - {x} = Metric.ball (-x) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.ball 1 δ / {x} = Metric.ball x⁻¹ δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>x +ᵥ Metric.ball 0 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>x • Metric.ball 1 δ = Metric.ball x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} * Metric.closedBall y δ = Metric.closedBall (x * y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>{x} / Metric.closedBall y δ = Metric.closedBall (x / y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x y : E<GOAL>Metric.closedBall x δ - {y} = Metric.closedBall (x - y) δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} + Metric.closedBall 0 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} * Metric.closedBall 1 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} - Metric.closedBall 0 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>{x} / Metric.closedBall 1 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.closedBall 0 δ + {x} = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.closedBall 1 δ * {x} = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.closedBall 0 δ - {x} = Metric.closedBall (-x) δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>Metric.closedBall 1 δ / {x} = Metric.closedBall x⁻¹ δ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>x +ᵥ Metric.closedBall 0 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>x : E<GOAL>x • Metric.closedBall 1 δ = Metric.closedBall x δ
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>s * Metric.ball 1 δ = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>s + Metric.ball 0 δ = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>s / Metric.ball 1 δ = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>s - Metric.ball 0 δ = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>Metric.ball 1 δ * s = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>Metric.ball 0 δ + s = Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>Metric.ball 0 δ - s = Metric.thickening δ (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<GOAL>Metric.ball 1 δ / s = Metric.thickening δ s⁻¹
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>s * Metric.ball x δ = x • Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>s + Metric.ball x δ = x +ᵥ Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>s / Metric.ball x δ = x⁻¹ • Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>s - Metric.ball x δ = -x +ᵥ Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>Metric.ball x δ + s = x +ᵥ Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>Metric.ball x δ * s = x • Metric.thickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>Metric.ball x δ / s = x • Metric.thickening δ s⁻¹
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s * Metric.closedBall 1 δ = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s + Metric.closedBall 0 δ = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s / Metric.closedBall 1 δ = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s - Metric.closedBall 0 δ = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>Metric.closedBall 1 δ * s = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>Metric.closedBall 0 δ + s = Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>Metric.closedBall 1 δ / s = Metric.cthickening δ s⁻¹
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>Metric.closedBall 0 δ - s = Metric.cthickening δ (-s)
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s * Metric.closedBall x δ = x • Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s + Metric.closedBall x δ = x +ᵥ Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s - Metric.closedBall x δ = -x +ᵥ Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s / Metric.closedBall x δ = x⁻¹ • Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
<VAR>E : Type u_1<VAR>SeminormedCommGroup E<VAR>δ : ℝ<VAR>s : Set E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>Metric.closedBall x δ * s = x • Metric.cthickening δ s
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>self : NormedAddGroupHom V W<GOAL>∃ C, ∀ (v : V), ‖self.toFun v‖ ≤ C * ‖v‖
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>self : NormedAddGroupHom V W<VAR>v₁ v₂ : V<GOAL>self.toFun (v₁ + v₂) = self.toFun v₁ + self.toFun v₂
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f : V → W<VAR>M : ℝ<VAR>h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖<GOAL>∃ N, 0 < N ∧ ∀ (x : V), ‖f x‖ ≤ N * ‖x‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>H : ⇑f = ⇑g<GOAL>f = g
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>Function.Injective NormedAddGroupHom.toFun
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>f = g ↔ ⇑f = ⇑g
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>H : ∀ (x : V₁), f x = g x<GOAL>f = g
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>f = g ↔ ∀ (x : V₁), f x = g x
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>f.toFun = ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ → V₂<VAR>h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂<VAR>h₂ : ℝ<VAR>h₃ : ∀ (v : V₁), ‖f v‖ ≤ h₂ * ‖v‖<GOAL>⇑{ toFun := f, map_add' := h₁, bound' := ⋯ } = f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ →+ V₂<VAR>C : ℝ<VAR>hC : ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖<GOAL>⇑(f.mkNormedAddGroupHom C hC) = ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ →+ V₂<VAR>C : ℝ≥0<VAR>hC : ∀ (x : V₁), ‖f x‖₊ ≤ C * ‖x‖₊<GOAL>⇑(f.mkNormedAddGroupHom' C hC) = ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>⇑f.toAddMonoidHom = ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>Function.Injective NormedAddGroupHom.toAddMonoidHom
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ → V₂<VAR>h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂<VAR>h₂ : ∃ C, ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖<GOAL>{ toFun := f, map_add' := h₁, bound' := h₂ }.toAddMonoidHom = AddMonoidHom.mk' f h₁
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>∃ C, 0 < C ∧ ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>K : ℝ≥0<VAR>h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖f x‖<GOAL>AntilipschitzWith K ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>K : AddSubgroup V₂<VAR>C C' : ℝ<VAR>h : f.SurjectiveOnWith K C<VAR>H : C ≤ C'<GOAL>f.SurjectiveOnWith K C'
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>K : AddSubgroup V₂<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith K C<GOAL>∃ C' > 0, f.SurjectiveOnWith K C'
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>K : AddSubgroup V₂<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith K C<GOAL>Set.SurjOn (⇑f) Set.univ ↑K
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>BddBelow {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>0 ≤ ‖f‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>x : V₁<GOAL>‖f x‖ ≤ ‖f‖ * ‖x‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>c : ℝ<VAR>x : V₁<VAR>h : ‖x‖ ≤ c<GOAL>‖f x‖ ≤ ‖f‖ * c
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>c : ℝ<VAR>h : ‖f‖ ≤ c<VAR>x : V₁<GOAL>‖f x‖ ≤ c * ‖x‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>LipschitzWith ⟨‖f‖, ⋯⟩ ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>UniformContinuous ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>Continuous ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>x : V₁<GOAL>‖f x‖ / ‖x‖ ≤ ‖f‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖<GOAL>‖f‖ ≤ M
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>M : ℝ<VAR>M_nonneg : 0 ≤ M<VAR>h_above : ∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖<VAR>h_below : ∀ N ≥ 0, (∀ (x : V₁), ‖f x‖ ≤ N * ‖x‖) → M ≤ N<GOAL>‖f‖ = M
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K ⇑f<GOAL>‖f‖ ≤ ↑K
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ →+ V₂<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖<GOAL>‖f.mkNormedAddGroupHom C h‖ ≤ C
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ →+ V₂<VAR>K : ℝ≥0<VAR>h : LipschitzWith K ⇑f<GOAL>‖NormedAddGroupHom.ofLipschitz f h‖ ≤ ↑K
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : V₁ →+ V₂<VAR>C : ℝ<VAR>h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖<GOAL>‖f.mkNormedAddGroupHom C h‖ ≤ max C 0
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>‖f + g‖ ≤ ‖f‖ + ‖g‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(f + g) v = f v + g v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>‖0‖ = 0
<VAR>V₁ : Type u_5<VAR>V₂ : Type u_6<VAR>NormedAddCommGroup V₁<VAR>NormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>‖f‖ = 0 ↔ f = 0