ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>a b : C<VAR>f : a ⟶ b<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(SkyscraperPresheafFunctor.map' p₀ f).app U = if h : p₀ ∈ Opposite.unop U then CategoryTheory.eqToHom ⋯ ≫ f ≫ CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>a : C<GOAL>SkyscraperPresheafFunctor.map' p₀ (𝟙 a) = 𝟙 (skyscraperPresheaf p₀ a)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>a b c : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>SkyscraperPresheafFunctor.map' p₀ (f ≫ g) = SkyscraperPresheafFunctor.map' p₀ f ≫ SkyscraperPresheafFunctor.map' p₀ g
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<GOAL>(skyscraperPresheafFunctor p₀).obj A = skyscraperPresheaf p₀ A
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), (skyscraperPresheafFunctor p₀).map f = SkyscraperPresheafFunctor.map' p₀ f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>y : ↑X<VAR>h : p₀ ⤳ y<VAR>U : (TopologicalSpace.OpenNhds y)ᵒᵖ<GOAL>(skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U = CategoryTheory.eqToHom ⋯
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>y : ↑X<VAR>h : p₀ ⤳ y<GOAL>(skyscraperPresheafCoconeOfSpecializes p₀ A h).pt = A
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>y : ↑X<GOAL>∀ (x : (TopologicalSpace.OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app x = CategoryTheory.Limits.terminal.from (((TopologicalSpace.OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).obj x)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>y : ↑X<GOAL>(skyscraperPresheafCocone p₀ A y).pt = ⊤_ C
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>A : C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>(skyscraperPresheaf p₀ A).IsSheaf
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasColimits C<VAR>𝓕 : TopCat.Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f).app U = if h : p₀ ∈ Opposite.unop U then 𝓕.germ ⟨p₀, h⟩ ≫ f ≫ CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (𝓕.obj U)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasColimits C<VAR>𝓕 : TopCat.Presheaf C X<VAR>c : C<VAR>f : 𝓕 ⟶ skyscraperPresheaf p₀ c<GOAL>StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ f) = f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasColimits C<VAR>𝓕 : TopCat.Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<GOAL>StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f) = f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasColimits C<VAR>𝓕 : TopCat.Presheaf C X<GOAL>(StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app 𝓕 = StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (𝟙 (((𝟭 (TopCat.Presheaf C X)).obj 𝓕).stalk p₀))
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>CategoryTheory.Category.{u, v} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasColimits C<VAR>c : C<GOAL>(StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app c = (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>self : α →C_c β<GOAL>HasCompactSupport self.toFun
<VAR>F : Type u_5<VAR>α : outParam (Type u_6)<VAR>β : outParam (Type u_7)<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : CompactlySupportedContinuousMapClass F α β<VAR>f : F<GOAL>HasCompactSupport ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C_c β<GOAL>HasCompactSupport ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C_c β<GOAL>⇑f.toContinuousMap = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f g : α →C_c β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : C(α, β)<VAR>h : HasCompactSupport ⇑f<GOAL>⇑{ toContinuousMap := f, hasCompactSupport' := h } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C_c β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α →C_c β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>IsEmpty α<VAR>f g : α →C_c β<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>CompactSpace α<VAR>f : α →C_c β<GOAL>CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported.symm f = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>CompactSpace α<VAR>f : C(α, β)<VAR>a : α<GOAL>(CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported f) a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>⇑0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>Zero β<GOAL>0 x = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>MulZeroClass β<VAR>ContinuousMul β<VAR>f g : α →C_c β<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>MulZeroClass β<VAR>ContinuousMul β<VAR>f g : α →C_c β<GOAL>(f * g) x = f x * g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>TopologicalSpace γ<VAR>SMulZeroClass γ β<VAR>ContinuousSMul γ β<VAR>F : Type u_5<VAR>FunLike F α γ<VAR>ContinuousMapClass F α γ<VAR>f : F<VAR>g : α →C_c β<GOAL>⇑(f • g) = fun x => f x • g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>TopologicalSpace γ<VAR>SMulZeroClass γ β<VAR>ContinuousSMul γ β<VAR>F : Type u_5<VAR>FunLike F α γ<VAR>ContinuousMapClass F α γ<VAR>f : F<VAR>g : α →C_c β<VAR>x : α<GOAL>(f • g) x = f x • g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddZeroClass β<VAR>ContinuousAdd β<VAR>f g : α →C_c β<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddZeroClass β<VAR>ContinuousAdd β<VAR>f g : α →C_c β<GOAL>(f + g) x = f x + g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>R : Type u_5<VAR>SMulZeroClass R β<VAR>ContinuousConstSMul R β<VAR>r : R<VAR>f : α →C_c β<GOAL>⇑(r • f) = r • ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>R : Type u_5<VAR>SMulZeroClass R β<VAR>ContinuousConstSMul R β<VAR>r : R<VAR>f : α →C_c β<VAR>x : α<GOAL>(r • f) x = r • f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α →C_c β<GOAL>⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α →C_c β<VAR>a : α<GOAL>(∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α →C_c β<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α →C_c β<GOAL>(-f) x = -f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f g : α →C_c β<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f g : α →C_c β<GOAL>(f - g) x = f x - g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>StarAddMonoid β<VAR>ContinuousStar β<VAR>f : α →C_c β<GOAL>⇑(star f) = star ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>StarAddMonoid β<VAR>ContinuousStar β<VAR>f : α →C_c β<VAR>x : α<GOAL>(star f) x = star (f x)
<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C_c δ<VAR>g : CocompactMap β γ<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C_c δ<GOAL>f.comp (CocompactMap.id γ) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>δ : Type u_5<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>f : γ →C_c δ<VAR>g : CocompactMap β γ<VAR>h : CocompactMap α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>Zero δ<VAR>g : CocompactMap β γ<GOAL>CompactlySupportedContinuousMap.comp 0 g = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Zero β<VAR>TopologicalSpace β<VAR>G : Type u_5<VAR>FunLike G α β<VAR>ContinuousMapClass G α β<VAR>CompactSpace α<GOAL>CompactlySupportedContinuousMapClass G α β
<VAR>F : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>Zero γ<VAR>FunLike F β γ<VAR>CompactlySupportedContinuousMapClass F β γ<VAR>f : F<GOAL>UniformContinuous ⇑f
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>SMul M X<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>self : ContinuousSMul M X<GOAL>Continuous fun p => p.1 • p.2
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>VAdd M X<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>self : ContinuousVAdd M X<GOAL>Continuous fun p => p.1 +ᵥ p.2
<VAR>R : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>FunLike F α β<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>TopologicalSpace R<VAR>LinearMapClass F R α β<VAR>tβ : TopologicalSpace β<VAR>ContinuousSMul R β<VAR>f : F<GOAL>ContinuousSMul R α
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : α → M<VAR>g : α → X<VAR>l : Filter α<VAR>c : M<VAR>a : X<VAR>hf : Filter.Tendsto f l (𝓝 c)<VAR>hg : Filter.Tendsto g l (𝓝 a)<GOAL>Filter.Tendsto (fun x => f x +ᵥ g x) l (𝓝 (c +ᵥ a))
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : α → M<VAR>g : α → X<VAR>l : Filter α<VAR>c : M<VAR>a : X<VAR>hf : Filter.Tendsto f l (𝓝 c)<VAR>hg : Filter.Tendsto g l (𝓝 a)<GOAL>Filter.Tendsto (fun x => f x • g x) l (𝓝 (c • a))
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : α → M<VAR>l : Filter α<VAR>c : M<VAR>hf : Filter.Tendsto f l (𝓝 c)<VAR>a : X<GOAL>Filter.Tendsto (fun x => f x • a) l (𝓝 (c • a))
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : α → M<VAR>l : Filter α<VAR>c : M<VAR>hf : Filter.Tendsto f l (𝓝 c)<VAR>a : X<GOAL>Filter.Tendsto (fun x => f x +ᵥ a) l (𝓝 (c +ᵥ a))
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>s : Set Y<VAR>hf : ContinuousWithinAt f s b<VAR>hg : ContinuousWithinAt g s b<GOAL>ContinuousWithinAt (fun x => f x • g x) s b
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>s : Set Y<VAR>hf : ContinuousWithinAt f s b<VAR>hg : ContinuousWithinAt g s b<GOAL>ContinuousWithinAt (fun x => f x +ᵥ g x) s b
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>hf : ContinuousAt f b<VAR>hg : ContinuousAt g b<GOAL>ContinuousAt (fun x => f x • g x) b
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>hf : ContinuousAt f b<VAR>hg : ContinuousAt g b<GOAL>ContinuousAt (fun x => f x +ᵥ g x) b
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : Y → M<VAR>g : Y → X<VAR>s : Set Y<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x +ᵥ g x) s
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>s : Set Y<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x • g x) s
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>f : Y → M<VAR>g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x +ᵥ g x
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x • g x
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>a b : M<VAR>x y : X<VAR>h₁ : a ⤳ b<VAR>h₂ : x ⤳ y<GOAL>(a • x) ⤳ (b • y)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>a b : M<VAR>x y : X<VAR>h₁ : a ⤳ b<VAR>h₂ : x ⤳ y<GOAL>(a +ᵥ x) ⤳ (b +ᵥ y)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>a b : M<VAR>x y : X<VAR>h₁ : Inseparable a b<VAR>h₂ : Inseparable x y<GOAL>Inseparable (a +ᵥ x) (b +ᵥ y)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>a b : M<VAR>x y : X<VAR>h₁ : Inseparable a b<VAR>h₂ : Inseparable x y<GOAL>Inseparable (a • x) (b • y)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>k : Set M<VAR>u : Set X<VAR>hk : IsCompact k<VAR>hu : IsCompact u<GOAL>IsCompact (k +ᵥ u)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>k : Set M<VAR>u : Set X<VAR>hk : IsCompact k<VAR>hu : IsCompact u<GOAL>IsCompact (k • u)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>K : Set M<VAR>L : Set X<GOAL>closure K +ᵥ closure L ⊆ closure (K +ᵥ L)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>K : Set M<VAR>L : Set X<GOAL>closure K • closure L ⊆ closure (K • L)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SMul M X<VAR>ContinuousSMul M X<VAR>g : Y → X<VAR>N : Type u_5<VAR>SMul N Y<VAR>TopologicalSpace N<VAR>f : N → M<VAR>hg : Inducing g<VAR>hf : Continuous f<VAR>hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x<GOAL>ContinuousSMul N Y
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>VAdd M X<VAR>ContinuousVAdd M X<VAR>g : Y → X<VAR>N : Type u_5<VAR>VAdd N Y<VAR>TopologicalSpace N<VAR>f : N → M<VAR>hg : Inducing g<VAR>hf : Continuous f<VAR>hsmul : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x<GOAL>ContinuousVAdd N Y
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>AddMonoid M<VAR>AddAction M X<VAR>ContinuousVAdd M X<VAR>N : Type u_5<VAR>TopologicalSpace N<VAR>AddMonoid N<VAR>f : N →+ M<VAR>hf : Continuous ⇑f<GOAL>ContinuousVAdd N X
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>TopologicalSpace X<VAR>Monoid M<VAR>MulAction M X<VAR>ContinuousSMul M X<VAR>N : Type u_5<VAR>TopologicalSpace N<VAR>Monoid N<VAR>f : N →* M<VAR>hf : Continuous ⇑f<GOAL>ContinuousSMul N X
<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>VAdd M X<VAR>ts : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ ts, ContinuousVAdd M X<GOAL>ContinuousVAdd M X
<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>SMul M X<VAR>ts : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ ts, ContinuousSMul M X<GOAL>ContinuousSMul M X
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>SMul M X<VAR>ts' : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), ContinuousSMul M X<GOAL>ContinuousSMul M X
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>VAdd M X<VAR>ts' : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), ContinuousVAdd M X<GOAL>ContinuousVAdd M X
<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>SMul M X<VAR>t₁ t₂ : TopologicalSpace X<VAR>ContinuousSMul M X<VAR>ContinuousSMul M X<GOAL>ContinuousSMul M X
<VAR>M : Type u_2<VAR>X : Type u_3<VAR>TopologicalSpace M<VAR>VAdd M X<VAR>t₁ t₂ : TopologicalSpace X<VAR>ContinuousVAdd M X<VAR>ContinuousVAdd M X<GOAL>ContinuousVAdd M X
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>AddGroup G<VAR>AddTorsor G P<VAR>TopologicalSpace G<VAR>PreconnectedSpace G<VAR>TopologicalSpace P<VAR>ContinuousVAdd G P<GOAL>ConnectedSpace P
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsUpperSet s → IsUpperSet (closure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsOpen s → IsOpen ↑(upperClosure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsOpen s → IsOpen ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsLowerSet s → IsLowerSet (closure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsUpperSet s → IsUpperSet (closure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsLowerSet s → IsLowerSet (closure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsOpen s → IsOpen ↑(upperClosure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<GOAL>IsOpen s → IsOpen ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsUpperSet (interior s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsLowerSet (interior s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>HasUpperLowerClosure α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>(interior s).OrdConnected
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>self : ContinuousMapZero X R<GOAL>self.toContinuousMap 0 = 0
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>f g : ContinuousMapZero X R<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>f : C(X, R)<VAR>h0 : f 0 = 0<GOAL>⇑{ toContinuousMap := f, map_zero' := h0 } = ⇑f
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Zero R<GOAL>Function.Injective toContinuousMap
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<GOAL>Set.range toContinuousMap = {f | f 0 = 0}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>R : Type u_3<VAR>Zero X<VAR>Zero Y<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace R<VAR>g : ContinuousMapZero Y R<VAR>f : ContinuousMapZero X Y<VAR>x : X<GOAL>(g.comp f) x = g (f x)
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>PartialOrder R<VAR>f g : ContinuousMapZero X R<GOAL>f ≤ g ↔ ∀ (x : X), f x ≤ g x
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<GOAL>Embedding toContinuousMap
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>Zero X<VAR>Zero R<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>T1Space R<GOAL>ClosedEmbedding toContinuousMap
<VAR>R : Type u_3<VAR>Zero R<VAR>TopologicalSpace R<VAR>s : Set R<VAR>Zero ↑s<VAR>h0 : ↑0 = 0<GOAL>∀ (a : ↑s), (ContinuousMapZero.id h0) a = ↑a
<VAR>R : Type u_3<VAR>Zero R<VAR>TopologicalSpace R<VAR>s : Set R<VAR>Zero ↑s<VAR>h0 : ↑0 = 0<GOAL>↑(ContinuousMapZero.id h0) = ContinuousMap.restrict s (ContinuousMap.id R)
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>Zero R<GOAL>⇑0 = 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>AddZeroClass R<VAR>ContinuousAdd R<VAR>f g : ContinuousMapZero X R<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>MulZeroClass R<VAR>ContinuousMul R<VAR>f g : ContinuousMapZero X R<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>M : Type u_3<VAR>Zero R<VAR>SMulZeroClass M R<VAR>ContinuousConstSMul M R<VAR>m : M<VAR>f : ContinuousMapZero X R<GOAL>⇑(m • f) = m • ⇑f
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>Zero X<VAR>TopologicalSpace X<VAR>TopologicalSpace R<VAR>CommSemiring R<VAR>TopologicalSemiring R<VAR>StarRing R<VAR>ContinuousStar R<VAR>f : ContinuousMapZero X R<GOAL>⇑(star f) = star ⇑f