ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>TopologicalSpace X<VAR>CommSemiring 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>TopologicalSemiring B<VAR>Star B<VAR>ContinuousStar B<VAR>Algebra 𝕜 B<VAR>φ : A →⋆ₐ[𝕜] B<VAR>hφ : Continuous ⇑φ<VAR>f : C(X, A)<GOAL>(ContinuousMap.compStarAlgHom X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ }.comp f
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>A : Type u_3<VAR>TopologicalSpace X<VAR>CommSemiring 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<GOAL>ContinuousMap.compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯ = StarAlgHom.id 𝕜 C(X, A)
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>TopologicalSpace X<VAR>CommSemiring 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>TopologicalSpace B<VAR>Semiring B<VAR>TopologicalSemiring B<VAR>Star B<VAR>ContinuousStar B<VAR>Algebra 𝕜 B<VAR>TopologicalSpace C<VAR>Semiring C<VAR>TopologicalSemiring C<VAR>Star C<VAR>ContinuousStar C<VAR>Algebra 𝕜 C<VAR>φ : A →⋆ₐ[𝕜] B<VAR>ψ : B →⋆ₐ[𝕜] C<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<GOAL>ContinuousMap.compStarAlgHom X (ψ.comp φ) ⋯ = (ContinuousMap.compStarAlgHom X ψ hψ).comp (ContinuousMap.compStarAlgHom X φ hφ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>AddCommGroup X<VAR>TopologicalAddGroup X<VAR>AddCommMonoid Y<VAR>ContinuousAdd Y<VAR>T2Space Y<VAR>f : C(X, Y)<VAR>p : X<GOAL>Function.Periodic (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)))) p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>𝕜 : Type u_3<VAR>CommSemiring 𝕜<VAR>A : Type u_4<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>StarRing A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>f : X ≃ₜ Y<VAR>a : C(X, A)<GOAL>(Homeomorph.compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>𝕜 : Type u_3<VAR>CommSemiring 𝕜<VAR>A : Type u_4<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>StarRing A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>f : X ≃ₜ Y<VAR>a : C(Y, A)<GOAL>(Homeomorph.compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) a
<VAR>X : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>CommSemiring S<VAR>CommSemiring R<VAR>Algebra S R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>x : X<VAR>f : C(X, R)<GOAL>(ContinuousMap.evalAlgHom S R x) f = f x
<VAR>X : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>CommSemiring S<VAR>CommSemiring R<VAR>Algebra S R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>StarRing R<VAR>ContinuousStar R<VAR>x : X<VAR>f : C(X, R)<GOAL>(ContinuousMap.evalStarAlgHom S R x) f = f x
<VAR>α : Type u_3<VAR>Preorder α<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>T2Space α<VAR>f : ℕ → α<VAR>c : α<VAR>hf : Summable f<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>∑' (n : ℕ), f n ≤ c
<VAR>α : Type u_3<VAR>Preorder α<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>T2Space α<VAR>f : ℕ → α<VAR>c : α<VAR>hf : Multipliable f<VAR>h : ∀ (n : ℕ), ∏ i ∈ Finset.range n, f i ≤ c<GOAL>∏' (n : ℕ), f n ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>h : ∀ (i : ι), f i ≤ g i<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>h : ∀ (i : ι), f i ≤ g i<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<VAR>h : f ≤ g<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<VAR>h : f ≤ g<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a a₂ : α<VAR>hf : HasSum f a<VAR>h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂<GOAL>a ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a a₂ : α<VAR>hf : HasProd f a<VAR>h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂<GOAL>a ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a a₂ : α<VAR>hf : HasProd f a<VAR>h : ∀ (s : Finset ι), a₂ ≤ ∏ i ∈ s, f i<GOAL>a₂ ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a a₂ : α<VAR>hf : HasSum f a<VAR>h : ∀ (s : Finset ι), a₂ ≤ ∑ i ∈ s, f i<GOAL>a₂ ≤ a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₁ a₂ : α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>hs : ∀ c ∉ Set.range e, 1 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₁ a₂ : α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>hs : ∀ c ∉ Set.range e, 0 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<GOAL>a₁ ≤ a₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>hs : ∀ c ∉ Set.range e, 1 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>tprod f ≤ tprod g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Function.Injective e<VAR>hs : ∀ c ∉ Set.range e, 0 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>tsum f ≤ tsum g
<VAR>κ : Type u_4<VAR>γ : Type u_5<VAR>OrderedCommGroup γ<VAR>UniformSpace γ<VAR>UniformGroup γ<VAR>OrderClosedTopology γ<VAR>CompleteSpace γ<VAR>f : κ → γ<VAR>β : Set κ<VAR>h : ∀ (a : κ), 1 ≤ f a<VAR>hf : Multipliable f<GOAL>∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a
<VAR>κ : Type u_4<VAR>γ : Type u_5<VAR>OrderedAddCommGroup γ<VAR>UniformSpace γ<VAR>UniformAddGroup γ<VAR>OrderClosedTopology γ<VAR>CompleteSpace γ<VAR>f : κ → γ<VAR>β : Set κ<VAR>h : ∀ (a : κ), 0 ≤ f a<VAR>hf : Summable f<GOAL>∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>s : Finset ι<VAR>hs : ∀ i ∉ s, 0 ≤ f i<VAR>hf : HasSum f a<GOAL>∑ i ∈ s, f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>s : Finset ι<VAR>hs : ∀ i ∉ s, 1 ≤ f i<VAR>hf : HasProd f a<GOAL>∏ i ∈ s, f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), 0 ≤ f i<VAR>hf : HasSum f a<GOAL>IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>hf : HasProd f a<GOAL>IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasSum f a<VAR>i : ι<VAR>hb : ∀ (j : ι), j ≠ i → 0 ≤ f j<GOAL>f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasProd f a<VAR>i : ι<VAR>hb : ∀ (j : ι), j ≠ i → 1 ≤ f j<GOAL>f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>s : Finset ι<VAR>hs : ∀ i ∉ s, 0 ≤ f i<VAR>hf : Summable f<GOAL>∑ i ∈ s, f i ≤ ∑' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>s : Finset ι<VAR>hs : ∀ i ∉ s, 1 ≤ f i<VAR>hf : Multipliable f<GOAL>∏ i ∈ s, f i ≤ ∏' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Summable f<VAR>i : ι<VAR>hb : ∀ (j : ι), j ≠ i → 0 ≤ f j<GOAL>f i ≤ ∑' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Multipliable f<VAR>i : ι<VAR>hb : ∀ (j : ι), j ≠ i → 1 ≤ f j<GOAL>f i ≤ ∏' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i ≤ g i<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>∏' (i : ι), f i ≤ ∏' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>h : ∀ (i : ι), f i ≤ g i<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>∑' (i : ι), f i ≤ ∑' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>h : f ≤ g<GOAL>∑' (n : ι), f n ≤ ∑' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<VAR>h : f ≤ g<GOAL>∏' (n : ι), f n ≤ ∏' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₂ : α<VAR>hf : Multipliable f<VAR>h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂<GOAL>∏' (i : ι), f i ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₂ : α<VAR>hf : Summable f<VAR>h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂<GOAL>∑' (i : ι), f i ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₂ : α<VAR>ha₂ : 1 ≤ a₂<VAR>h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂<GOAL>∏' (i : ι), f i ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a₂ : α<VAR>ha₂ : 0 ≤ a₂<VAR>h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂<GOAL>∑' (i : ι), f i ≤ a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), 1 ≤ g i<VAR>ha : HasProd g a<GOAL>1 ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), 0 ≤ g i<VAR>ha : HasSum g a<GOAL>0 ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), g i ≤ 0<VAR>ha : HasSum g a<GOAL>a ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>a : α<VAR>h : ∀ (i : ι), g i ≤ 1<VAR>ha : HasProd g a<GOAL>a ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>h : ∀ (i : ι), 0 ≤ g i<GOAL>0 ≤ ∑' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>h : ∀ (i : ι), 1 ≤ g i<GOAL>1 ≤ ∏' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>h : ∀ (i : ι), f i ≤ 1<GOAL>∏' (i : ι), f i ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>h : ∀ (i : ι), f i ≤ 0<GOAL>∑' (i : ι), f i ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>HasSum f 0 ↔ f = 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : ∀ (i : ι), 1 ≤ f i<GOAL>HasProd f 1 ↔ f = 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<VAR>h : f < g<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<VAR>h : f < g<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>∑' (n : ι), f n < ∑' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>∏' (n : ι), f n < ∏' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<VAR>h : f < g<GOAL>∏' (n : ι), f n < ∏' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>OrderClosedTopology α<VAR>f g : ι → α<VAR>hf : Summable f<VAR>hg : Summable g<VAR>h : f < g<GOAL>∑' (n : ι), f n < ∑' (n : ι), g n
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>hsum : Summable g<VAR>hg : ∀ (i : ι), 0 ≤ g i<VAR>i : ι<VAR>hi : 0 < g i<GOAL>0 < ∑' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>OrderedCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>OrderClosedTopology α<VAR>g : ι → α<VAR>hsum : Multipliable g<VAR>hg : ∀ (i : ι), 1 ≤ g i<VAR>i : ι<VAR>hi : 1 < g i<GOAL>1 < ∏' (i : ι), g i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasSum f a<VAR>i : ι<GOAL>f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasProd f a<VAR>i : ι<GOAL>f i ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Summable f<VAR>i : ι<GOAL>f i ≤ ∑' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Multipliable f<VAR>i : ι<GOAL>f i ≤ ∏' (i : ι), f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<GOAL>HasSum f 0 ↔ ∀ (x : ι), f x = 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<GOAL>HasProd f 1 ↔ ∀ (x : ι), f x = 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Summable f<GOAL>∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Multipliable f<GOAL>∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Summable f<GOAL>∑' (i : ι), f i ≠ 0 ↔ ∃ x, f x ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>hf : Multipliable f<GOAL>∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasSum f a<GOAL>IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : HasProd f a<GOAL>IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : ι → α<VAR>i : α<VAR>h : ∀ (i : ι), 0 ≤ f i<VAR>hf : IsLUB (Set.range fun s => ∑ i ∈ s, f i) i<GOAL>HasSum f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : ι → α<VAR>i : α<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>hf : IsLUB (Set.range fun s => ∏ i ∈ s, f i) i<GOAL>HasProd f i
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyLinearOrderedCommMonoid α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : ι → α<VAR>b : α<VAR>hf : IsLUB (Set.range fun s => ∏ i ∈ s, f i) b<GOAL>HasProd f b
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : ι → α<VAR>b : α<VAR>hf : IsLUB (Set.range fun s => ∑ i ∈ s, f i) b<GOAL>HasSum f b
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>f : ι → α<GOAL>(Summable fun x => |f x|) ↔ Summable f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedCommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>f : ι → α<GOAL>(Multipliable fun x => mabs (f x)) ↔ Multipliable f
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>Archimedean α<VAR>OrderClosedTopology α<VAR>b : α<VAR>hb : 0 < b<VAR>hf : Summable fun x => b<GOAL>Finite ι
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<VAR>TopologicalSpace α<VAR>Archimedean α<VAR>OrderClosedTopology α<VAR>b : α<VAR>hb : 0 < b<VAR>hf : Summable fun x => b<GOAL>Set.univ.Finite
<VAR>α : Type u_3<VAR>LinearOrderedField α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : ℕ → α<VAR>hf : Summable f⁻¹<VAR>hf' : ∀ (n : ℕ), 0 < f n<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop
<VAR>α : Type u_7<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : BoundedLENhdsClass α<VAR>a : α<GOAL>Filter.IsBounded (fun x x_1 => x ≤ x_1) (𝓝 a)
<VAR>α : Type u_7<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : BoundedGENhdsClass α<VAR>a : α<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) (𝓝 a)
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>a : α<GOAL>Filter.IsBounded (fun x x_1 => x ≤ x_1) (𝓝 a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>f : Filter ι<VAR>u : ι → α<VAR>a : α<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>u : ι → α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>h : Filter.Tendsto u Filter.cofinite (𝓝 a)<GOAL>BddAbove (Set.range u)
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>u : ℕ → α<VAR>h : Filter.Tendsto u Filter.atTop (𝓝 a)<GOAL>BddAbove (Set.range u)
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>a : α<GOAL>Filter.IsCobounded (fun x x_1 => x ≥ x_1) (𝓝 a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedLENhdsClass α<VAR>f : Filter ι<VAR>u : ι → α<VAR>a : α<VAR>f.NeBot<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>a : α<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) (𝓝 a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>f : Filter ι<VAR>u : ι → α<VAR>a : α<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>u : ι → α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>h : Filter.Tendsto u Filter.cofinite (𝓝 a)<GOAL>BddBelow (Set.range u)
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>a : α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>u : ℕ → α<VAR>h : Filter.Tendsto u Filter.atTop (𝓝 a)<GOAL>BddBelow (Set.range u)
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>a : α<GOAL>Filter.IsCobounded (fun x x_1 => x ≤ x_1) (𝓝 a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>BoundedGENhdsClass α<VAR>f : Filter ι<VAR>u : ι → α<VAR>a : α<VAR>f.NeBot<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter α<VAR>a : α<VAR>hl : Filter.IsBounded (fun x x_1 => x ≤ x_1) f<VAR>hg : Filter.IsBounded (fun x x_1 => x ≥ x_1) f<VAR>hs : f.limsSup = a<VAR>hi : f.limsInf = a<GOAL>f ≤ 𝓝 a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<GOAL>(𝓝 a).limsSup = a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<GOAL>(𝓝 a).limsInf = a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter α<VAR>a : α<VAR>f.NeBot<VAR>h : f ≤ 𝓝 a<GOAL>f.limsInf = a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter α<VAR>a : α<VAR>f.NeBot<GOAL>f ≤ 𝓝 a → f.limsSup = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>f.NeBot<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.limsup u f = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>f.NeBot<VAR>h : Filter.Tendsto u f (𝓝 a)<GOAL>Filter.liminf u f = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hinf : Filter.liminf u f = a<VAR>hsup : Filter.limsup u f = a<VAR>h : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<VAR>h' : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>Filter.Tendsto u f (𝓝 a)