ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>(x : X) → Decidable (x ∈ s)<VAR>(y : Y) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<VAR>Hs : e.source ∩ frontier s = e'.source ∩ frontier s<VAR>Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)<GOAL>(e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>h : s ⊆ e.target<GOAL>ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>x : Z<VAR>hx : f x ∈ e.source<VAR>h : f ⁻¹' e.source ∈ 𝓝[s] x<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>x : Z<VAR>h : f ⁻¹' e.source ∈ 𝓝 x<GOAL>ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>h : s ⊆ f ⁻¹' e.source<GOAL>ContinuousOn f s ↔ ContinuousOn (↑e ∘ f) s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>h : f ⁻¹' e.source = Set.univ<GOAL>Continuous f ↔ Continuous (↑e ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : s ⊆ e.source<VAR>ht : ↑e '' s = t<GOAL>∀ (a : ↑t), (e.homeomorphOfImageSubsetSource hs ht).symm a = Set.MapsTo.restrict (↑e.symm) t s ⋯ a
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : s ⊆ e.source<VAR>ht : ↑e '' s = t<GOAL>∀ (a : ↑s), (e.homeomorphOfImageSubsetSource hs ht) a = Set.MapsTo.restrict (↑e) s t ⋯ a
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>∀ (a : ↑e.target), ↑(e.toHomeomorphSourceTarget.symm a) = ↑e.symm ↑a
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>∀ (a : ↑e.source), ↑(e.toHomeomorphSourceTarget a) = ↑e ↑a
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>SecondCountableTopology Y<GOAL>SecondCountableTopology ↑e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>𝓝 x = Filter.comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = Set.univ<VAR>h' : e.target = Set.univ<GOAL>⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = Set.univ<VAR>h' : e.target = Set.univ<GOAL>⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>OpenEmbedding (e.source.restrict ↑e)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = Set.univ<GOAL>OpenEmbedding ↑e
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(Homeomorph.refl X).toPartialHomeomorph = PartialHomeomorph.refl X
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>e.symm.toPartialHomeomorph = e.toPartialHomeomorph.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>e' : Y ≃ₜ Z<GOAL>(e.trans e').toPartialHomeomorph = e.toPartialHomeomorph.trans e'.toPartialHomeomorph
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>f' : PartialHomeomorph Y Z<GOAL>(e.transPartialHomeomorph f').target = f'.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>f' : PartialHomeomorph Y Z<GOAL>(e.transPartialHomeomorph f').source = ⇑e ⁻¹' f'.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>f' : PartialHomeomorph Y Z<GOAL>↑(e.transPartialHomeomorph f') = ↑f' ∘ ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>f' : PartialHomeomorph Y Z<GOAL>↑(e.transPartialHomeomorph f').symm = ⇑e.symm ∘ ↑f'.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ₜ Y<VAR>f' : PartialHomeomorph Y Z<GOAL>e.transPartialHomeomorph f' = e.toPartialHomeomorph.trans f'
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : X ≃ₜ Y<VAR>f : PartialHomeomorph Y Z<VAR>f' : PartialHomeomorph Z Z'<GOAL>(e.transPartialHomeomorph f).trans f' = e.transPartialHomeomorph (f.trans f')
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : X ≃ₜ Y<VAR>e' : Y ≃ₜ Z<VAR>f'' : PartialHomeomorph Z Z'<GOAL>(e.trans e').transPartialHomeomorph f'' = e.transPartialHomeomorph (e'.transPartialHomeomorph f'')
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>Nonempty X<GOAL>(OpenEmbedding.toPartialHomeomorph f h).source = Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>Nonempty X<GOAL>↑(OpenEmbedding.toPartialHomeomorph f h) = f
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>Nonempty X<GOAL>(OpenEmbedding.toPartialHomeomorph f h).target = Set.range f
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>Nonempty X<VAR>x : X<GOAL>↑(OpenEmbedding.toPartialHomeomorph f h).symm (f x) = x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>Nonempty X<VAR>x : Y<VAR>hx : x ∈ Set.range f<GOAL>f (↑(OpenEmbedding.toPartialHomeomorph f h).symm x) = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>↑(s.partialHomeomorphSubtypeCoe hs) = Subtype.val
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>(s.partialHomeomorphSubtypeCoe hs).source = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>(s.partialHomeomorphSubtypeCoe hs).target = ↑s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<GOAL>↑(e.transHomeomorph f').symm = ↑e.symm ∘ ⇑f'.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<GOAL>↑(e.transHomeomorph f') = ⇑f' ∘ ↑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<GOAL>(e.transHomeomorph f').target = ⇑f'.symm ⁻¹' e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<GOAL>(e.transHomeomorph f').source = e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<GOAL>e.transHomeomorph f' = e.trans f'.toPartialHomeomorph
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<VAR>f'' : Z ≃ₜ Z'<GOAL>(e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>f'' : Z ≃ₜ Z'<GOAL>(e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>e.subtypeRestr hs = (s.partialHomeomorphSubtypeCoe hs).trans e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>↑(e.subtypeRestr hs) = (↑s).restrict ↑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<GOAL>(e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<VAR>x : ↥s<VAR>hxe : ↑x ∈ e.source<GOAL>↑e ↑x ∈ (e.subtypeRestr hs).target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : TopologicalSpace.Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<GOAL>(f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>U : TopologicalSpace.Opens X<VAR>hU : Nonempty ↥U<GOAL>Set.EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>U V : TopologicalSpace.Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<GOAL>Set.EqOn (↑(e.subtypeRestr hV).symm) (Set.inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : C(X, ℝ)<VAR>x : X<GOAL>↑(f.attachBound x) = f x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : Polynomial ℝ<GOAL>(g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound = ↑((Polynomial.aeval f) g)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : Polynomial ℝ<GOAL>(g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<GOAL>p.comp (↑f).attachBound ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<GOAL>|↑f| ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>↑f ⊓ ↑g ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑f ⊓ ↑g ∈ A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>↑f ⊔ ↑g ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑f ⊔ ↑g ∈ A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<GOAL>closure L = ⊤
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<GOAL>A.topologicalClosure = ⊤
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : C(X, ℝ)<GOAL>f ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : X → ℝ<VAR>c : Continuous f<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<GOAL>(Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)).SeparatesPoints
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<GOAL>A.topologicalClosure = ⊤
<VAR>s : Set ℝ<VAR>CompactSpace ↑s<GOAL>(polynomialFunctions s).topologicalClosure = ⊤
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>s : Set 𝕜<VAR>CompactSpace ↑s<GOAL>(polynomialFunctions s).starClosure.topologicalClosure = ⊤
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℝ A<VAR>TopologicalSpace A<VAR>T2Space A<VAR>s : Set ℝ<VAR>CompactSpace ↑s<VAR>φ ψ : C(↑s, ℝ) →ₐ[ℝ] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)<GOAL>φ = ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>Ring A<VAR>StarRing A<VAR>Algebra 𝕜 A<VAR>TopologicalSpace A<VAR>T2Space A<VAR>s : Set 𝕜<VAR>CompactSpace ↑s<VAR>φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)<GOAL>φ = ψ
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<GOAL>↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) = ↑(Submodule.span 𝕜 ({1} ∪ ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})))
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<GOAL>↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) = ↑(Submodule.span 𝕜 {1}) + ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<GOAL>↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ⊆ ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<GOAL>↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
<VAR>F : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>A : Type u_6<VAR>CommRing K<VAR>Ring A<VAR>Algebra K A<VAR>TopologicalSpace K<VAR>T1Space K<VAR>TopologicalSpace A<VAR>ContinuousSub A<VAR>ContinuousSMul K A<VAR>FunLike F A K<VAR>AlgHomClass F K A K<VAR>SetLike S A<VAR>OneMemClass S A<VAR>AddSubgroupClass S A<VAR>SMulMemClass S K A<VAR>φ : F<VAR>hφ : Continuous ⇑φ<VAR>s : S<GOAL>closure (↑s ∩ ↑(RingHom.ker φ)) = closure ↑s ∩ ↑(RingHom.ker φ)
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>CompactSpace ↑s<GOAL>↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = closure ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>s : Set 𝕜<VAR>Zero ↑s<VAR>h0 : ↑0 = 0<VAR>CompactSpace ↑s<GOAL>Dense ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id h0})
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑Additive.ofMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑Additive.toMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑Multiplicative.ofAdd
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑Multiplicative.toAdd
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑Additive.ofMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑Additive.toMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑Multiplicative.ofAdd
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑Multiplicative.toAdd
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑Additive.ofMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑Additive.toMul
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑Multiplicative.ofAdd
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑Multiplicative.toAdd
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 (Additive.ofMul x) = Filter.map (⇑Additive.ofMul) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 (Multiplicative.ofAdd x) = Filter.map (⇑Multiplicative.ofAdd) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : Additive X<GOAL>𝓝 (Additive.toMul x) = Filter.map (⇑Additive.toMul) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : Multiplicative X<GOAL>𝓝 (Multiplicative.toAdd x) = Filter.map (⇑Multiplicative.toAdd) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑OrderDual.toDual
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Continuous ⇑OrderDual.ofDual
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑OrderDual.toDual
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsOpenMap ⇑OrderDual.ofDual
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑OrderDual.toDual
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsClosedMap ⇑OrderDual.ofDual
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 (OrderDual.toDual x) = Filter.map (⇑OrderDual.toDual) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 (OrderDual.ofDual x) = Filter.map (⇑OrderDual.ofDual) (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Setoid X<VAR>V : Set (Quotient s)<VAR>x : X<VAR>hs : V ∈ 𝓝 (Quotient.mk' x)<GOAL>Quotient.mk' ⁻¹' V ∈ 𝓝 x
<VAR>X : Type u<VAR>Setoid X<VAR>TopologicalSpace X<VAR>s : Set X<VAR>H : Dense s<GOAL>Dense (Quotient.mk' '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Setoid X<VAR>TopologicalSpace X<VAR>f : Y → X<VAR>hf : DenseRange f<GOAL>DenseRange (Quotient.mk' ∘ f)
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>s t : Setoid α<VAR>h : s ≤ t<GOAL>Continuous (Setoid.map_of_le h)
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>S : Set (Setoid α)<VAR>s : Setoid α<VAR>h : s ∈ S<GOAL>Continuous (Setoid.map_sInf h)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace β<VAR>f : α → β<VAR>y : β<GOAL>Filter.comap f (𝓝[Set.range f] y) = Filter.comap f (𝓝 y)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : { x // x ∈ s }<VAR>t : Set { x // x ∈ s }<GOAL>t ∈ 𝓝 x ↔ ∃ u ∈ 𝓝 ↑x, Subtype.val ⁻¹' u ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : { x // x ∈ s }<GOAL>𝓝 x = Filter.comap Subtype.val (𝓝 ↑x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : { x // x ∈ s }<GOAL>𝓝 x = Filter.comap Subtype.val (𝓝[s] ↑x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>x : ↑s<GOAL>𝓝[Subtype.val ⁻¹' t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set X<VAR>x : ↑S<GOAL>𝓝[≠] x = ⊥ ↔ 𝓝[≠] ↑x ⊓ 𝓟 S = ⊥
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set X<VAR>x : ↑S<GOAL>(𝓝[≠] x).NeBot ↔ (𝓝[≠] ↑x ⊓ 𝓟 S).NeBot
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set X<GOAL>DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
<VAR>X : Type u<VAR>s : Set (CofiniteTopology X)<GOAL>IsOpen s ↔ s.Nonempty → sᶜ.Finite
<VAR>X : Type u<VAR>s : Set (CofiniteTopology X)<GOAL>IsOpen s ↔ s = ∅ ∨ sᶜ.Finite
<VAR>X : Type u<VAR>s : Set (CofiniteTopology X)<GOAL>IsClosed s ↔ s = Set.univ ∨ s.Finite
<VAR>X : Type u<VAR>x : CofiniteTopology X<GOAL>𝓝 x = pure x ⊔ Filter.cofinite
<VAR>X : Type u<VAR>x : CofiniteTopology X<VAR>s : Set (CofiniteTopology X)<GOAL>s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : X → Z<GOAL>(Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Prod.fst
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y × Z<VAR>hf : Continuous f<GOAL>Continuous fun x => (f x).1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>hf : Continuous f<GOAL>Continuous fun x => f x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X × Y<GOAL>ContinuousAt Prod.fst p
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y × Z<VAR>x : X<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => (f x).1) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>x : X<VAR>y : Y<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => f x.1) (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Z<VAR>x : X × Y<VAR>hf : ContinuousAt f x.1<GOAL>ContinuousAt (fun x => f x.1) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>l : Filter X<VAR>f : X → Y × Z<VAR>p : Y × Z<VAR>h : Filter.Tendsto f l (𝓝 p)<GOAL>Filter.Tendsto (fun a => (f a).1) l (𝓝 p.1)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous Prod.snd
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y × Z<VAR>hf : Continuous f<GOAL>Continuous fun x => (f x).2
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : Y → Z<VAR>hf : Continuous f<GOAL>Continuous fun x => f x.2
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X × Y<GOAL>ContinuousAt Prod.snd p
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y × Z<VAR>x : X<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => (f x).2) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : Y → Z<VAR>x : X<VAR>y : Y<VAR>hf : ContinuousAt f y<GOAL>ContinuousAt (fun x => f x.2) (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : Y → Z<VAR>x : X × Y<VAR>hf : ContinuousAt f x.2<GOAL>ContinuousAt (fun x => f x.2) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>l : Filter X<VAR>f : X → Y × Z<VAR>p : Y × Z<VAR>h : Filter.Tendsto f l (𝓝 p)<GOAL>Filter.Tendsto (fun a => (f a).2) l (𝓝 p.2)