ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_4<VAR>f g : ι → ℝ≥0∞<VAR>h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k<GOAL>iSup f + iSup g = ⨆ a, f a + g a
<VAR>ι : Type u_4<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → ℝ≥0∞<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>iSup f + iSup g = ⨆ a, f a + g a
<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>s : Finset α<VAR>f : α → ι → ℝ≥0∞<VAR>hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k<GOAL>∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>f : α → ι → ℝ≥0∞<VAR>hf : ∀ (a : α), Monotone (f a)<GOAL>∑ a ∈ s, iSup (f a) = ⨆ n, ∑ a ∈ s, f a n
<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>a * iSup f = ⨆ i, a * f i
<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>a * sSup s = ⨆ i ∈ s, a * i
<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>iSup f * a = ⨆ i, f i * a
<VAR>ι : Sort u_4<VAR>R : Type u_5<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>f : ι → ℝ≥0∞<VAR>c : R<GOAL>c • ⨆ i, f i = ⨆ i, c • f i
<VAR>R : Type u_4<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>c : R<GOAL>c • sSup s = ⨆ i ∈ s, c • i
<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>iSup f / a = ⨆ i, f i / a
<VAR>r : ℝ≥0<VAR>b : ℝ≥0∞<GOAL>Filter.Tendsto (fun b => ↑r - b) (𝓝 b) (𝓝 (↑r - b))
<VAR>a : ℝ≥0∞<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>b : ι → ℝ≥0∞<VAR>hr : a < ⊤<GOAL>a - ⨆ i, b i = ⨅ i, a - b i
<GOAL>∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
<VAR>x y z : ℝ≥0∞<VAR>h : x < y + z<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>∃ y' z', y' < y ∧ z' < z ∧ x < y' + z'
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>Nonempty α<GOAL>ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)
<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<GOAL>∃ R, ∃ᶠ (n : ι) in l, x n < R
<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hx : Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤<GOAL>∃ R, ∃ᶠ (n : ι) in l, R < x n
<VAR>ι : Type u_4<VAR>l : Filter ι<VAR>x : ι → ℝ<VAR>hf : Filter.liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤<VAR>hbdd : ¬Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => |x i|<GOAL>∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
<VAR>α : Type u_1<VAR>r : ℝ≥0<VAR>f : α → ℝ≥0<VAR>h : HasSum f r<GOAL>∑' (a : α), ↑(f a) = ↑r
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<GOAL>Summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<GOAL>HasSum f (⨆ s, ∑ a ∈ s, f a)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<GOAL>Summable f
<VAR>β : Type u_2<VAR>f : β → ℝ≥0<GOAL>∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<GOAL>∑' (a : α), f a = ⨆ s, ∑ a ∈ s, f a
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>s : ι → Finset α<VAR>hs : ∀ (t : Finset α), ∃ i, t ⊆ s i<GOAL>∑' (a : α), f a = ⨆ i, ∑ a ∈ s i, f a
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>f : (a : α) → β a → ℝ≥0∞<GOAL>∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>f : (a : α) × β a → ℝ≥0∞<GOAL>∑' (p : (a : α) × β a), f p = ∑' (a : α) (b : β a), f ⟨a, b⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → ℝ≥0∞<GOAL>∑' (p : α × β), f p.1 p.2 = ∑' (a : α) (b : β), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α × β → ℝ≥0∞<GOAL>∑' (p : α × β), f p = ∑' (a : α) (b : β), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → ℝ≥0∞<GOAL>∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0∞<GOAL>∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ (a : α), f a ≤ g a<GOAL>∑' (a : α), f a ≤ ∑' (a : α), g a
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ (a : α), f a ≤ g a<GOAL>tsum f ≤ tsum g
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>s : Finset α<GOAL>∑ x ∈ s, f x ≤ ∑' (x : α), f x
<VAR>f : ℕ → ℝ≥0∞<VAR>N : ℕ → ℕ<VAR>hN : Filter.Tendsto N Filter.atTop Filter.atTop<GOAL>∑' (i : ℕ), f i = ⨆ i, ∑ a ∈ Finset.range (N i), f a
<VAR>f : ℕ → ℝ≥0∞<GOAL>∑' (i : ℕ), f i = ⨆ i, ∑ a ∈ Finset.range i, f a
<VAR>f : ℕ → ℝ≥0∞<GOAL>∑' (i : ℕ), f i = Filter.liminf (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
<VAR>f : ℕ → ℝ≥0∞<GOAL>∑' (i : ℕ), f i = Filter.limsup (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>f a ≤ ∑' (a : α), f a
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<GOAL>∑' (i : α), f i = 0 ↔ ∀ (i : α), f i = 0
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<GOAL>(∃ a, f a = ⊤) → ∑' (a : α), f a = ⊤
<VAR>α : Type u_1<VAR>a : α → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : α), a i ≠ ⊤<VAR>j : α<GOAL>a j < ⊤
<VAR>α : Type u_1<VAR>Nonempty α<GOAL>∑' (x : α), ⊤ = ⊤
<VAR>α : Type u_4<VAR>Infinite α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>∑' (x : α), c = ⊤
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>h : ∑' (a : α), f a ≠ ⊤<VAR>a : α<GOAL>f a ≠ ⊤
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>∑' (i : α), a * f i = a * ∑' (i : α), f i
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>∑' (i : α), f i * a = (∑' (i : α), f i) * a
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>R : Type u_4<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>a : R<GOAL>∑' (i : α), a • f i = a • ∑' (i : α), f i
<VAR>α : Type u_4<VAR>a : α<VAR>f : α → ℝ≥0∞<GOAL>∑' (b : α), ⨆ (_ : a = b), f b = f a
<VAR>f : ℕ → ℝ≥0∞<VAR>r : ℝ≥0∞<GOAL>HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 r)
<VAR>f : ℕ → ℝ≥0∞<GOAL>Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (i : α), f i ≠ ⊤<VAR>x : α<GOAL>↑((ENNReal.toNNReal ∘ f) x) = f x
<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (i : α), f i ≠ ⊤<GOAL>Summable (ENNReal.toNNReal ∘ f)
<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<GOAL>Filter.Tendsto f Filter.cofinite (𝓝 0)
<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (x : ℕ), f x ≠ ⊤<GOAL>Filter.Tendsto f Filter.atTop (𝓝 0)
<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<GOAL>Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (𝓝 0)
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>x : α<GOAL>tsum (fun i => f i) x = ∑' (i : ι), f i x
<VAR>f g : ℕ → ℝ≥0∞<VAR>h₁ : ∑' (i : ℕ), g i ≠ ⊤<VAR>h₂ : g ≤ f<GOAL>∑' (i : ℕ), (f i - g i) = ∑' (i : ℕ), f i - ∑' (i : ℕ), g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : β → ℝ≥0∞<GOAL>∑' (x : α), g (f x) ≤ ∑' (y : β), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>g : β → ℝ≥0∞<GOAL>∑' (y : β), g y ≤ ∑' (x : α), g (f x)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : α → ℝ≥0∞<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (i : ι) (x : ↑(t i)), f ↑x
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : α → ℝ≥0∞<VAR>s : Set ι<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : α → ℝ≥0∞<VAR>s : Finset ι<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Fintype ι<VAR>f : α → ℝ≥0∞<VAR>t : ι → Set α<GOAL>∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<GOAL>∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
<VAR>β : Type u_2<VAR>f : β → ℝ≥0∞<VAR>b : β<GOAL>∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x
<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (n : ℕ), f n = ⊤<VAR>hf0 : f 0 ≠ ⊤<GOAL>∑' (n : ℕ), f (n + 1) = ⊤
<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>tsum_ne_top : ∑' (i : ι), a i ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<GOAL>{i | ε ≤ a i}.Finite
<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<VAR>tsum_le_c : ∑' (i : ι), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<GOAL>∃ (hf : {i | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → ℝ≥0∞<VAR>g : β → γ<GOAL>∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i
<VAR>ι : Type u_4<VAR>fi : Filter ι<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ (i : ι), f i ≠ ⊤<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>Filter.Tendsto (fun n => (f n).toReal) fi (𝓝 x.toReal) ↔ Filter.Tendsto f fi (𝓝 x)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<GOAL>∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun a => ↑(f a)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<GOAL>∑' (a : α), ↑(f a) = ⊤ ↔ ¬Summable fun a => ↑(f a)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>hsum : ∑' (x : α), f x ≠ ⊤<GOAL>HasSum (fun x => (f x).toReal) (∑' (x : α), (f x).toReal)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>hsum : ∑' (x : α), f x ≠ ⊤<GOAL>Summable fun x => (f x).toReal
<VAR>β : Type u_2<VAR>f : β → ℝ≥0<GOAL>∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal
<VAR>β : Type u_2<VAR>f g : β → ℝ≥0<VAR>r : ℝ≥0<VAR>hgf : ∀ (b : β), g b ≤ f b<VAR>hfr : HasSum f r<GOAL>∃ p ≤ r, HasSum g p
<VAR>β : Type u_2<VAR>f g : β → ℝ≥0<VAR>hgf : ∀ (b : β), g b ≤ f b<GOAL>Summable f → Summable g
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>h : Summable f<GOAL>(Function.support f).Countable
<VAR>f : ℕ → ℝ≥0<VAR>r : ℝ≥0<GOAL>HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 r)
<VAR>f : ℕ → ℝ≥0<GOAL>¬Summable f ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
<VAR>f : ℕ → ℝ≥0<GOAL>Summable f ↔ ¬Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
<VAR>f : ℕ → ℝ≥0<VAR>c : ℝ≥0<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>Summable f
<VAR>f : ℕ → ℝ≥0<VAR>c : ℝ≥0<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>∑' (n : ℕ), f n ≤ c
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i : β → α<VAR>hi : Function.Injective i<GOAL>∑' (x : β), f (i x) ≤ ∑' (x : α), f x
<VAR>α : Type u_1<VAR>β : α → Type u_4<VAR>f : (x : α) × β x → ℝ≥0<GOAL>Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>s : Set α<GOAL>Summable (s.indicator f)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>s : Set α<VAR>h : ∃ a ∈ s, f a ≠ 0<GOAL>∑' (x : α), s.indicator f x ≠ 0
<VAR>f : ℕ → ℝ≥0<GOAL>Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0<VAR>sf sg : ℝ≥0<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<GOAL>sf < sg
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0<VAR>sf sg : ℝ≥0<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<VAR>h : f < g<GOAL>sf < sg
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hg : Summable g<GOAL>∑' (n : α), f n < ∑' (n : α), g n
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0<VAR>hg : Summable g<VAR>h : f < g<GOAL>∑' (n : α), f n < ∑' (n : α), g n
<VAR>α : Type u_1<VAR>g : α → ℝ≥0<VAR>hg : Summable g<VAR>i : α<VAR>hi : 0 < g i<GOAL>0 < ∑' (b : α), g b
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i : α<GOAL>∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≠ ⊤<GOAL>(∑' (a : α), f a).toNNReal = ∑' (a : α), (f a).toNNReal
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≠ ⊤<GOAL>(∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal
<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (i : ℕ), f i ≠ ⊤<GOAL>Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (𝓝 0)
<VAR>f : ℕ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>∑' (n : ℕ), f n ≤ c
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0∞<VAR>sf sg : ℝ≥0∞<VAR>i : α<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<VAR>hsf : sf ≠ ⊤<VAR>hf : HasSum f sf<VAR>hg : HasSum g sg<GOAL>sf < sg
<VAR>α : Type u_1<VAR>f g : α → ℝ≥0∞<VAR>i : α<VAR>hfi : tsum f ≠ ⊤<VAR>h : ∀ (a : α), f a ≤ g a<VAR>hi : f i < g i<GOAL>∑' (x : α), f x < ∑' (x : α), g x
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>f : α → ℝ<VAR>hf : Summable f<VAR>hn : ∀ (a : α), 0 ≤ f a<VAR>i : β → α<VAR>hi : Function.Injective i<GOAL>tsum (f ∘ i) ≤ tsum f
<VAR>β : Type u_2<VAR>f g : β → ℝ<VAR>hg : ∀ (b : β), 0 ≤ g b<VAR>hgf : ∀ (b : β), g b ≤ f b<VAR>hf : Summable f<GOAL>Summable g
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf : Summable f<GOAL>Summable fun n => (f n).toNNReal
<VAR>α : Type u_1<VAR>f : α → ℝ≥0∞<VAR>h : ∑' (i : α), f i ≠ ⊤<GOAL>(Function.support f).Countable
<VAR>f : ℕ → ℝ<VAR>hf : ∀ (i : ℕ), 0 ≤ f i<VAR>r : ℝ<GOAL>HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 r)
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf_nonneg : ∀ (n : α), 0 ≤ f n<VAR>hf : Summable f<GOAL>ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)
<VAR>β : Type u_2<VAR>EMetricSpace β<VAR>a : β<VAR>r : ℝ≥0∞<VAR>x y : ↑(EMetric.ball a r)<GOAL>edist ↑x ↑y ≠ ⊤
<VAR>β : Type u_2<VAR>EMetricSpace β<VAR>a x : β<VAR>r : ℝ≥0∞<VAR>h : x ∈ EMetric.ball a r<GOAL>𝓝 x = Filter.map Subtype.val (𝓝 ⟨x, h⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>l : Filter β<VAR>f : β → α<VAR>y : α<GOAL>Filter.Tendsto f l (𝓝 y) ↔ Filter.Tendsto (fun x => edist (f x) y) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>s : β → α<GOAL>CauchySeq s ↔ ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<GOAL>Continuous f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>Continuous fun p => edist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => edist (f b) (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>f g : β → α<VAR>x : Filter β<VAR>a b : α<VAR>hf : Filter.Tendsto f x (𝓝 a)<VAR>hg : Filter.Tendsto g x (𝓝 b)<GOAL>Filter.Tendsto (fun x => edist (f x) (g x)) x (𝓝 (edist a b))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)<VAR>hd : Summable d<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>hd : tsum d ≠ ⊤<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>a : α<VAR>r : ℝ≥0∞<GOAL>IsClosed (EMetric.closedBall a r)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>EMetric.diam (closure s) = EMetric.diam s
<VAR>α : Type u_4<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Metric.diam (closure s) = Metric.diam s
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<GOAL>IsClosed {f | LipschitzOnWith K f s}
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<GOAL>IsClosed {f | LipschitzWith K f}
<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<GOAL>EMetric.diam s = ENNReal.ofReal (sSup s - sInf s)
<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<GOAL>Metric.diam s = sSup s - sInf s
<VAR>a b : ℝ<GOAL>EMetric.diam (Set.Ioo a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>EMetric.diam (Set.Icc a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>EMetric.diam (Set.Ico a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>EMetric.diam (Set.Ioc a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Set.Icc a b) = b - a
<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Set.Ico a b) = b - a
<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Set.Ioc a b) = b - a
<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Set.Ioo a b) = b - a
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>edist (f 0) a ≤ ∑' (m : ℕ), d m
<VAR>t x : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x_le : x ≤ t<GOAL>t.truncateToReal x = x.toReal
<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>t.truncateToReal x ≤ t.toReal
<VAR>t x : ℝ≥0∞<GOAL>0 ≤ t.truncateToReal x
<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<GOAL>Monotone t.truncateToReal
<VAR>t : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<GOAL>Continuous t.truncateToReal
<VAR>ι : Type u_4<VAR>F : Filter ι<VAR>F.NeBot<VAR>f : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<GOAL>Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
<VAR>ι : Type u_4<VAR>F : Filter ι<VAR>F.NeBot<VAR>f : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<GOAL>Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
<VAR>ι : Type u_4<VAR>F : Filter ι<VAR>F.NeBot<VAR>f : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<GOAL>Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
<VAR>ι : Type u_4<VAR>F : Filter ι<VAR>F.NeBot<VAR>f : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<GOAL>Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<GOAL>Filter.liminf (fun i => (xs i).toReal) F = (Filter.liminf xs F).toReal
<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<GOAL>Filter.limsup (fun i => (xs i).toReal) F = (Filter.limsup xs F).toReal
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>f : C(α, β)<GOAL>Filter.Tendsto F p (𝓝 f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>f : C(α, β)<GOAL>(UniformOnFun.toFun {K | IsCompact K}) f.toUniformOnFunIsCompact = ⇑f
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<GOAL>UniformEmbedding ContinuousMap.toUniformOnFunIsCompact
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>ι : Type u_1<VAR>pi : ι → Prop<VAR>s : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis pi s<GOAL>(𝓤 C(α, β)).HasBasis (fun p => IsCompact p.1 ∧ pi p.2) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<GOAL>(𝓤 C(α, β)).HasBasis (fun p => IsCompact p.1 ∧ p.2 ∈ 𝓤 β) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2}
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>X : Set (C(α, β) × C(α, β))<GOAL>X ∈ 𝓤 C(α, β) ↔ ∃ K V, IsCompact K ∧ V ∈ 𝓤 β ∧ {fg | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>ι : Type u_1<VAR>p : ι → Prop<VAR>V : ι → Set (β × β)<VAR>K : CompactExhaustion α<VAR>hb : (𝓤 β).HasBasis p V<GOAL>(𝓤 C(α, β)).HasBasis (fun i => p i.2) fun i => {fg | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2}
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>V : ℕ → Set (β × β)<VAR>K : CompactExhaustion α<VAR>hb : (𝓤 β).HasAntitoneBasis V<GOAL>(𝓤 C(α, β)).HasAntitoneBasis fun n => {fg | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n}
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>h : TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p<GOAL>Filter.Tendsto F p (𝓝 f)
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>WeaklyLocallyCompactSpace α<GOAL>Filter.Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>WeaklyLocallyCompactSpace α<VAR>h : Filter.Tendsto F p (𝓝 f)<GOAL>TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>δ : Type u_2<VAR>UniformSpace δ<VAR>g : C(β, δ)<VAR>hg : UniformContinuous ⇑g<GOAL>UniformContinuous g.comp
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>δ : Type u_2<VAR>UniformSpace δ<VAR>g : C(β, δ)<VAR>hg : UniformInducing ⇑g<GOAL>UniformInducing g.comp
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>δ : Type u_2<VAR>UniformSpace δ<VAR>g : C(β, δ)<VAR>hg : UniformEmbedding ⇑g<GOAL>UniformEmbedding g.comp
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>γ : Type u_1<VAR>TopologicalSpace γ<VAR>g : C(α, γ)<GOAL>UniformContinuous fun f => f.comp g
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>CompactSpace α<GOAL>(𝓤 C(α, β)).HasBasis (fun V => V ∈ 𝓤 β) fun V => {fg | ∀ (x : α), (fg.1 x, fg.2 x) ∈ V}
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>CompactSpace α<GOAL>Filter.Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>δ₁ : Type u_1<VAR>δ₂ : Type u_2<VAR>TopologicalSpace δ₁<VAR>TopologicalSpace δ₂<VAR>φ₁ : C(δ₁, α)<VAR>φ₂ : C(δ₂, α)<VAR>h_proper₁ : IsProperMap ⇑φ₁<VAR>h_proper₂ : IsProperMap ⇑φ₂<VAR>h_cover : Set.range ⇑φ₁ ∪ Set.range ⇑φ₂ = Set.univ<GOAL>inferInstanceAs (UniformSpace C(α, β)) = UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>TopologicalSpace α<VAR>UniformSpace β<VAR>ι : Type u₃<VAR>δ : ι → Type u_1<VAR>(i : ι) → TopologicalSpace (δ i)<VAR>φ : (i : ι) → C(δ i, α)<VAR>h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)<VAR>h_lf : LocallyFinite fun i => Set.range ⇑(φ i)<VAR>h_cover : ⋃ i, Set.range ⇑(φ i) = Set.univ<GOAL>inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>CompactSpace α<GOAL>𝓝ˢ (Set.diagonal α) = 𝓤 α
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>CompactSpace α<GOAL>𝓤 α = ⨆ x, 𝓝 (x, x)
<VAR>γ : Type u_3<VAR>t : TopologicalSpace γ<VAR>CompactSpace γ<VAR>u u' : UniformSpace γ<VAR>h : UniformSpace.toTopologicalSpace = t<VAR>h' : UniformSpace.toTopologicalSpace = t<GOAL>u = u'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>CompactSpace α<VAR>f : α → β<VAR>h : Continuous f<GOAL>UniformContinuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<GOAL>UniformContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>r : Set (β × β)<VAR>s : Set α<VAR>hs : IsCompact s<VAR>f : α → β<VAR>hf : ∀ a ∈ s, ContinuousAt f a<VAR>hr : r ∈ 𝓤 β<GOAL>{x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>x : β<VAR>h_cont : Continuous f<VAR>hx : Filter.Tendsto f (Filter.cocompact α) (𝓝 x)<GOAL>UniformContinuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>Zero β<VAR>h1 : HasCompactSupport f<VAR>h2 : Continuous f<GOAL>UniformContinuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>One β<VAR>h1 : HasCompactMulSupport f<VAR>h2 : Continuous f<GOAL>UniformContinuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>LocallyCompactSpace α<VAR>CompactSpace β<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>x : α<VAR>U : Set α<VAR>hxU : U ∈ 𝓝 x<VAR>h : ContinuousOn (↿f) (U ×ˢ Set.univ)<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>WeaklyLocallyCompactSpace α<VAR>CompactSpace β<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>h : Continuous ↿f<VAR>x : α<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u