ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist a b ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist a b ≤ ‖a‖ + ‖b‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>|‖a‖ - ‖b‖| ≤ ‖a - b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>|‖a‖ - ‖b‖| ≤ ‖a / b‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a‖ - ‖b‖ ≤ ‖a - b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a‖ - ‖b‖ ≤ ‖a / b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>dist ‖a‖ ‖b‖ ≤ ‖a / b‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>dist ‖a‖ ‖b‖ ≤ ‖a - b‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>u v : E<GOAL>‖u‖ ≤ ‖v‖ + ‖u / v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>u v : E<GOAL>‖u‖ ≤ ‖v‖ + ‖u - v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>u v : E<GOAL>‖v‖ ≤ ‖u‖ + ‖u - v‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>u v : E<GOAL>‖v‖ ≤ ‖u‖ + ‖u / v‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>u v : E<GOAL>‖u‖ ≤ ‖u * v‖ + ‖v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>u v : E<GOAL>‖u‖ ≤ ‖u + v‖ + ‖v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>y : E<VAR>ε : ℝ<GOAL>Metric.ball y ε = {x | ‖x - y‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>y : E<VAR>ε : ℝ<GOAL>Metric.ball y ε = {x | ‖x / y‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>r : ℝ<GOAL>Metric.ball 1 r = {x | ‖x‖ < r}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>r : ℝ<GOAL>Metric.ball 0 r = {x | ‖x‖ < r}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.ball a r ↔ ‖b - a‖ < r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.ball a r ↔ ‖b / a‖ < r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.ball a r ↔ ‖a - b‖ < r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.ball a r ↔ ‖a / b‖ < r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.ball 1 r ↔ ‖a‖ < r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.ball 0 r ↔ ‖a‖ < r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<VAR>h : b ∈ Metric.closedBall a r<GOAL>‖b‖ ≤ ‖a‖ + r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<VAR>h : b ∈ Metric.closedBall a r<GOAL>‖b‖ ≤ ‖a‖ + r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<VAR>h : b ∈ Metric.ball a r<GOAL>‖b‖ < ‖a‖ + r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<VAR>h : b ∈ Metric.ball a r<GOAL>‖b‖ < ‖a‖ + r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>u v w : E<GOAL>‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>u v w : E<GOAL>‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.sphere a r ↔ ‖b - a‖ = r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>b ∈ Metric.sphere a r ↔ ‖b / a‖ = r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.sphere 1 r ↔ ‖a‖ = r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>r : ℝ<GOAL>a ∈ Metric.sphere 0 r ↔ ‖a‖ = r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>r : ℝ<VAR>x : ↑(Metric.sphere 0 r)<GOAL>‖↑x‖ = r
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>r : ℝ<VAR>x : ↑(Metric.sphere 1 r)<GOAL>‖↑x‖ = r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x : ↑(Metric.sphere 0 r)<GOAL>↑x ≠ 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>x : ↑(Metric.sphere 1 r)<GOAL>↑x ≠ 1
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : ↑(Metric.sphere 0 1)<GOAL>↑x ≠ 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : ↑(Metric.sphere 1 1)<GOAL>↑x ≠ 1
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>⇑(normAddGroupSeminorm E) = norm
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>⇑(normGroupSeminorm E) = norm
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>f : α → E<VAR>l : Filter α<GOAL>Filter.Tendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>l : Filter α<GOAL>Filter.Tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
<VAR>E : Type u_6<VAR>F : Type u_7<VAR>SeminormedAddGroup E<VAR>SeminormedAddGroup F<VAR>f : E → F<VAR>x : E<VAR>y : F<GOAL>Filter.Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' - x‖ < δ → ‖f x' - y‖ < ε
<VAR>E : Type u_6<VAR>F : Type u_7<VAR>SeminormedGroup E<VAR>SeminormedGroup F<VAR>f : E → F<VAR>x : E<VAR>y : F<GOAL>Filter.Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y - x‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y / x‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>(𝓝 1).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>(𝓤 E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 / p.2‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>(𝓤 E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 - p.2‖ < ε}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>↑‖a‖₊ = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>↑‖a‖₊ = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>NNReal.toReal ∘ nnnorm = norm
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>NNReal.toReal ∘ nnnorm = norm
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖a‖.toNNReal = ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖a‖.toNNReal = ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>nndist a b = ‖a / b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>nndist a b = ‖a - b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>‖1‖₊ = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>‖0‖₊ = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖a‖₊ ≠ 0 → a ≠ 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖a‖₊ ≠ 0 → a ≠ 1
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>‖-a‖₊ = ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>‖a⁻¹‖₊ = ‖a‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>nndist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>ENNReal.ofReal ‖a‖ = ↑‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>ENNReal.ofReal ‖a‖ = ↑‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<GOAL>(↑‖a‖₊).toReal = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<GOAL>(↑‖a‖₊).toReal = ‖a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a b : E<GOAL>edist a b = ↑‖a - b‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a b : E<GOAL>edist a b = ↑‖a / b‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>edist x 0 = ↑‖x‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>edist x 1 = ↑‖x‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>edist (s.indicator f x) (t.indicator f x) = ↑‖(symmDiff s t).indicator f x‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(symmDiff s t).mulIndicator f x‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>r : ℝ≥0∞<GOAL>a ∈ EMetric.ball 1 r ↔ ↑‖a‖₊ < r
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>r : ℝ≥0∞<GOAL>a ∈ EMetric.ball 0 r ↔ ↑‖a‖₊ < r
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>f : α → E<VAR>a : Filter α<VAR>b : E<GOAL>Filter.Tendsto f a (𝓝 b) ↔ Filter.Tendsto (fun e => ‖f e / b‖) a (𝓝 0)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>a : Filter α<VAR>b : E<GOAL>Filter.Tendsto f a (𝓝 b) ↔ Filter.Tendsto (fun e => ‖f e - b‖) a (𝓝 0)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>a : Filter α<GOAL>Filter.Tendsto f a (𝓝 0) ↔ Filter.Tendsto (fun x => ‖f x‖) a (𝓝 0)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>f : α → E<VAR>a : Filter α<GOAL>Filter.Tendsto f a (𝓝 1) ↔ Filter.Tendsto (fun x => ‖f x‖) a (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>Filter.comap norm (𝓝 0) = 𝓝 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>Filter.comap norm (𝓝 0) = 𝓝 1
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>a : α → ℝ<VAR>t₀ : Filter α<VAR>h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n<VAR>h' : Filter.Tendsto a t₀ (𝓝 0)<GOAL>Filter.Tendsto f t₀ (𝓝 0)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>f : α → E<VAR>a : α → ℝ<VAR>t₀ : Filter α<VAR>h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n<VAR>h' : Filter.Tendsto a t₀ (𝓝 0)<GOAL>Filter.Tendsto f t₀ (𝓝 1)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>f : α → E<VAR>a : α → ℝ<VAR>t₀ : Filter α<VAR>h : ∀ (n : α), ‖f n‖ ≤ a n<GOAL>Filter.Tendsto a t₀ (𝓝 0) → Filter.Tendsto f t₀ (𝓝 1)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>f : α → E<VAR>a : α → ℝ<VAR>t₀ : Filter α<VAR>h : ∀ (n : α), ‖f n‖ ≤ a n<GOAL>Filter.Tendsto a t₀ (𝓝 0) → Filter.Tendsto f t₀ (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>Filter.Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>Filter.Tendsto (fun a => ‖a - x‖) (𝓝 x) (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>Filter.Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>Filter.Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>Filter.Tendsto (fun a => ‖a‖) (𝓝 1) (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>Filter.Tendsto (fun a => ‖a‖) (𝓝 0) (𝓝 0)
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>Continuous fun a => ‖a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>Continuous fun a => ‖a‖
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>Continuous fun a => ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>Continuous fun a => ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>x : E<GOAL>x ∈ closure {0} ↔ ‖x‖ = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>x : E<GOAL>x ∈ closure {1} ↔ ‖x‖ = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<GOAL>closure {1} = {x | ‖x‖ = 0}
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<GOAL>closure {0} = {x | ‖x‖ = 0}
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => ‖f x‖) l (𝓝 ‖a‖)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => ‖f x‖) l (𝓝 ‖a‖)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>a : E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => ‖f x‖₊) l (𝓝 ‖a‖₊)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>a : E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => ‖f x‖₊) l (𝓝 ‖a‖₊)
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>Continuous f → Continuous fun x => ‖f x‖
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>Continuous f → Continuous fun x => ‖f x‖
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>Continuous f → Continuous fun x => ‖f x‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>Continuous f → Continuous fun x => ‖f x‖₊
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>a : α<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => ‖f x‖) a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>a : α<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => ‖f x‖) a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>a : α<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => ‖f x‖₊) a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>a : α<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => ‖f x‖₊) a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => ‖f x‖) s a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => ‖f x‖) s a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => ‖f x‖₊) s a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => ‖f x‖₊) s a
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => ‖f x‖) s
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => ‖f x‖) s
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => ‖f x‖₊) s
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => ‖f x‖₊) s
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop<VAR>x : E<GOAL>∀ᶠ (y : α) in l, f y ≠ x
<VAR>α : Type u_3<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>l : Filter α<VAR>f : α → E<VAR>h : Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop<VAR>x : E<GOAL>∀ᶠ (y : α) in l, f y ≠ x
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>s : Set E<VAR>a : E<GOAL>a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>s : Set E<VAR>a : E<GOAL>a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>T0Space E<VAR>a : E<GOAL>‖a‖ ≤ 0 ↔ a = 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>T0Space E<VAR>a : E<GOAL>‖a‖ ≤ 0 ↔ a = 1
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>T0Space E<VAR>a : E<GOAL>‖a‖ = 0 ↔ a = 1
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>T0Space E<VAR>a : E<GOAL>‖a‖ = 0 ↔ a = 0
<VAR>E : Type u_6<VAR>SeminormedAddGroup E<VAR>T0Space E<VAR>a : E<GOAL>0 < ‖a‖ ↔ a ≠ 0
<VAR>E : Type u_6<VAR>SeminormedGroup E<VAR>T0Space E<VAR>a : E<GOAL>0 < ‖a‖ ↔ a ≠ 1
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedAddGroup G<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>TendstoUniformlyOn f 0 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedGroup G<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedGroup G<VAR>f : ι → κ → G<VAR>l : Filter ι<VAR>l' : Filter κ<GOAL>UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedAddGroup G<VAR>f : ι → κ → G<VAR>l : Filter ι<VAR>l' : Filter κ<GOAL>UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedAddGroup G<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) s
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>G : Type u_8<VAR>SeminormedGroup G<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>x y : E<GOAL>dist (-x) y = dist x (-y)
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>x y : E<GOAL>dist x⁻¹ y = dist x y⁻¹
<VAR>E : Type u_9<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_9<VAR>E : Type u_10<VAR>SeminormedAddCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<GOAL>‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<VAR>n : ι → ℝ<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>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f : ι → E<VAR>n : ι → ℝ<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 a : ι → E<VAR>d : ι → ℝ<VAR>h : ∀ b ∈ s, dist (f b) (a b) ≤ d b<GOAL>dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, d b
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f a : ι → E<VAR>d : ι → ℝ<VAR>h : ∀ b ∈ s, dist (f b) (a b) ≤ d b<GOAL>dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>s : Finset ι<VAR>f a : ι → E<GOAL>dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)
<VAR>ι : Type u_4<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>s : Finset ι<VAR>f a : ι → E<GOAL>dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a * b ∈ Metric.ball a r ↔ ‖b‖ < r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a + b ∈ Metric.ball a r ↔ ‖b‖ < r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>(fun x => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>n : ℕ<VAR>a : E<GOAL>‖n • a‖ ≤ ↑n * ‖a‖
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>n : ℕ<VAR>a : E<GOAL>‖a ^ n‖ ≤ ↑n * ‖a‖
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>n : ℕ<VAR>a : E<GOAL>‖a ^ n‖₊ ≤ ↑n * ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>n : ℕ<VAR>a : E<GOAL>‖n • a‖₊ ≤ ↑n * ‖a‖₊
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>n : ℕ<VAR>h : a ∈ Metric.closedBall b r<GOAL>a ^ n ∈ Metric.closedBall (b ^ n) (n • r)
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>n : ℕ<VAR>h : a ∈ Metric.closedBall b r<GOAL>n • a ∈ Metric.closedBall (n • b) (n • r)
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : a ∈ Metric.ball b r<GOAL>a ^ n ∈ Metric.ball (b ^ n) (n • r)
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : a ∈ Metric.ball b r<GOAL>n • a ∈ Metric.ball (n • b) (n • r)
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>a * c ∈ Metric.closedBall (b * c) r ↔ a ∈ Metric.closedBall b r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>a + c ∈ Metric.closedBall (b + c) r ↔ a ∈ Metric.closedBall b r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>a * c ∈ Metric.ball (b * c) r ↔ a ∈ Metric.ball b r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>a + c ∈ Metric.ball (b + c) r ↔ a ∈ Metric.ball b r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a • Metric.closedBall b r = Metric.closedBall (a • b) r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a b : E<VAR>r : ℝ<GOAL>a • Metric.ball b r = Metric.ball (a • b) r
<VAR>E : Type u_6<VAR>SeminormedAddCommGroup E<VAR>a : E<VAR>s : AddSubgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<GOAL>∃ v, Filter.Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), v i) Filter.atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 - a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<VAR>E : Type u_6<VAR>SeminormedCommGroup E<VAR>a : E<VAR>s : Subgroup E<VAR>hg : a ∈ closure ↑s<VAR>b : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < b n<GOAL>∃ v, Filter.Tendsto (fun n => ∏ i ∈ Finset.range (n + 1), v i) Filter.atTop (𝓝 a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
<VAR>E : Type u_6<VAR>F : Type u_7<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup 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