ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>s : Set M<VAR>n : ℕ<GOAL>ContinuousOn (fun x => n • x) s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>s : Set M<VAR>n : ℕ<GOAL>ContinuousOn (fun x => x ^ n) s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>x : M<VAR>n : ℕ<GOAL>ContinuousAt (fun x => n • x) x
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>x : M<VAR>n : ℕ<GOAL>ContinuousAt (fun x => x ^ n) x
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>l : Filter α<VAR>f : α → M<VAR>x : M<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => f x ^ n) l (𝓝 (x ^ n))
<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>ContinuousAdd M<VAR>l : Filter α<VAR>f : α → M<VAR>x : M<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => n • f x) l (𝓝 (n • x))
<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>x : X<VAR>s : Set X<VAR>hf : ContinuousWithinAt f s x<VAR>n : ℕ<GOAL>ContinuousWithinAt (fun x => n • f x) s x
<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>x : X<VAR>s : Set X<VAR>hf : ContinuousWithinAt f s x<VAR>n : ℕ<GOAL>ContinuousWithinAt (fun x => f x ^ n) s x
<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>x : X<VAR>hf : ContinuousAt f x<VAR>n : ℕ<GOAL>ContinuousAt (fun x => n • f x) x
<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>x : X<VAR>hf : ContinuousAt f x<VAR>n : ℕ<GOAL>ContinuousAt (fun x => f x ^ n) x
<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>s : Set X<VAR>hf : ContinuousOn f s<VAR>n : ℕ<GOAL>ContinuousOn (fun x => f x ^ n) s
<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>s : Set X<VAR>hf : ContinuousOn f s<VAR>n : ℕ<GOAL>ContinuousOn (fun x => n • f x) s
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>a b : M<VAR>ha : b * a = 1<GOAL>Filter.Tendsto (fun x => a * x) (Filter.cocompact M) (Filter.cocompact M)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>Monoid M<VAR>ContinuousMul M<VAR>a b : M<VAR>ha : a * b = 1<GOAL>Filter.Tendsto (fun x => x * a) (Filter.cocompact M) (Filter.cocompact M)
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>AddMonoid M<VAR>AddMonoid N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>f : M →+ N<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑(AddUnits.map f)
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>Monoid M<VAR>Monoid N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>f : M →* N<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑(Units.map f)
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>oS : IsOpen ↑S<GOAL>↑S ∈ 𝓝 1
<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>oS : IsOpen ↑S<GOAL>↑S ∈ 𝓝 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>s : Multiset ι<GOAL>(∀ i ∈ s, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).prod) x (𝓝 (Multiset.map a s).prod)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>s : Multiset ι<GOAL>(∀ i ∈ s, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).sum) x (𝓝 (Multiset.map a s).sum)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>s : Finset ι<GOAL>(∀ i ∈ s, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => ∑ c ∈ s, f c b) x (𝓝 (∑ c ∈ s, a c))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>s : Finset ι<GOAL>(∀ i ∈ s, Filter.Tendsto (f i) x (𝓝 (a i))) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>s : Multiset ι<GOAL>(∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).prod
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>s : Multiset ι<GOAL>(∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).sum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>s : Multiset ι<VAR>t : Set X<GOAL>(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).sum) t
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>s : Multiset ι<VAR>t : Set X<GOAL>(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).prod) t
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>s : Finset ι<GOAL>(∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>s : Finset ι<GOAL>(∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∑ i ∈ s, f i a
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>s : Finset ι<VAR>t : Set X<GOAL>(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>s : Finset ι<VAR>t : Set X<GOAL>(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∑ i ∈ s, f i a) t
<VAR>ι : Type u_1<VAR>X : Type u_6<VAR>M : Type u_7<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>l : Filter X<VAR>f g : ι → X → M<VAR>hs : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>∑ i ∈ s, f i =ᶠ[l] ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>X : Type u_6<VAR>M : Type u_7<VAR>CommMonoid M<VAR>s : Finset ι<VAR>l : Filter X<VAR>f g : ι → X → M<VAR>hs : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => Function.support (f i)<VAR>x₀ : X<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (Function.support fun i => f i x) ⊆ ↑I
<VAR>ι : Type u_1<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>x₀ : X<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (Function.mulSupport fun i => f i x) ⊆ ↑I
<VAR>ι : Type u_1<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>x : X<GOAL>∃ s, ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
<VAR>ι : Type u_1<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => Function.support (f i)<VAR>x : X<GOAL>∃ s, ∀ᶠ (y : X) in 𝓝 x, ∑ᶠ (i : ι), f i y = ∑ i ∈ s, f i y
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>Continuous fun x => ∏ᶠ (i : ι), f i x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => Function.support (f i)<GOAL>Continuous fun x => ∑ᶠ (i : ι), f i x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>CommMonoid M<VAR>ContinuousMul M<VAR>f : ι → X → M<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Continuous (f i)<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>f : ι → X → M<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Continuous (f i)<VAR>hf : LocallyFinite fun i => Function.support (f i)<GOAL>Continuous fun x => ∑ᶠ (i : ι) (_ : p i), f i x
<VAR>M : Type u_3<VAR>Add M<VAR>ts : Set (TopologicalSpace M)<VAR>h : ∀ t ∈ ts, ContinuousAdd M<GOAL>ContinuousAdd M
<VAR>M : Type u_3<VAR>Mul M<VAR>ts : Set (TopologicalSpace M)<VAR>h : ∀ t ∈ ts, ContinuousMul M<GOAL>ContinuousMul M
<VAR>M : Type u_3<VAR>ι' : Sort u_6<VAR>Mul M<VAR>ts : ι' → TopologicalSpace M<VAR>h' : ∀ (i : ι'), ContinuousMul M<GOAL>ContinuousMul M
<VAR>M : Type u_3<VAR>ι' : Sort u_6<VAR>Add M<VAR>ts : ι' → TopologicalSpace M<VAR>h' : ∀ (i : ι'), ContinuousAdd M<GOAL>ContinuousAdd M
<VAR>M : Type u_3<VAR>Add M<VAR>t₁ t₂ : TopologicalSpace M<VAR>h₁ : ContinuousAdd M<VAR>h₂ : ContinuousAdd M<GOAL>ContinuousAdd M
<VAR>M : Type u_3<VAR>Mul M<VAR>t₁ t₂ : TopologicalSpace M<VAR>h₁ : ContinuousMul M<VAR>h₂ : ContinuousMul M<GOAL>ContinuousMul M
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>Mul X<VAR>ContinuousMul X<VAR>x : X<GOAL>⇑(ContinuousMap.mulRight x) = fun y => y * x
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>Add X<VAR>ContinuousAdd X<VAR>x : X<GOAL>⇑(ContinuousMap.addRight x) = fun y => y + x
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>Add X<VAR>ContinuousAdd X<VAR>x : X<GOAL>⇑(ContinuousMap.addLeft x) = fun y => x + y
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>Mul X<VAR>ContinuousMul X<VAR>x : X<GOAL>⇑(ContinuousMap.mulLeft x) = fun y => x * y
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>Ring R<VAR>Module R E<VAR>Module R F<VAR>f : E →ᵃ[R] F<GOAL>Continuous ⇑f ↔ Continuous ⇑f.linear
<VAR>R : Type u_1<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>Ring R<VAR>Module R F<VAR>TopologicalSpace R<VAR>ContinuousSMul R F<VAR>p v : F<GOAL>Continuous ⇑(AffineMap.lineMap p v)
<VAR>R : Type u_1<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>CommRing R<VAR>Module R F<VAR>ContinuousConstSMul R F<VAR>x : F<VAR>t : R<GOAL>Continuous ⇑(AffineMap.homothety x t)
<VAR>R : Type u_1<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>Field R<VAR>Module R F<VAR>ContinuousConstSMul R F<VAR>x : F<VAR>t : R<VAR>ht : t ≠ 0<GOAL>IsOpenMap ⇑(AffineMap.homothety x t)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NonAssocRing α<VAR>ContinuousMul α<GOAL>ContinuousNeg α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NonAssocRing α<GOAL>TopologicalSemiring α → TopologicalRing α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Semiring α<VAR>TopologicalSemiring α<VAR>s : Subsemiring α<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Semiring α<VAR>TopologicalSemiring α<VAR>s : Subsemiring α<GOAL>s ≤ s.topologicalClosure
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Semiring α<VAR>TopologicalSemiring α<VAR>s : Subsemiring α<GOAL>IsClosed ↑s.topologicalClosure
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Semiring α<VAR>TopologicalSemiring α<VAR>s : Subsemiring α<VAR>t : Subsemiring α<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>R : Type u_2<VAR>NonUnitalNonAssocRing R<VAR>TopologicalSpace R<VAR>TopologicalAddGroup R<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hmul_left : ∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)<VAR>hmul_right : ∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)<GOAL>TopologicalRing R
<VAR>R : Type u_2<VAR>NonUnitalNonAssocRing R<VAR>TopologicalSpace R<VAR>hadd : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hneg : Filter.Tendsto (fun x => -x) (𝓝 0) (𝓝 0)<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hmul_left : ∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)<VAR>hmul_right : ∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : R), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<GOAL>TopologicalRing R
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocRing α<VAR>TopologicalRing α<VAR>x : α<GOAL>Continuous ⇑(AddMonoidHom.mulLeft x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NonUnitalNonAssocRing α<VAR>TopologicalRing α<VAR>x : α<GOAL>Continuous ⇑(AddMonoidHom.mulRight x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Ring α<VAR>TopologicalRing α<VAR>s : Subring α<GOAL>s ≤ s.topologicalClosure
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Ring α<VAR>TopologicalRing α<VAR>s : Subring α<GOAL>IsClosed ↑s.topologicalClosure
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Ring α<VAR>TopologicalRing α<VAR>s : Subring α<VAR>t : Subring α<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>α : Type u_1<VAR>Ring α<GOAL>Function.Injective RingTopology.toTopologicalSpace
<VAR>α : Type u_1<VAR>Ring α<VAR>f g : RingTopology α<VAR>h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>t : TopologicalSpace α<VAR>Ring β<VAR>f : α → β<GOAL>Continuous f
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>ContinuousSMul R A<GOAL>Continuous ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<GOAL>Continuous ⇑(algebraMap R A) ↔ Continuous fun p => p.1 • p.2
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>h : Continuous ⇑(algebraMap R A)<GOAL>ContinuousSMul R A
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>ContinuousSMul R A<VAR>a : R<GOAL>(algebraMapCLM R A) a = (algebraMap R A) a
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>ContinuousSMul R A<GOAL>⇑(algebraMapCLM R A) = ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>A : Type u<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>TopologicalSpace A<VAR>ContinuousSMul R A<GOAL>↑(algebraMapCLM R A) = Algebra.linearMap R A
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>A : Type u_4<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_5<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>self : A →A[R] B<GOAL>Continuous (↑↑self.toRingHom).toFun
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>f.toAlgHom = ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : A →A[R] B<GOAL>↑f = ↑g ↔ f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>h : Continuous (↑↑f.toRingHom).toFun<GOAL>↑{ toAlgHom := f, cont := h } = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>h : Continuous (↑↑f.toRingHom).toFun<GOAL>⇑{ toAlgHom := f, cont := h } = ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>E₁ : Type u_4<VAR>E₂ : Type u_5<VAR>UniformSpace E₁<VAR>UniformSpace E₂<VAR>Ring E₁<VAR>Ring E₂<VAR>Algebra R E₁<VAR>Algebra R E₂<VAR>UniformAddGroup E₁<VAR>UniformAddGroup E₂<VAR>f : E₁ →A[R] E₂<GOAL>UniformContinuous ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : A →A[R] B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f g : A →A[R] B<GOAL>f = g ↔ ∀ (x : A), f x = g x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>x y : A<GOAL>f (x + y) = f x + f y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<VAR>c : R<VAR>x : A<GOAL>f (c • x) = c • f x
<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring S<VAR>SMul R A<VAR>Algebra S A<VAR>SMul R B<VAR>Algebra S B<VAR>MulActionHomClass (A →A[S] B) R A B<VAR>f : A →A[S] B<VAR>c : R<VAR>x : A<GOAL>f (c • x) = c • f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>ι : Type u_4<VAR>f : A →A[R] B<VAR>s : Finset ι<VAR>g : ι → A<GOAL>f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>f g : R →A[R] A<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>f g : R →A[R] A<GOAL>f = g ↔ f 1 = g 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>T2Space B<VAR>s : Set A<VAR>f g : A →A[R] B<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn (⇑f) (⇑g) (closure ↑(Algebra.adjoin R s))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>T2Space B<VAR>s : Set A<VAR>hs : Dense ↑(Algebra.adjoin R s)<VAR>f g : A →A[R] B<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>TopologicalSemiring B<VAR>f : A →A[R] B<VAR>s : Subalgebra R A<GOAL>Subalgebra.map (↑f) s.topologicalClosure ≤ (Subalgebra.map f.toAlgHom s).topologicalClosure
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>Algebra R A<VAR>s : Subalgebra R A<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>TopologicalSemiring B<VAR>f : A →A[R] B<VAR>hf' : DenseRange ⇑f<VAR>s : Subalgebra R A<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Subalgebra.map (↑f) s).topologicalClosure = ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<GOAL>1 = ContinuousAlgHom.id R A
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>x : A<GOAL>(ContinuousAlgHom.id R A) x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<GOAL>↑(ContinuousAlgHom.id R A) = AlgHom.id R A
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<GOAL>⇑(ContinuousAlgHom.id R A) = id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>f : A →A[R] A<GOAL>↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>Algebra R A<VAR>x : A<GOAL>1 x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>h : B →A[R] C<VAR>f : A →A[R] B<GOAL>↑(h.comp f) = (↑h).comp ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>h : B →A[R] C<VAR>f : A →A[R] B<GOAL>⇑(h.comp f) = ⇑h ∘ ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>g : B →A[R] C<VAR>f : A →A[R] B<VAR>x : A<GOAL>(g.comp f) x = g (f x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>f.comp (ContinuousAlgHom.id R A) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →A[R] B<GOAL>(ContinuousAlgHom.id R B).comp f = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>TopologicalSpace A<VAR>B : Type u_3<VAR>Semiring B<VAR>TopologicalSpace B<VAR>Algebra R A<VAR>Algebra R B<VAR>C : Type u_4<VAR>Semiring C<VAR>Algebra R C<VAR>TopologicalSpace C<VAR>D : Type u_5<VAR>Semiring D<VAR>Algebra R D<VAR>TopologicalSpace D<VAR>h : C →A[R] D<VAR>g : B →A[R] C<VAR>f : A →A[R] B<GOAL>(h.comp g).comp f = h.comp (g.comp f)