ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<VAR>E : Type u_5<VAR>Zero E<VAR>MulActionWithZero G₀ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>ContinuousConstSMul G₀ E<VAR>c : G₀<VAR>s : Set E<GOAL>closure (c • s) = c • closure s
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>IsClosedMap fun x => c • x
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>hs : IsClosed s<VAR>hc : c ≠ 0<GOAL>IsClosed (c • s)
<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<VAR>E : Type u_5<VAR>Zero E<VAR>MulActionWithZero G₀ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>ContinuousConstSMul G₀ E<VAR>c : G₀<GOAL>IsClosedMap fun x => c • x
<VAR>G₀ : Type u_4<VAR>GroupWithZero G₀<VAR>E : Type u_5<VAR>Zero E<VAR>MulActionWithZero G₀ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>ContinuousConstSMul G₀ E<VAR>c : G₀<VAR>s : Set E<VAR>hs : IsClosed s<GOAL>IsClosed (c • s)
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>β : Type u_5<VAR>One β<VAR>f : α → β<VAR>h : HasCompactMulSupport f<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>HasCompactMulSupport fun x => f (c • x)
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>β : Type u_5<VAR>Zero β<VAR>f : α → β<VAR>h : HasCompactSupport f<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>HasCompactSupport fun x => f (c • x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>c : M<VAR>hc : IsUnit c<GOAL>Filter.Tendsto (fun x => c • f x) l (𝓝 (c • a)) ↔ Filter.Tendsto f l (𝓝 a)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : M<VAR>s : Set β<VAR>hc : IsUnit c<GOAL>ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : M<VAR>s : Set β<VAR>hc : IsUnit c<GOAL>ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : M<VAR>hc : IsUnit c<GOAL>ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : M<VAR>hc : IsUnit c<GOAL>(Continuous fun x => c • f x) ↔ Continuous f
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>c : M<VAR>hc : IsUnit c<GOAL>IsOpenMap fun x => c • x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>c : M<VAR>hc : IsUnit c<GOAL>IsClosedMap fun x => c • x
<VAR>Γ : Type u_4<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>SMul Γ T<VAR>self : ProperlyDiscontinuousSMul Γ T<VAR>K L : Set T<GOAL>IsCompact K → IsCompact L → {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>Γ : Type u_4<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>VAdd Γ T<VAR>self : ProperlyDiscontinuousVAdd Γ T<VAR>K L : Set T<GOAL>IsCompact K → IsCompact L → {γ | (fun x => γ +ᵥ x) '' K ∩ L ≠ ∅}.Finite
<VAR>Γ : Type u_4<VAR>AddGroup Γ<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>AddAction Γ T<VAR>ContinuousConstVAdd Γ T<GOAL>IsOpenMap Quotient.mk'
<VAR>Γ : Type u_4<VAR>Group Γ<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>MulAction Γ T<VAR>ContinuousConstSMul Γ T<GOAL>IsOpenMap Quotient.mk'
<VAR>Γ : Type u_4<VAR>AddGroup Γ<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>AddAction Γ T<VAR>SecondCountableTopology T<VAR>ContinuousConstVAdd Γ T<GOAL>SecondCountableTopology (Quotient (AddAction.orbitRel Γ T))
<VAR>Γ : Type u_4<VAR>Group Γ<VAR>T : Type u_5<VAR>TopologicalSpace T<VAR>MulAction Γ T<VAR>SecondCountableTopology T<VAR>ContinuousConstSMul Γ T<GOAL>SecondCountableTopology (Quotient (MulAction.orbitRel Γ T))
<VAR>α : Type u_2<VAR>G₀ : Type u_6<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>x : α<VAR>hs : s ∈ 𝓝 x<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 (c • x)
<VAR>α : Type u_2<VAR>G₀ : Type u_6<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>x : α<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 (c • x) ↔ s ∈ 𝓝 x
<VAR>α : Type u_2<VAR>G₀ : Type u_6<VAR>GroupWithZero G₀<VAR>AddMonoid α<VAR>DistribMulAction G₀ α<VAR>TopologicalSpace α<VAR>ContinuousConstSMul G₀ α<VAR>s : Set α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>One M<GOAL>Continuous 1
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Zero M<GOAL>Continuous 0
<VAR>M : Type u<VAR>TopologicalSpace M<VAR>Add M<VAR>self : ContinuousAdd M<GOAL>Continuous fun p => p.1 + p.2
<VAR>M : Type u<VAR>TopologicalSpace M<VAR>Mul M<VAR>self : ContinuousMul M<GOAL>Continuous fun p => p.1 * p.2
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<GOAL>Continuous fun p => p.1 * p.2
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<GOAL>Continuous fun p => p.1 + p.2
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>FunLike F α β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>ContinuousMul β<VAR>f : F<GOAL>ContinuousMul α
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>FunLike F α β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddMonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>ContinuousAdd β<VAR>f : F<GOAL>ContinuousAdd α
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>f g : X → M<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x * g x
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>f g : X → M<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x + g x
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a : M<GOAL>Continuous fun b => a * b
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a : M<GOAL>Continuous fun b => a + b
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a : M<GOAL>Continuous fun b => b + a
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a : M<GOAL>Continuous fun b => b * a
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>f g : X → M<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x * g x) s
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>f g : X → M<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x + g x) s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a b : M<GOAL>Filter.Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a b : M<GOAL>Filter.Tendsto (fun p => p.1 + p.2) (𝓝 (a, b)) (𝓝 (a + b))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>f g : α → M<VAR>x : Filter α<VAR>a b : M<VAR>hf : Filter.Tendsto f x (𝓝 a)<VAR>hg : Filter.Tendsto g x (𝓝 b)<GOAL>Filter.Tendsto (fun x => f x * g x) x (𝓝 (a * b))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>f g : α → M<VAR>x : Filter α<VAR>a b : M<VAR>hf : Filter.Tendsto f x (𝓝 a)<VAR>hg : Filter.Tendsto g x (𝓝 b)<GOAL>Filter.Tendsto (fun x => f x + g x) x (𝓝 (a + b))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>b : M<VAR>c : M<VAR>f : α → M<VAR>l : Filter α<VAR>h : Filter.Tendsto (fun k => f k) l (𝓝 c)<GOAL>Filter.Tendsto (fun k => b * f k) l (𝓝 (b * c))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>b : M<VAR>c : M<VAR>f : α → M<VAR>l : Filter α<VAR>h : Filter.Tendsto (fun k => f k) l (𝓝 c)<GOAL>Filter.Tendsto (fun k => b + f k) l (𝓝 (b + c))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>b : M<VAR>c : M<VAR>f : α → M<VAR>l : Filter α<VAR>h : Filter.Tendsto (fun k => f k) l (𝓝 c)<GOAL>Filter.Tendsto (fun k => f k * b) l (𝓝 (c * b))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>b : M<VAR>c : M<VAR>f : α → M<VAR>l : Filter α<VAR>h : Filter.Tendsto (fun k => f k) l (𝓝 c)<GOAL>Filter.Tendsto (fun k => f k + b) l (𝓝 (c + b))
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a b : M<GOAL>𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a b : M<GOAL>𝓝 a + 𝓝 b ≤ 𝓝 (a + b)
<VAR>M : Type u_6<VAR>AddZeroClass M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>a : M<GOAL>𝓝 0 + 𝓝 a = 𝓝 a
<VAR>M : Type u_6<VAR>MulOneClass M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>a : M<GOAL>𝓝 1 * 𝓝 a = 𝓝 a
<VAR>M : Type u_6<VAR>MulOneClass M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>a : M<GOAL>𝓝 a * 𝓝 1 = 𝓝 a
<VAR>M : Type u_6<VAR>AddZeroClass M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>a : M<GOAL>𝓝 a + 𝓝 0 = 𝓝 a
<VAR>α : Type u_2<VAR>𝕜 : Type u_6<VAR>Preorder 𝕜<VAR>Zero 𝕜<VAR>Mul 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousMul 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>b c : 𝕜<VAR>hb : 0 < b<VAR>PosMulStrictMono 𝕜<VAR>PosMulReflectLT 𝕜<VAR>h : Filter.Tendsto f l (𝓝[>] c)<GOAL>Filter.Tendsto (fun a => b * f a) l (𝓝[>] (b * c))
<VAR>α : Type u_2<VAR>𝕜 : Type u_6<VAR>Preorder 𝕜<VAR>Zero 𝕜<VAR>Mul 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousMul 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>b c : 𝕜<VAR>hb : 0 < b<VAR>PosMulStrictMono 𝕜<VAR>PosMulReflectLT 𝕜<VAR>h : Filter.Tendsto f l (𝓝[<] c)<GOAL>Filter.Tendsto (fun a => b * f a) l (𝓝[<] (b * c))
<VAR>α : Type u_2<VAR>𝕜 : Type u_6<VAR>Preorder 𝕜<VAR>Zero 𝕜<VAR>Mul 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousMul 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>b c : 𝕜<VAR>hb : 0 < b<VAR>MulPosStrictMono 𝕜<VAR>MulPosReflectLT 𝕜<VAR>h : Filter.Tendsto f l (𝓝[>] c)<GOAL>Filter.Tendsto (fun a => f a * b) l (𝓝[>] (c * b))
<VAR>α : Type u_2<VAR>𝕜 : Type u_6<VAR>Preorder 𝕜<VAR>Zero 𝕜<VAR>Mul 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousMul 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>b c : 𝕜<VAR>hb : 0 < b<VAR>MulPosStrictMono 𝕜<VAR>MulPosReflectLT 𝕜<VAR>h : Filter.Tendsto f l (𝓝[<] c)<GOAL>Filter.Tendsto (fun a => f a * b) l (𝓝[<] (c * b))
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a b c d : M<VAR>hab : a ⤳ b<VAR>hcd : c ⤳ d<GOAL>(a * c) ⤳ (b * d)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a b c d : M<VAR>hab : a ⤳ b<VAR>hcd : c ⤳ d<GOAL>(a + c) ⤳ (b + d)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>a b c d : M<VAR>hab : Inseparable a b<VAR>hcd : Inseparable c d<GOAL>Inseparable (a + c) (b + d)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>a b c d : M<VAR>hab : Inseparable a b<VAR>hcd : Inseparable c d<GOAL>Inseparable (a * c) (b * d)
<VAR>M : Type u_6<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>a b : M<VAR>h : a ⤳ b<VAR>n : ℕ<GOAL>(a ^ n) ⤳ (b ^ n)
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>a b : M<VAR>h : a ⤳ b<VAR>n : ℕ<GOAL>(n • a) ⤳ (n • b)
<VAR>M : Type u_6<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>a b : M<VAR>h : Inseparable a b<VAR>n : ℕ<GOAL>Inseparable (a ^ n) (b ^ n)
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>a b : M<VAR>h : Inseparable a b<VAR>n : ℕ<GOAL>Inseparable (n • a) (n • b)
<VAR>ι : Type u_1<VAR>N : Type u_4<VAR>TopologicalSpace N<VAR>AddMonoid N<VAR>ContinuousAdd N<VAR>T2Space N<VAR>f : ι → AddUnits N<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>l.NeBot<VAR>h₁ : Filter.Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (𝓝 r₂)<GOAL>↑(h₁.addUnits h₂) = r₁
<VAR>ι : Type u_1<VAR>N : Type u_4<VAR>TopologicalSpace N<VAR>AddMonoid N<VAR>ContinuousAdd N<VAR>T2Space N<VAR>f : ι → AddUnits N<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>l.NeBot<VAR>h₁ : Filter.Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (𝓝 r₂)<GOAL>↑(-h₁.addUnits h₂) = r₂
<VAR>ι : Type u_1<VAR>N : Type u_4<VAR>TopologicalSpace N<VAR>Monoid N<VAR>ContinuousMul N<VAR>T2Space N<VAR>f : ι → Nˣ<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>l.NeBot<VAR>h₁ : Filter.Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)<GOAL>↑(h₁.units h₂)⁻¹ = r₂
<VAR>ι : Type u_1<VAR>N : Type u_4<VAR>TopologicalSpace N<VAR>Monoid N<VAR>ContinuousMul N<VAR>T2Space N<VAR>f : ι → Nˣ<VAR>r₁ r₂ : N<VAR>l : Filter ι<VAR>l.NeBot<VAR>h₁ : Filter.Tendsto (fun x => ↑(f x)) l (𝓝 r₁)<VAR>h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)<GOAL>↑(h₁.units h₂) = r₁
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>f g : X → M<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun x => f x + g x) x
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>f g : X → M<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun x => f x * g x) x
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Add M<VAR>ContinuousAdd M<VAR>f g : X → M<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun x => f x + g x) s x
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Mul M<VAR>ContinuousMul M<VAR>f g : X → M<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun x => f x * g x) s x
<VAR>M : Type u<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x + x₀) (𝓝 0)<GOAL>ContinuousAdd M
<VAR>M : Type u<VAR>Monoid M<VAR>TopologicalSpace M<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x * x₀) (𝓝 1)<GOAL>ContinuousMul M
<VAR>M : Type u<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<GOAL>ContinuousAdd M
<VAR>M : Type u<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun x => x₀ * x) (𝓝 1)<GOAL>ContinuousMul M
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>One M₁<VAR>One M₂<GOAL>IsClosed {f | f 1 = 1}
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Zero M₁<VAR>Zero M₂<GOAL>IsClosed {f | f 0 = 0}
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Mul M₁<VAR>Mul M₂<VAR>ContinuousMul M₂<GOAL>IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Add M₁<VAR>Add M₂<VAR>ContinuousAdd M₂<GOAL>IsClosed {f | ∀ (x y : M₁), f (x + y) = f x + f y}
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>AddZeroClass M₁<VAR>AddZeroClass M₂<VAR>ContinuousAdd M₂<VAR>F : Type u_8<VAR>FunLike F M₁ M₂<VAR>AddMonoidHomClass F M₁ M₂<VAR>f : M₁ → M₂<VAR>hf : f ∈ closure (Set.range fun f x => f x)<GOAL>⇑(addMonoidHomOfMemClosureRangeCoe f hf) = f
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>MulOneClass M₁<VAR>MulOneClass M₂<VAR>ContinuousMul M₂<VAR>F : Type u_8<VAR>FunLike F M₁ M₂<VAR>MonoidHomClass F M₁ M₂<VAR>f : M₁ → M₂<VAR>hf : f ∈ closure (Set.range fun f x => f x)<GOAL>⇑(monoidHomOfMemClosureRangeCoe f hf) = f
<VAR>α : Type u_2<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>AddZeroClass M₁<VAR>AddZeroClass M₂<VAR>ContinuousAdd M₂<VAR>F : Type u_8<VAR>FunLike F M₁ M₂<VAR>AddMonoidHomClass F M₁ M₂<VAR>l : Filter α<VAR>f : M₁ → M₂<VAR>g : α → F<VAR>l.NeBot<VAR>h : Filter.Tendsto (fun a x => (g a) x) l (𝓝 f)<GOAL>⇑(addMonoidHomOfTendsto f g h) = f
<VAR>α : Type u_2<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>MulOneClass M₁<VAR>MulOneClass M₂<VAR>ContinuousMul M₂<VAR>F : Type u_8<VAR>FunLike F M₁ M₂<VAR>MonoidHomClass F M₁ M₂<VAR>l : Filter α<VAR>f : M₁ → M₂<VAR>g : α → F<VAR>l.NeBot<VAR>h : Filter.Tendsto (fun a x => (g a) x) l (𝓝 f)<GOAL>⇑(monoidHomOfTendsto f g h) = f
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>AddZeroClass M₁<VAR>AddZeroClass M₂<VAR>ContinuousAdd M₂<GOAL>IsClosed (Set.range DFunLike.coe)
<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>MulOneClass M₁<VAR>MulOneClass M₂<VAR>ContinuousMul M₂<GOAL>IsClosed (Set.range DFunLike.coe)
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>F : Type u_8<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousMul N<VAR>f : F<VAR>hf : Inducing ⇑f<GOAL>ContinuousMul M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>F : Type u_8<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>f : F<VAR>hf : Inducing ⇑f<GOAL>ContinuousAdd M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>F : Type u_8<VAR>Mul M<VAR>Mul N<VAR>FunLike F M N<VAR>MulHomClass F M N<VAR>TopologicalSpace N<VAR>ContinuousMul N<VAR>f : F<GOAL>ContinuousMul M
<VAR>M : Type u_6<VAR>N : Type u_7<VAR>F : Type u_8<VAR>Add M<VAR>Add N<VAR>FunLike F M N<VAR>AddHomClass F M N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>f : F<GOAL>ContinuousAdd M
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>MulOneClass M<VAR>ContinuousMul M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 1<GOAL>∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddZeroClass M<VAR>ContinuousAdd M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 0<GOAL>∃ V, IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>MulOneClass M<VAR>ContinuousMul M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddZeroClass M<VAR>ContinuousAdd M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 0<GOAL>∃ V ∈ 𝓝 0, ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddZeroClass M<VAR>ContinuousAdd M<VAR>U : Set M<VAR>hU : U ∈ 𝓝 0<GOAL>∃ V, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>MulOneClass M<VAR>ContinuousMul M<VAR>U : Set M<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<GOAL>closure ↑s * closure ↑s ⊆ closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<GOAL>closure ↑s + closure ↑s ⊆ closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<GOAL>closure ↑s + closure ↑s = closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<GOAL>closure ↑s * closure ↑s = closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<GOAL>s ≤ s.topologicalClosure
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<GOAL>s ≤ s.topologicalClosure
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<GOAL>IsClosed ↑s.topologicalClosure
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<GOAL>IsClosed ↑s.topologicalClosure
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Submonoid M<VAR>t : Submonoid M<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid M<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>u : Set M<VAR>hu : u ∈ 𝓝 0<GOAL>∃ V ∈ 𝓝 0, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>u : Set M<VAR>hu : u ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s t : Set M<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s * t)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s t : Set M<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s + t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>l : List ι<GOAL>(∀ i ∈ l, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => (List.map (fun c => f c b) l).sum) x (𝓝 (List.map a l).sum)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>l : List ι<GOAL>(∀ i ∈ l, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => (List.map (fun c => f c b) l).prod) x (𝓝 (List.map a l).prod)
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>l : List ι<VAR>h : ∀ i ∈ l, Continuous (f i)<GOAL>Continuous fun a => (List.map (fun i => f i a) l).sum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>h : ∀ i ∈ l, Continuous (f i)<GOAL>Continuous fun a => (List.map (fun i => f i a) l).prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>h : ∀ i ∈ l, ContinuousOn (f i) t<GOAL>ContinuousOn (fun a => (List.map (fun i => f i a) l).prod) t
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>h : ∀ i ∈ l, ContinuousOn (f i) t<GOAL>ContinuousOn (fun a => (List.map (fun i => f i a) l).sum) t
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>n : ℕ<GOAL>Continuous fun a => n • a
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>n : ℕ<GOAL>Continuous fun a => a ^ n
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>f : X → M<VAR>h : Continuous f<VAR>n : ℕ<GOAL>Continuous fun b => n • f b
<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>f : X → M<VAR>h : Continuous f<VAR>n : ℕ<GOAL>Continuous fun b => f b ^ n