ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>self : ModuleFilterBasis R M<VAR>U : Set M<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>self : ModuleFilterBasis R M<VAR>m₀ : M<VAR>U : Set M<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : ModuleFilterBasis R M<VAR>U : Set M<VAR>hU : U ∈ B<GOAL>∃ V ∈ 𝓝 0, ∃ W ∈ B, V • W ⊆ U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : ModuleFilterBasis R M<VAR>x₀ : R<VAR>U : Set M<VAR>hU : U ∈ B<GOAL>∃ V ∈ B, V ⊆ (fun x => x₀ • x) ⁻¹' U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>B : ModuleFilterBasis R M<VAR>m₀ : M<VAR>U : Set M<VAR>hU : U ∈ B<GOAL>∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>TopologicalRing R<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>p : ι → Prop<VAR>b : ι → Set M<VAR>h : (𝓝 0).HasBasis p b<VAR>hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i<VAR>hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ Set.MapsTo (fun x => x₀ • x) (b j) (b i)<VAR>hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i<GOAL>ContinuousSMul R M
<VAR>α : Type u_4<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>β : Type u_5<VAR>f : β → α<GOAL>tsum f = if h : Summable f then if (Function.support f).Finite then finsum f else Exists.choose h else 0
<VAR>α : Type u_4<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>β : Type u_5<VAR>f : β → α<GOAL>tprod f = if h : Multipliable f then if (Function.mulSupport f).Finite then finprod f else Exists.choose h else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>h : HasProd f a<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>h : HasSum f a<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>h : ¬Multipliable f<GOAL>∏' (b : β), f b = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>h : ¬Summable f<GOAL>∑' (b : β), f b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>hf : ∀ x ∉ Set.range g, f x = 0<GOAL>HasSum (f ∘ g) a ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>hf : ∀ x ∉ Set.range g, f x = 1<GOAL>HasProd (f ∘ g) a ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set β<VAR>hf : Function.support f ⊆ s<GOAL>HasSum (f ∘ Subtype.val) a ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set β<VAR>hf : Function.mulSupport f ⊆ s<GOAL>HasProd (f ∘ Subtype.val) a ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>Fintype β<VAR>f : β → α<GOAL>HasSum f (∑ b : β, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>Fintype β<VAR>f : β → α<GOAL>HasProd f (∏ b : β, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>HasSum (f ∘ Subtype.val) (∑ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 0<GOAL>HasSum f (∑ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 1<GOAL>HasProd f (∏ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 0<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 1<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ha : Summable f<GOAL>HasSum f (∑' (b : β), f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ha : Multipliable f<GOAL>HasProd f (∏' (b : β), f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>T2Space α<GOAL>HasProd f a₁ → HasProd f a₂ → a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>T2Space α<GOAL>HasSum f a₁ → HasSum f a₂ → a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>T2Space α<VAR>ha : HasProd f a<GOAL>∏' (b : β), f b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>T2Space α<VAR>ha : HasSum f a<GOAL>∑' (b : β), f b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>T2Space α<VAR>h : Summable f<GOAL>HasSum f a ↔ ∑' (b : β), f b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>T2Space α<VAR>h : Multipliable f<GOAL>HasProd f a ↔ ∏' (b : β), f b = a
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a₁ : α<VAR>a₂ : α<VAR>h : HasSum f a₁<GOAL>HasSum (fun i => a₂ * f i) (a₂ * a₁)
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a₁ : α<VAR>a₂ : α<VAR>hf : HasSum f a₁<GOAL>HasSum (fun i => f i * a₂) (a₁ * a₂)
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>hf : Summable f<GOAL>Summable fun i => a * f i
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>hf : Summable f<GOAL>Summable fun i => f i * a
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>T2Space α<VAR>a : α<VAR>hf : Summable f<GOAL>∑' (i : ι), a * f i = a * ∑' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>T2Space α<VAR>a : α<VAR>hf : Summable f<GOAL>∑' (i : ι), f i * a = (∑' (i : ι), f i) * a
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>T2Space α<VAR>a : α<VAR>h : ∀ (i : ι), Commute a (f i)<GOAL>Commute a (∑' (i : ι), f i)
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>T2Space α<VAR>a : α<VAR>h : ∀ (i : ι), Commute (f i) a<GOAL>Commute (∑' (i : ι), f i) a
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>h : HasSum f a<VAR>b : α<GOAL>HasSum (fun i => f i / b) (a / b)
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>h : Summable f<VAR>b : α<GOAL>Summable fun i => f i / b
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a₁ a₂ : α<VAR>h : a₂ ≠ 0<GOAL>HasSum (fun i => a₂ * f i) (a₂ * a₁) ↔ HasSum f a₁
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a₁ a₂ : α<VAR>h : a₂ ≠ 0<GOAL>HasSum (fun i => f i * a₂) (a₁ * a₂) ↔ HasSum f a₁
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a₁ a₂ : α<VAR>h : a₂ ≠ 0<GOAL>HasSum (fun i => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>h : a ≠ 0<GOAL>(Summable fun i => a * f i) ↔ Summable f
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>h : a ≠ 0<GOAL>(Summable fun i => f i * a) ↔ Summable f
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>h : a ≠ 0<GOAL>(Summable fun i => f i / a) ↔ Summable f
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>T2Space α<GOAL>∑' (x : ι), a * f x = a * ∑' (x : ι), f x
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>T2Space α<GOAL>∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
<VAR>ι : Type u_1<VAR>α : Type u_4<VAR>DivisionSemiring α<VAR>TopologicalSpace α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>a : α<VAR>T2Space α<GOAL>∑' (x : ι), f x / a = (∑' (x : ι), f x) / a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>T3Space α<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>g : κ → α<VAR>s t u : α<VAR>hf : HasSum f s<VAR>hg : HasSum g t<VAR>hfg : HasSum (fun x => f x.1 * g x.2) u<GOAL>s * t = u
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>T3Space α<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>g : κ → α<VAR>s t : α<VAR>hf : HasSum f s<VAR>hg : HasSum g t<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>HasSum (fun x => f x.1 * g x.2) (s * t)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>T3Space α<VAR>NonUnitalNonAssocSemiring α<VAR>TopologicalSemiring α<VAR>f : ι → α<VAR>g : κ → α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2
<VAR>α : Type u_4<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocSemiring α<VAR>f g : A → α<GOAL>(Summable fun x => f x.1 * g x.2) ↔ Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
<VAR>α : Type u_4<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>T3Space α<VAR>TopologicalSemiring α<VAR>h : Summable fun x => f x.1 * g x.2<GOAL>Summable fun n => ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
<VAR>α : Type u_4<VAR>A : Type u_5<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocSemiring α<VAR>f g : A → α<VAR>T3Space α<VAR>TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>T3Space α<VAR>TopologicalSemiring α<VAR>h : Summable fun x => f x.1 * g x.2<GOAL>Summable fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>T3Space α<VAR>TopologicalSemiring α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hfg : Summable fun x => f x.1 * g x.2<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>x y : X<GOAL>dist x y = ↑(⨅ l, (List.zipWith d (x :: l) (l ++ [y])).sum)
<VAR>X : Type u_1<VAR>d : X → X → ℝ≥0<VAR>dist_self : ∀ (x : X), d x x = 0<VAR>dist_comm : ∀ (x y : X), d x y = d y x<VAR>x y : X<GOAL>dist x y ≤ ↑(d x y)
<VAR>X : Type u_2<VAR>UniformSpace X<VAR>(𝓤 X).IsCountablyGenerated<GOAL>∃ I, PseudoMetricSpace.toUniformSpace = inst✝
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>(𝓤 X).IsCountablyGenerated<VAR>T0Space X<GOAL>TopologicalSpace.MetrizableSpace X
<VAR>X : Type u_1<VAR>UniformSpace X<VAR>i : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>h : TotallyBounded s<GOAL>TopologicalSpace.IsSeparable s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>a : α<GOAL>HasSum (⇑UniformSpace.Completion.toCompl ∘ f) (↑α a) ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<GOAL>Summable f ↔ Summable (⇑UniformSpace.Completion.toCompl ∘ f) ∧ ∑' (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<GOAL>Summable f ↔ (CauchySeq fun s => ∑ b ∈ s, f b) ∧ ∑' (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>hf : Summable f<GOAL>∑' (i : β), UniformSpace.Completion.toCompl (f i) = ↑α (∑' (i : β), f i)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>h : Summable fun n => dist (f n) (f n.succ)<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>dist (f 0) a ≤ tsum d
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>h : Summable fun n => dist (f n) (f n.succ)<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ ∑' (m : ℕ), dist (f (n + m)) (f (n + m).succ)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>h : Summable fun n => dist (f n) (f n.succ)<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)
<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), 0 ≤ f n<GOAL>¬Summable f ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), 0 ≤ f n<GOAL>Summable f ↔ ¬Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
<VAR>α : Type u_1<VAR>β : α → Type u_3<VAR>f : (x : α) × β x → ℝ<VAR>hf : ∀ (x : (x : α) × β x), 0 ≤ f x<GOAL>Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : β → ℝ<VAR>hf : 0 ≤ f<VAR>s : α → Set β<VAR>hs : ∀ (i : β), ∃! j, i ∈ s j<GOAL>Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α × β → ℝ<VAR>hf : 0 ≤ f<GOAL>Summable f ↔ (∀ (x : α), Summable fun y => f (x, y)) ∧ Summable fun x => ∑' (y : β), f (x, y)
<VAR>ι : Type u_3<VAR>f : ι → ℝ<VAR>c : ℝ<VAR>hf : 0 ≤ f<VAR>h : ∀ (u : Finset ι), ∑ x ∈ u, f x ≤ c<GOAL>Summable f
<VAR>f : ℕ → ℝ<VAR>c : ℝ<VAR>hf : ∀ (n : ℕ), 0 ≤ f n<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>Summable f
<VAR>f : ℕ → ℝ<VAR>c : ℝ<VAR>hf : ∀ (n : ℕ), 0 ≤ f n<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>∑' (n : ℕ), f n ≤ c
<VAR>i : ℕ<VAR>f g : ℕ → ℝ<VAR>h0 : ∀ (b : ℕ), 0 ≤ f b<VAR>h : ∀ (b : ℕ), f b ≤ g b<VAR>hi : f i < g i<VAR>hg : Summable g<GOAL>∑' (n : ℕ), f n < ∑' (n : ℕ), g n
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : CompactIccSpace α<VAR>a b : α<GOAL>IsCompact (Set.Icc a b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>h : ∀ {a b : α}, a ≤ b → IsCompact (Set.Icc a b)<GOAL>CompactIccSpace α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>h : ∀ {a b : α}, a < b → IsCompact (Set.Icc a b)<GOAL>CompactIccSpace α
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>IsCompact (Set.uIcc a b)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>∃ x, IsLeast s x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>∃ x, IsGreatest s x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>∃ x ∈ s, IsGLB s x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>∃ x ∈ s, IsLUB s x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α ≤ Filter.atBot ⊔ Filter.atTop
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTop α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α ≤ Filter.atBot
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderBot α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α ≤ Filter.atTop
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMinOrder α<VAR>ClosedIicTopology α<GOAL>Filter.atBot ≤ Filter.cocompact α
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMaxOrder α<VAR>ClosedIciTopology α<GOAL>Filter.atTop ≤ Filter.cocompact α
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>OrderClosedTopology α<GOAL>Filter.atBot ⊔ Filter.atTop ≤ Filter.cocompact α
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMaxOrder α<VAR>NoMinOrder α<VAR>OrderClosedTopology α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMinOrder α<VAR>OrderTop α<VAR>ClosedIicTopology α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α = Filter.atBot
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>NoMaxOrder α<VAR>OrderBot α<VAR>ClosedIciTopology α<VAR>CompactIccSpace α<GOAL>Filter.cocompact α = Filter.atTop
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>NoMaxOrder α<VAR>f : β → α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<VAR>a : α<VAR>hf' : ∀ b ∈ s, a < f b<GOAL>∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, ∀ y ∈ s, f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, IsMaxOn f s x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, ∀ y ∈ s, f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in Filter.cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in Filter.cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<GOAL>∃ x ∈ s, ∀ y ∈ s, f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in Filter.cocompact β ⊓ 𝓟 s, f x ≤ f x₀<GOAL>∃ x ∈ s, IsMaxOn f s x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in Filter.cocompact β ⊓ 𝓟 s, f x ≤ f x₀<GOAL>∃ x ∈ s, ∀ y ∈ s, f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>hf : Continuous f<VAR>x₀ : β<VAR>h : ∀ᶠ (x : β) in Filter.cocompact β, f x₀ ≤ f x<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>hf : Continuous f<VAR>x₀ : β<VAR>h : ∀ᶠ (x : β) in Filter.cocompact β, f x ≤ f x₀<GOAL>∃ x, ∀ (y : β), f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>Nonempty β<VAR>f : β → α<VAR>hf : Continuous f<VAR>hlim : Filter.Tendsto f (Filter.cocompact β) Filter.atTop<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>Nonempty β<VAR>f : β → α<VAR>hf : Continuous f<VAR>hlim : Filter.Tendsto f (Filter.cocompact β) Filter.atBot<GOAL>∃ x, ∀ (y : β), f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>Nonempty β<VAR>One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>Nonempty β<VAR>Zero α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>Nonempty β<VAR>One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<GOAL>∃ x, ∀ (y : β), f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>Nonempty β<VAR>Zero α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>∃ x, ∀ (y : β), f y ≤ f x
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>Nonempty α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>BddBelow s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>Nonempty α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>BddAbove s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>Nonempty α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : ContinuousOn f K<GOAL>BddBelow (f '' K)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>Nonempty α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : ContinuousOn f K<GOAL>BddAbove (f '' K)