ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a : α<VAR>s : Finset β<GOAL>HasProd (fun x => f ↑x) a ↔ HasProd f (a * ∏ i ∈ s, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a : α<VAR>s : Finset β<GOAL>HasSum (fun x => f ↑x) a ↔ HasSum f (a + ∑ i ∈ s, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a : α<VAR>s : Finset β<GOAL>HasProd f a ↔ HasProd (fun x => f ↑x) (a / ∏ i ∈ s, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a : α<VAR>s : Finset β<GOAL>HasSum f a ↔ HasSum (fun x => f ↑x) (a - ∑ i ∈ s, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>s : Finset β<GOAL>(Summable fun x => f ↑x) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>s : Finset β<GOAL>(Multipliable fun x => f ↑x) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>s : Set β<VAR>hs : s.Finite<GOAL>Multipliable (f ∘ Subtype.val) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>s : Set β<VAR>hs : s.Finite<GOAL>Summable (f ∘ Subtype.val) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a : α<VAR>DecidableEq β<VAR>hf : HasProd f a<VAR>b : β<GOAL>HasProd (fun n => if n = b then 1 else f n) (a / f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a : α<VAR>DecidableEq β<VAR>hf : HasSum f a<VAR>b : β<GOAL>HasSum (fun n => if n = b then 0 else f n) (a - f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>T2Space α<GOAL>∑' (b : β), -f b = -∑' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>T2Space α<GOAL>∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f g : β → α<VAR>T2Space α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>∏' (b : β), f b / g b = (∏' (b : β), f b) / ∏' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f g : β → α<VAR>T2Space α<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>∑' (b : β), (f b - g b) = ∑' (b : β), f b - ∑' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>T2Space α<VAR>s : Finset β<VAR>hf : Summable f<GOAL>∑ x ∈ s, f x + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>T2Space α<VAR>s : Finset β<VAR>hf : Multipliable f<GOAL>(∏ x ∈ s, f x) * ∏' (x : ↑(↑s)ᶜ), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>T2Space α<VAR>DecidableEq β<VAR>hf : Summable f<VAR>b : β<GOAL>∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>T2Space α<VAR>DecidableEq β<VAR>hf : Multipliable f<VAR>b : β<GOAL>∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>CompleteSpace α<VAR>f : β → α<GOAL>Multipliable f ↔ CauchySeq fun s => ∏ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>CompleteSpace α<VAR>f : β → α<GOAL>Summable f ↔ CauchySeq fun s => ∑ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<GOAL>(CauchySeq fun s => ∑ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 0, ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<GOAL>(CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<GOAL>(CauchySeq fun s => ∑ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 0, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<GOAL>(CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<GOAL>Summable f ↔ ∀ e ∈ 𝓝 0, ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<GOAL>Summable f ↔ ∀ e ∈ 𝓝 0, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f g : β → α<VAR>CompleteSpace α<VAR>hf : Multipliable f<VAR>h : ∀ (b : β), g b = 1 ∨ g b = f b<GOAL>Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f g : β → α<VAR>CompleteSpace α<VAR>hf : Summable f<VAR>h : ∀ (b : β), g b = 0 ∨ g b = f b<GOAL>Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>hf : Summable f<VAR>s : Set β<GOAL>Summable (s.indicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>hf : Multipliable f<VAR>s : Set β<GOAL>Multipliable (s.mulIndicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>i : γ → β<VAR>hf : Summable f<VAR>hi : Function.Injective i<GOAL>Summable (f ∘ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>i : γ → β<VAR>hf : Multipliable f<VAR>hi : Function.Injective i<GOAL>Multipliable (f ∘ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>hf : Multipliable f<VAR>s : Set β<GOAL>Multipliable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>hf : Summable f<VAR>s : Set β<GOAL>Summable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>s : Set β<GOAL>((Summable fun x => f ↑x) ∧ Summable fun x => f ↑x) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>f : β → α<VAR>CompleteSpace α<VAR>s : Set β<GOAL>((Multipliable fun x => f ↑x) ∧ Multipliable fun x => f ↑x) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>hf : Summable f<VAR>s : Set β<GOAL>∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>s : Set β<GOAL>(∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>hf : Summable f<VAR>s : Finset β<GOAL>∑ x ∈ s, f x + ∑' (x : { x // x ∉ s }), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>s : Finset β<GOAL>(∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>f : α → G<VAR>hf : Summable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 0<GOAL>∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k ∈ t, f k ∈ e
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>f : α → G<VAR>hf : Summable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 0<GOAL>∃ s, ∀ (t : Set α), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>f : α → G<GOAL>Filter.Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>f : α → G<GOAL>Filter.Tendsto (fun s => ∑' (a : { x // x ∉ s }), f ↑a) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>f : α → G<VAR>hf : Summable f<GOAL>Filter.Tendsto f Filter.cofinite (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<GOAL>Filter.Tendsto f Filter.cofinite (𝓝 1)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>f : α → G<VAR>FirstCountableTopology G<VAR>T1Space G<VAR>hf : Multipliable f<GOAL>(Function.mulSupport f).Countable
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>f : α → G<VAR>FirstCountableTopology G<VAR>T1Space G<VAR>hf : Summable f<GOAL>(Function.support f).Countable
<VAR>β : Type u_2<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>Infinite β<VAR>T2Space G<VAR>a : G<GOAL>(Multipliable fun x => a) ↔ a = 1
<VAR>β : Type u_2<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>Infinite β<VAR>T2Space G<VAR>a : G<GOAL>(Summable fun x => a) ↔ a = 0
<VAR>β : Type u_2<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>AddCommGroup G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>a : G<GOAL>∑' (x : β), a = Nat.card β • a
<VAR>β : Type u_2<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>CommGroup G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>a : G<GOAL>∏' (x : β), a = a ^ Nat.card β
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>f : ContinuousMonoidHom A B<VAR>x : PontryaginDual B<VAR>y : A<GOAL>((PontryaginDual.map f) x) y = x (f y)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>PontryaginDual.map (ContinuousMonoidHom.one A B) = ContinuousMonoidHom.one (PontryaginDual B) (PontryaginDual A)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>g : ContinuousMonoidHom B C<VAR>f : ContinuousMonoidHom A B<GOAL>PontryaginDual.map (g.comp f) = (PontryaginDual.map f).comp (PontryaginDual.map g)
<VAR>A : Type u_1<VAR>E : Type u_5<VAR>Monoid A<VAR>CommGroup E<VAR>TopologicalSpace A<VAR>TopologicalSpace E<VAR>TopologicalGroup E<VAR>f g : ContinuousMonoidHom A E<GOAL>PontryaginDual.map (f * g) = PontryaginDual.map f * PontryaginDual.map g
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>Valued K Γ₀<GOAL>Continuous ⇑Valued.v
<VAR>K : Type u_1<VAR>Field K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<GOAL>Continuous Valued.extension
<VAR>K : Type u_1<VAR>Field K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x : K<GOAL>Valued.extension (↑K x) = Valued.v x
<VAR>K : Type u_1<VAR>Field K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>γ : Γ₀ˣ<GOAL>closure (↑K '' {x | Valued.v x < ↑γ}) = {x | Valued.extensionValuation x < ↑γ}
<VAR>K : Type u_1<VAR>Field K<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x : K<GOAL>Valued.v (↑K x) = Valued.v x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<GOAL>HasProd (fun x => 1) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<GOAL>HasSum (fun x => 0) 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>HasSum f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>HasProd f 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<GOAL>Summable fun x => 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<GOAL>Multipliable fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hfg : ∀ (b : β), f b = g b<GOAL>Multipliable f ↔ Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hfg : ∀ (b : β), f b = g b<GOAL>Summable f ↔ Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hf : Summable f<VAR>hfg : ∀ (b : β), f b = g b<GOAL>Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hf : Multipliable f<VAR>hfg : ∀ (b : β), f b = g b<GOAL>Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>a : α<VAR>hf : HasSum f a<VAR>h : ∀ (x : β), g x = f x<GOAL>HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>h : ∀ (x : β), g x = f x<GOAL>HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b<VAR>hf : HasProd g a<GOAL>HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b<VAR>hf : HasSum g a<GOAL>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>h₁ : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b<VAR>h₂ : ∀ (v : Finset β), ∃ u, ∀ (u' : Finset γ), u ⊆ u' → ∃ v', v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x<GOAL>HasProd f a ↔ HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>h₁ : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b<VAR>h₂ : ∀ (v : Finset β), ∃ u, ∀ (u' : Finset γ), u ⊆ u' → ∃ v', v ⊆ v' ∧ ∑ b ∈ v', f b = ∑ x ∈ u', g x<GOAL>HasSum f a ↔ HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>hf : ∀ x ∉ Set.range g, f x = 0<GOAL>Summable (f ∘ g) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>hf : ∀ x ∉ Set.range g, f x = 1<GOAL>Multipliable (f ∘ g) ↔ Multipliable f
<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<GOAL>HasProd (Function.extend g f 1) a ↔ HasProd f a
<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<GOAL>HasSum (Function.extend g f 0) a ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : β → γ<VAR>hg : Function.Injective g<GOAL>Summable (Function.extend g f 0) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : β → γ<VAR>hg : Function.Injective g<GOAL>Multipliable (Function.extend g f 1) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set β<GOAL>HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set β<GOAL>HasSum (f ∘ Subtype.val) a ↔ HasSum (s.indicator f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<GOAL>Multipliable (f ∘ Subtype.val) ↔ Multipliable (s.mulIndicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<GOAL>Summable (f ∘ Subtype.val) ↔ Summable (s.indicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<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 : α<GOAL>HasProd (f ∘ Subtype.val) a ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>Summable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>Multipliable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>hs : s.Finite<VAR>f : β → α<GOAL>Multipliable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>hs : s.Finite<VAR>f : β → α<GOAL>Summable (f ∘ Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>h : (Function.support f).Finite<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>h : (Function.mulSupport f).Finite<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>Finite β<VAR>f : β → α<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>Finite β<VAR>f : β → α<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 0<GOAL>HasSum f (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 1<GOAL>HasProd f (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>Unique β<VAR>f : β → α<GOAL>HasSum f (f default)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>Unique β<VAR>f : β → α<GOAL>HasProd f (f default)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>m : β<VAR>f : β → α<GOAL>HasSum ({m}.restrict f) (f m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>m : β<VAR>f : β → α<GOAL>HasProd ({m}.restrict f) (f m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>DecidablePred fun x => x = b<VAR>a : α<GOAL>HasSum (fun b' => if b' = b then a else 0) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>DecidablePred fun x => x = b<VAR>a : α<GOAL>HasProd (fun b' => if b' = b then a else 1) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>e : γ ≃ β<GOAL>HasSum (f ∘ ⇑e) 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>e : γ ≃ β<GOAL>HasProd (f ∘ ⇑e) a ↔ HasProd 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<GOAL>HasProd (fun x => f ↑x) a ↔ HasProd (f ∘ g) a
<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<GOAL>HasSum (fun x => f ↑x) a ↔ HasSum (f ∘ g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>e : γ ≃ β<GOAL>Summable (f ∘ ⇑e) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>e : γ ≃ β<GOAL>Multipliable (f ∘ ⇑e) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)<VAR>he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x<GOAL>HasProd f a ↔ HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>e : ↑(Function.support f) ≃ ↑(Function.support g)<VAR>he : ∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x<GOAL>HasSum f a ↔ HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>i : ↑(Function.mulSupport g) → β<VAR>hi : Function.Injective i<VAR>hf : Function.mulSupport f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(Function.mulSupport g)), f (i x) = g ↑x<GOAL>HasProd f a ↔ HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>g : γ → α<VAR>i : ↑(Function.support g) → β<VAR>hi : Function.Injective i<VAR>hf : Function.support f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(Function.support g)), f (i x) = g ↑x<GOAL>HasSum f a ↔ HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)<VAR>he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x<GOAL>Multipliable f ↔ Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>e : ↑(Function.support f) ≃ ↑(Function.support g)<VAR>he : ∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x<GOAL>Summable f ↔ Summable g