ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<VAR>hinf : a ≤ Filter.liminf u f<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)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>f : Filter β<VAR>u : β → α<VAR>s : Set α<VAR>hs : Dense s<VAR>H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)<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>∃ c, Filter.Tendsto u f (𝓝 c)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>FirstCountableTopology α<VAR>f : Filter β<VAR>CountableInterFilter f<VAR>u : β → α<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u := by isBoundedDefault<GOAL>∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>FirstCountableTopology α<VAR>f : Filter β<VAR>CountableInterFilter f<VAR>u : β → α<VAR>hf : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u := by isBoundedDefault<GOAL>∀ᶠ (b : β) in f, Filter.liminf u f ≤ u b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>FirstCountableTopology α<VAR>OrderTopology α<VAR>f : Filter β<VAR>CountableInterFilter f<VAR>u : β → α<GOAL>Filter.limsup u f = ⊥ ↔ u =ᶠ[f] ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>FirstCountableTopology α<VAR>OrderTopology α<VAR>f : Filter β<VAR>CountableInterFilter f<VAR>u : β → α<GOAL>Filter.liminf u f = ⊤ ↔ u =ᶠ[f] ⊤
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>F : Filter R<VAR>F.NeBot<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>f_cont : ContinuousAt f F.limsSup<VAR>bdd_above : Filter.IsBounded (fun x x_1 => x ≤ x_1) F := by isBoundedDefault<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≤ x_1) F := by isBoundedDefault<GOAL>f F.limsSup = Filter.liminf f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>a : ι → R<VAR>f_cont : ContinuousAt f (Filter.limsup a F)<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a := by isBoundedDefault<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F a := by isBoundedDefault<GOAL>f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>F : Filter R<VAR>F.NeBot<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>f_cont : ContinuousAt f F.limsInf<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≥ x_1) F := by isBoundedDefault<VAR>bdd_below : Filter.IsBounded (fun x x_1 => x ≥ x_1) F := by isBoundedDefault<GOAL>f F.limsInf = Filter.limsup f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>a : ι → R<VAR>f_cont : ContinuousAt f (Filter.liminf a F)<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F a := by isBoundedDefault<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a := by isBoundedDefault<GOAL>f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>F : Filter R<VAR>F.NeBot<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>f_cont : ContinuousAt f F.limsSup<VAR>bdd_above : Filter.IsBounded (fun x x_1 => x ≤ x_1) F := by isBoundedDefault<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≤ x_1) F := by isBoundedDefault<GOAL>f F.limsSup = Filter.limsup f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>a : ι → R<VAR>f_cont : ContinuousAt f (Filter.limsup a F)<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a := by isBoundedDefault<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F a := by isBoundedDefault<GOAL>f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>F : Filter R<VAR>F.NeBot<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>f_cont : ContinuousAt f F.limsInf<VAR>cobdd : Filter.IsCobounded (fun x x_1 => x ≥ x_1) F := by isBoundedDefault<VAR>bdd_below : Filter.IsBounded (fun x x_1 => x ≥ x_1) F := by isBoundedDefault<GOAL>f F.limsInf = Filter.liminf f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Filter ι<VAR>F.NeBot<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>ConditionallyCompleteLinearOrder S<VAR>TopologicalSpace S<VAR>OrderTopology S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>a : ι → R<VAR>f_cont : ContinuousAt f (Filter.liminf a F)<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F a := by isBoundedDefault<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a := by isBoundedDefault<GOAL>f (Filter.liminf a F) = Filter.liminf (f ∘ a) F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_le : ∀ (i : ι), x ≤ as i<VAR>F : Filter ι<VAR>F.NeBot<VAR>as_lim : Filter.Tendsto as F (𝓝 x)<GOAL>⨅ i, as i = x
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>le_x : ∀ (i : ι), as i ≤ x<VAR>F : Filter ι<VAR>F.NeBot<VAR>as_lim : Filter.Tendsto as F (𝓝 x)<GOAL>⨆ i, as i = x
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_lt : ∀ (i : ι), x < as i<VAR>F : Filter ι<VAR>F.NeBot<VAR>as_lim : Filter.Tendsto as F (𝓝 x)<GOAL>⋃ i, Set.Ici (as i) = Set.Ioi x
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>lt_x : ∀ (i : ι), as i < x<VAR>F : Filter ι<VAR>F.NeBot<VAR>as_lim : Filter.Tendsto as F (𝓝 x)<GOAL>⋃ i, Set.Iic (as i) = Set.Iio x
<VAR>α : Type u_2<VAR>s : ℕ → Set α<GOAL>Filter.limsup s Filter.atTop = {ω | Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop}
<VAR>α : Type u_2<VAR>R : Type u_7<VAR>StrictOrderedSemiring R<VAR>Archimedean R<VAR>s : ℕ → Set α<GOAL>Filter.limsup s Filter.atTop = {ω | Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop}
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>Add R<VAR>ContinuousAdd R<VAR>CovariantClass R R (fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f<GOAL>Filter.limsup (fun i => c + f i) F = c + Filter.limsup f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>Add R<VAR>ContinuousAdd R<VAR>CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f<GOAL>Filter.limsup (fun i => f i + c) F = Filter.limsup f F + c
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>Add R<VAR>ContinuousAdd R<VAR>CovariantClass R R (fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f<GOAL>Filter.liminf (fun i => c + f i) F = c + Filter.liminf f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>Add R<VAR>ContinuousAdd R<VAR>CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f<GOAL>Filter.liminf (fun i => f i + c) F = Filter.liminf f F + c
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>AddCommSemigroup R<VAR>Sub R<VAR>ContinuousSub R<VAR>OrderedSub R<VAR>CovariantClass R R (fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f<GOAL>Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>AddCommSemigroup R<VAR>Sub R<VAR>ContinuousSub R<VAR>OrderedSub R<VAR>f : ι → R<VAR>c : R<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f<GOAL>Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>AddCommSemigroup R<VAR>Sub R<VAR>ContinuousSub R<VAR>OrderedSub R<VAR>CovariantClass R R (fun x y => x + y) fun x y => x ≤ y<VAR>f : ι → R<VAR>c : R<VAR>bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f<GOAL>Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>ConditionallyCompleteLinearOrder R<VAR>TopologicalSpace R<VAR>OrderTopology R<VAR>F : Filter ι<VAR>F.NeBot<VAR>AddCommSemigroup R<VAR>Sub R<VAR>ContinuousSub R<VAR>OrderedSub R<VAR>f : ι → R<VAR>c : R<VAR>cobdd : Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) F f<VAR>bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f<GOAL>Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>Ring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>ContinuousSMul R M<VAR>Module R N<VAR>ContinuousAdd M<VAR>IsSimpleModule R N<VAR>l : M →ₗ[R] N<GOAL>IsClosed ↑(LinearMap.ker l) ∨ Dense ↑(LinearMap.ker l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>DecidableEq β<VAR>b : β<VAR>a : α<GOAL>HasProd (Pi.mulSingle b a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>DecidableEq β<VAR>b : β<VAR>a : α<GOAL>HasSum (Pi.single b a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>DecidableEq β<VAR>b : β<VAR>a : α<GOAL>∑' (b' : β), Pi.single b a b' = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>DecidableEq β<VAR>b : β<VAR>a : α<GOAL>∏' (b' : β), Pi.mulSingle b a b' = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>t : Set γ<VAR>f : β × γ → α<GOAL>∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>t : Set γ<VAR>f : β × γ → α<GOAL>∑' (x : ↑({b} ×ˢ t)), f ↑x = ∑' (c : ↑t), f (b, ↑c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>c : γ<VAR>f : β × γ → α<GOAL>∑' (x : ↑(s ×ˢ {c})), f ↑x = ∑' (b : ↑s), f (↑b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>c : γ<VAR>f : β × γ → α<GOAL>∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β × γ → α<VAR>hf : Multipliable f<GOAL>Multipliable fun p => f p.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β × γ → α<VAR>hf : Summable f<GOAL>Summable fun p => f p.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>f : β → α<VAR>g : β → γ<VAR>a : α<VAR>b : γ<VAR>hf : HasProd f a<VAR>hg : HasProd g b<GOAL>HasProd (fun x => (f x, g x)) (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>f : β → α<VAR>g : β → γ<VAR>a : α<VAR>b : γ<VAR>hf : HasSum f a<VAR>hg : HasSum g b<GOAL>HasSum (fun x => (f x, g x)) (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>RegularSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasProd f a<VAR>hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)<GOAL>HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>RegularSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasSum f a<VAR>hf : ∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)<GOAL>HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>RegularSpace α<VAR>f : β × γ → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasProd f a<VAR>hf : ∀ (b : β), HasProd (fun c => f (b, c)) (g b)<GOAL>HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>RegularSpace α<VAR>f : β × γ → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasSum f a<VAR>hf : ∀ (b : β), HasSum (fun c => f (b, c)) (g b)<GOAL>HasSum g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>RegularSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Summable f<VAR>hf : ∀ (b : β), Summable fun c => f ⟨b, c⟩<GOAL>Summable fun b => ∑' (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>RegularSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Multipliable f<VAR>hf : ∀ (b : β), Multipliable fun c => f ⟨b, c⟩<GOAL>Multipliable fun b => ∏' (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>T3Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasProd g a<VAR>hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)<VAR>hf' : Multipliable f<GOAL>HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>T3Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>g : β → α<VAR>a : α<VAR>ha : HasSum g a<VAR>hf : ∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)<VAR>hf' : Summable f<GOAL>HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>T3Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>h₁ : ∀ (b : β), Summable fun c => f ⟨b, c⟩<VAR>h₂ : Summable f<GOAL>∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>T3Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>h₁ : ∀ (b : β), Multipliable fun c => f ⟨b, c⟩<VAR>h₂ : Multipliable f<GOAL>∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>T3Space α<VAR>f : β × γ → α<VAR>h : Multipliable f<VAR>h₁ : ∀ (b : β), Multipliable fun c => f (b, c)<GOAL>∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>T3Space α<VAR>f : β × γ → α<VAR>h : Summable f<VAR>h₁ : ∀ (b : β), Summable fun c => f (b, c)<GOAL>∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>T3Space α<VAR>f : β → γ → α<VAR>h : Multipliable (Function.uncurry f)<VAR>h₁ : ∀ (b : β), Multipliable (f b)<VAR>h₂ : ∀ (c : γ), Multipliable fun b => f b c<GOAL>∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>T3Space α<VAR>f : β → γ → α<VAR>h : Summable (Function.uncurry f)<VAR>h₁ : ∀ (b : β), Summable (f b)<VAR>h₂ : ∀ (c : γ), Summable fun b => f b c<GOAL>∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Summable f<VAR>b : β<GOAL>Summable fun c => f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Multipliable f<VAR>b : β<GOAL>Multipliable fun c => f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Multipliable f<GOAL>Multipliable fun b => ∏' (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Summable f<GOAL>Summable fun b => ∑' (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>f : β × γ → α<VAR>h : Multipliable f<VAR>b : β<GOAL>Multipliable fun c => f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>f : β × γ → α<VAR>h : Summable f<VAR>b : β<GOAL>Summable fun c => f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>g : β → γ<GOAL>HasProd (fun c => ∏' (b : ↑(g ⁻¹' {c})), f ↑b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T2Space α<VAR>f : β → α<VAR>a : α<VAR>hf : HasSum f a<VAR>g : β → γ<GOAL>HasSum (fun c => ∑' (b : ↑(g ⁻¹' {c})), f ↑b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Multipliable f<GOAL>∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>γ : β → Type u_5<VAR>f : (b : β) × γ b → α<VAR>ha : Summable f<GOAL>∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>f : β × γ → α<VAR>h : Multipliable f<GOAL>∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>f : β × γ → α<VAR>h : Summable f<GOAL>∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommGroup α<VAR>UniformSpace α<VAR>UniformGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>f : β → γ → α<VAR>h : Multipliable (Function.uncurry f)<GOAL>∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup α<VAR>UniformSpace α<VAR>UniformAddGroup α<VAR>CompleteSpace α<VAR>T0Space α<VAR>f : β → γ → α<VAR>h : Summable (Function.uncurry f)<GOAL>∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → AddCommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<VAR>g : (x : α) → π x<GOAL>HasSum f g ↔ ∀ (x : α), HasSum (fun i => f i x) (g x)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → CommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<VAR>g : (x : α) → π x<GOAL>HasProd f g ↔ ∀ (x : α), HasProd (fun i => f i x) (g x)
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → CommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<GOAL>Multipliable f ↔ ∀ (x : α), Multipliable fun i => f i x
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → AddCommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<GOAL>Summable f ↔ ∀ (x : α), Summable fun i => f i x
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → AddCommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>∀ (x : α), T2Space (π x)<VAR>f : ι → (x : α) → π x<VAR>x : α<VAR>hf : Summable f<GOAL>tsum (fun i => f i) x = ∑' (i : ι), f i x
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>(x : α) → CommMonoid (π x)<VAR>(x : α) → TopologicalSpace (π x)<VAR>∀ (x : α), T2Space (π x)<VAR>f : ι → (x : α) → π x<VAR>x : α<VAR>hf : Multipliable f<GOAL>tprod (fun i => f i) x = ∏' (i : ι), f i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>hf : HasSum f a<GOAL>HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>hf : Summable f<GOAL>Summable (MulOpposite.op ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → αᵐᵒᵖ<VAR>a : αᵐᵒᵖ<VAR>hf : HasSum f a<GOAL>HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → αᵐᵒᵖ<VAR>hf : Summable f<GOAL>Summable (MulOpposite.unop ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<GOAL>HasSum (fun a => MulOpposite.op (f a)) (MulOpposite.op a) ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → αᵐᵒᵖ<VAR>a : αᵐᵒᵖ<GOAL>HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a) ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<GOAL>(Summable fun a => MulOpposite.op (f a)) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → αᵐᵒᵖ<GOAL>(Summable fun a => MulOpposite.unop (f a)) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>T2Space α<GOAL>∑' (x : β), MulOpposite.op (f x) = MulOpposite.op (∑' (x : β), f x)