ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>TopologicalSpace M<VAR>TopologicalSpace R<VAR>TopologicalSpace.SeparableSpace R<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>s : Set M<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>TopologicalSpace.IsSeparable ↑(Submodule.span R s)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>s : Submodule R M<VAR>c : R<GOAL>Set.MapsTo (fun x => c • x) (closure ↑s) (closure ↑s)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>s : Submodule R M<VAR>c : R<GOAL>c • closure ↑s ⊆ closure ↑s
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<GOAL>s ≤ s.topologicalClosure
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Set M<GOAL>closure s ⊆ ↑(Submodule.span R s).topologicalClosure
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<GOAL>IsClosed ↑s.topologicalClosure
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<VAR>t : Submodule R M<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s t : Submodule R M<VAR>h : s ≤ t<GOAL>s.topologicalClosure ≤ t.topologicalClosure
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<VAR>hs : IsClosed ↑s<GOAL>s.topologicalClosure = s
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<GOAL>Dense ↑s ↔ s.topologicalClosure = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>s : Submodule R M<VAR>hs : IsCoatom s<GOAL>IsClosed ↑s ∨ Dense ↑s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Finite ι<VAR>Semiring R<VAR>TopologicalSpace R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>ContinuousSMul R M<VAR>f : (ι → R) →ₗ[R] M<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>σ : R →+* S<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>self : M →SL[σ] M₂<GOAL>Continuous (↑self).toFun
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>self : M ≃SL[σ] M₂<GOAL>Continuous self.invFun
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>M₂ : Type u_4<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>self : M ≃SL[σ] M₂<GOAL>Continuous (↑self.toLinearEquiv).toFun
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>S : outParam (Type u_3)<VAR>Semiring R<VAR>Semiring S<VAR>σ : outParam (R →+* S)<VAR>σ' : outParam (S →+* R)<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M : outParam (Type u_4)<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>M₂ : outParam (Type u_5)<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>EquivLike F M M₂<VAR>self : ContinuousSemilinearEquivClass F σ M M₂<VAR>f : F<GOAL>Continuous ⇑f
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>S : outParam (Type u_3)<VAR>Semiring R<VAR>Semiring S<VAR>σ : outParam (R →+* S)<VAR>σ' : outParam (S →+* R)<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M : outParam (Type u_4)<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>M₂ : outParam (Type u_5)<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>EquivLike F M M₂<VAR>self : ContinuousSemilinearEquivClass F σ M M₂<VAR>f : F<GOAL>Continuous (EquivLike.inv f)
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module S M₂<VAR>ContinuousConstSMul S M₂<VAR>ContinuousAdd M₂<VAR>σ : R →+* S<VAR>f : M₁ → M₂<VAR>hf : f ∈ closure (Set.range DFunLike.coe)<GOAL>⇑(linearMapOfMemClosureRangeCoe f hf) = (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module S M₂<VAR>ContinuousConstSMul S M₂<VAR>ContinuousAdd M₂<VAR>σ : R →+* S<VAR>l : Filter α<VAR>f : M₁ → M₂<VAR>g : α → M₁ →ₛₗ[σ] M₂<VAR>l.NeBot<VAR>h : Filter.Tendsto (fun a x => (g a) x) l (𝓝 f)<GOAL>⇑(linearMapOfTendsto f g h) = f
<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>TopologicalSpace M₂<VAR>T2Space M₂<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module S M₂<VAR>ContinuousConstSMul S M₂<VAR>ContinuousAdd M₂<VAR>σ : R →+* S<GOAL>IsClosed (Set.range DFunLike.coe)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<GOAL>Function.Injective ContinuousLinearMap.toLinearMap
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>h : Continuous f.toFun<GOAL>↑{ toLinearMap := f, cont := h } = f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>h : Continuous f.toFun<GOAL>⇑{ toLinearMap := f, cont := h } = ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>Continuous ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>E₁ : Type u_9<VAR>E₂ : Type u_10<VAR>UniformSpace E₁<VAR>UniformSpace E₂<VAR>AddCommGroup E₁<VAR>AddCommGroup E₂<VAR>Module R₁ E₁<VAR>Module R₂ E₂<VAR>UniformAddGroup E₁<VAR>UniformAddGroup E₂<VAR>f : E₁ →SL[σ₁₂] E₂<GOAL>UniformContinuous ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<GOAL>↑f = ↑g ↔ f = g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<GOAL>Function.Injective DFunLike.coe
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<VAR>h : ∀ (x : M₁), f x = g x<GOAL>f = g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<GOAL>f = g ↔ ∀ (x : M₁), f x = g x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>f' : M₁ → M₂<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>f' : M₁ → M₂<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>f 0 = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>x y : M₁<GOAL>f (x + y) = f x + f y
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>c : R₁<VAR>x : M₁<GOAL>f (c • x) = σ₁₂ c • f x
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₁ M₂<VAR>f : M₁ →L[R₁] M₂<VAR>c : R₁<VAR>x : M₁<GOAL>f (c • x) = c • f x
<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>R : Type u_9<VAR>S : Type u_10<VAR>Semiring S<VAR>SMul R M₁<VAR>Module S M₁<VAR>SMul R M₂<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M₁ M₂ R S<VAR>f : M₁ →L[S] M₂<VAR>c : R<VAR>x : M₁<GOAL>f (c • x) = c • f x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ι : Type u_9<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>s : Finset ι<VAR>g : ι → M₁<GOAL>f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>⇑↑f = ⇑f
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>TopologicalSpace R₁<VAR>f g : R₁ →L[R₁] M₁<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>TopologicalSpace R₁<VAR>f g : R₁ →L[R₁] M₁<GOAL>f = g ↔ f 1 = g 1
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>T2Space M₂<VAR>s : Set M₁<VAR>f g : M₁ →SL[σ₁₂] M₂<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn (⇑f) (⇑g) (closure ↑(Submodule.span R₁ s))
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>T2Space M₂<VAR>s : Set M₁<VAR>hs : Dense ↑(Submodule.span R₁ s)<VAR>f g : M₁ →SL[σ₁₂] M₂<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>RingHomSurjective σ₁₂<VAR>TopologicalSpace R₁<VAR>TopologicalSpace R₂<VAR>ContinuousSMul R₁ M₁<VAR>ContinuousAdd M₁<VAR>ContinuousSMul R₂ M₂<VAR>ContinuousAdd M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>s : Submodule R₁ M₁<GOAL>Submodule.map (↑f) s.topologicalClosure ≤ (Submodule.map (↑f) s).topologicalClosure
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>RingHomSurjective σ₁₂<VAR>TopologicalSpace R₁<VAR>TopologicalSpace R₂<VAR>ContinuousSMul R₁ M₁<VAR>ContinuousAdd M₁<VAR>ContinuousSMul R₂ M₂<VAR>ContinuousAdd M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf' : DenseRange ⇑f<VAR>s : Submodule R₁ M₁<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Submodule.map (↑f) s).topologicalClosure = ⊤
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>S₂ : Type u_9<VAR>Monoid S₂<VAR>DistribMulAction S₂ M₂<VAR>SMulCommClass R₂ S₂ M₂<VAR>ContinuousConstSMul S₂ M₂<VAR>c : S₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>x : M₁<GOAL>(c • f) x = c • f x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>S₂ : Type u_9<VAR>Monoid S₂<VAR>DistribMulAction S₂ M₂<VAR>SMulCommClass R₂ S₂ M₂<VAR>ContinuousConstSMul S₂ M₂<VAR>c : S₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>↑(c • f) = c • ↑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>S₂ : Type u_9<VAR>Monoid S₂<VAR>DistribMulAction S₂ M₂<VAR>SMulCommClass R₂ S₂ M₂<VAR>ContinuousConstSMul S₂ M₂<VAR>c : S₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>⇑(c • f) = c • ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<GOAL>default = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>x : M₁<GOAL>0 x = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<GOAL>↑0 = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<GOAL>⇑0 = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf : f ≠ 0<GOAL>∃ x, f x ≠ 0
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<GOAL>1 = ContinuousLinearMap.id R₁ M₁
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>x : M₁<GOAL>(ContinuousLinearMap.id R₁ M₁) x = x
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<GOAL>↑(ContinuousLinearMap.id R₁ M₁) = LinearMap.id
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<GOAL>⇑(ContinuousLinearMap.id R₁ M₁) = id
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>f : M₁ →L[R₁] M₁<GOAL>↑f = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁
<VAR>R₁ : Type u_1<VAR>Semiring R₁<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>x : M₁<GOAL>1 x = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<VAR>x : M₁<GOAL>(f + g) x = f x + g x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<GOAL>↑(f + g) = ↑f + ↑g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>f g : M₁ →SL[σ₁₂] M₂<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>ι : Type u_9<VAR>t : Finset ι<VAR>f : ι → M₁ →SL[σ₁₂] M₂<GOAL>↑(∑ d ∈ t, f d) = ∑ d ∈ t, ↑(f d)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>ι : Type u_9<VAR>t : Finset ι<VAR>f : ι → M₁ →SL[σ₁₂] M₂<GOAL>⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>ContinuousAdd M₂<VAR>ι : Type u_9<VAR>t : Finset ι<VAR>f : ι → M₁ →SL[σ₁₂] M₂<VAR>b : M₁<GOAL>(∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>↑(h.comp f) = (↑h).comp ↑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>⇑(h.comp f) = ⇑h ∘ ⇑f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>x : M₁<GOAL>(g.comp f) x = g (f x)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>f.comp (ContinuousLinearMap.id R₁ M₁) = f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>Semiring R₁<VAR>Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>(ContinuousLinearMap.id R₂ M₂).comp f = f
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>g : M₂ →SL[σ₂₃] M₃<GOAL>g.comp 0 = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>ContinuousLinearMap.comp 0 f = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>ContinuousAdd M₂<VAR>ContinuousAdd M₃<VAR>g : M₂ →SL[σ₂₃] M₃<VAR>f₁ f₂ : M₁ →SL[σ₁₂] M₂<GOAL>g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>TopologicalSpace M₁<VAR>AddCommMonoid M₁<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>TopologicalSpace M₃<VAR>AddCommMonoid M₃<VAR>Module R₁ M₁<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>ContinuousAdd M₃<VAR>g₁ g₂ : M₂ →SL[σ₂₃] M₃<VAR>f : M₁ →SL[σ₁₂] M₂<GOAL>(g₁ + g₂).comp f = g₁.comp f + g₂.comp f