ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>TopologicalSpace 𝕜<VAR>CommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>y : F<GOAL>Continuous fun x => (B x) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>TopologicalSpace 𝕜<VAR>CommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>TopologicalSpace α<VAR>g : α → WeakBilin B<VAR>h : ∀ (y : F), Continuous fun a => (B (g a)) y<GOAL>Continuous g
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>TopologicalSpace 𝕜<VAR>CommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>hB : Function.Injective ⇑B<GOAL>Embedding fun x y => (B x) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>TopologicalSpace 𝕜<VAR>CommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>l : Filter α<VAR>f : α → WeakBilin B<VAR>x : WeakBilin B<VAR>hB : Function.Injective ⇑B<GOAL>Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : F), Filter.Tendsto (fun i => (B (f i)) y) l (𝓝 ((B x) y))
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>v : E →L[𝕜] 𝕜<VAR>x : E<GOAL>((topDualPairing 𝕜 E) v) x = v x
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<GOAL>Continuous fun x y => x y
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>y : E<GOAL>Continuous fun x => x y
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalSpace α<VAR>g : α → WeakDual 𝕜 E<VAR>h : ∀ (y : E), Continuous fun a => (g a) y<GOAL>Continuous g
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>(WeakSpace.map f) x = f x
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>F : Type u_6<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>AddCommMonoid F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>f : E →L[𝕜] F<GOAL>⇑(WeakSpace.map f) = ⇑f
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>x : E<GOAL>(continuousLinearMapToWeakSpace 𝕜 E) x = (toWeakSpace 𝕜 E) x
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<GOAL>Function.Bijective ⇑(continuousLinearMapToWeakSpace 𝕜 E)
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<GOAL>IsOpenMap ⇑(toWeakSpace 𝕜 E).symm
<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>V : Set E<VAR>hV : IsOpen (⇑(continuousLinearMapToWeakSpace 𝕜 E) '' V)<GOAL>IsOpen V
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_5<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>l : Filter α<VAR>f : α → WeakDual 𝕜 E<VAR>x : WeakDual 𝕜 E<GOAL>Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : E), Filter.Tendsto (fun i => ((topDualPairing 𝕜 E) (f i)) y) l (𝓝 (((topDualPairing 𝕜 E) x) y))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<GOAL>𝔠 ≤ #𝕜
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nontrivial E<GOAL>𝔠 ≤ #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nontrivial E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<GOAL>𝔠 ≤ #↑s
<VAR>E : Type u<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nontrivial E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>Dense sᶜ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>⇑↑φ = ⇑φ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<VAR>φ ψ : ↑(WeakDual.characterSpace 𝕜 A)<VAR>h : ∀ (x : A), φ x = ψ x<GOAL>φ = ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>⇑(WeakDual.CharacterSpace.toCLM φ) = ⇑φ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>⇑(WeakDual.CharacterSpace.toNonUnitalAlgHom φ) = ⇑φ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<GOAL>WeakDual.characterSpace 𝕜 A ∪ {0} = {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommSemiring 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>NonUnitalNonAssocSemiring A<VAR>TopologicalSpace A<VAR>Module 𝕜 A<VAR>T2Space 𝕜<VAR>ContinuousMul 𝕜<GOAL>IsClosed (WeakDual.characterSpace 𝕜 A ∪ {0})
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra 𝕜 A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>∀ (a : A), (WeakDual.CharacterSpace.toAlgHom φ) a = (WeakDual.CharacterSpace.toNonUnitalAlgHom φ).toFun a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra 𝕜 A<VAR>Nontrivial 𝕜<GOAL>WeakDual.characterSpace 𝕜 A = {φ | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra 𝕜 A<VAR>Nontrivial 𝕜<VAR>T2Space 𝕜<VAR>ContinuousMul 𝕜<GOAL>IsClosed (WeakDual.characterSpace 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>TopologicalSpace A<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>Nontrivial 𝕜<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<VAR>a : A<GOAL>φ a ∈ spectrum 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>ContinuousAdd 𝕜<VAR>ContinuousConstSMul 𝕜 𝕜<VAR>TopologicalSpace A<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>φ ψ : ↑(WeakDual.characterSpace 𝕜 A)<VAR>h : RingHom.ker φ = RingHom.ker ψ<GOAL>φ = ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>CommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>φ : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>((WeakDual.gelfandTransform 𝕜 A) a) φ = φ a
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>VAdd M X<VAR>self : UniformContinuousConstVAdd M X<VAR>c : M<GOAL>UniformContinuous fun x => c +ᵥ x
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>SMul M X<VAR>self : UniformContinuousConstSMul M X<VAR>c : M<GOAL>UniformContinuous fun x => c • x
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddCommGroup M<VAR>DistribMulAction R M<VAR>UniformSpace M<VAR>UniformAddGroup M<VAR>ContinuousConstSMul R M<GOAL>UniformContinuousConstSMul R M
<VAR>M : Type v<VAR>X : Type x<VAR>Y : Type y<VAR>UniformSpace X<VAR>UniformSpace Y<VAR>VAdd M X<VAR>UniformContinuousConstVAdd M X<VAR>f : Y → X<VAR>hf : UniformContinuous f<VAR>c : M<GOAL>UniformContinuous (c +ᵥ f)
<VAR>M : Type v<VAR>X : Type x<VAR>Y : Type y<VAR>UniformSpace X<VAR>UniformSpace Y<VAR>SMul M X<VAR>UniformContinuousConstSMul M X<VAR>f : Y → X<VAR>hf : UniformContinuous f<VAR>c : M<GOAL>UniformContinuous (c • f)
<VAR>M : Type v<VAR>X : Type x<VAR>Y : Type y<VAR>UniformSpace X<VAR>UniformSpace Y<VAR>SMul M X<VAR>SMul M Y<VAR>UniformContinuousConstSMul M Y<VAR>f : X → Y<VAR>hf : UniformInducing f<VAR>hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x<GOAL>UniformContinuousConstSMul M X
<VAR>M : Type v<VAR>X : Type x<VAR>Y : Type y<VAR>UniformSpace X<VAR>UniformSpace Y<VAR>VAdd M X<VAR>VAdd M Y<VAR>UniformContinuousConstVAdd M Y<VAR>f : X → Y<VAR>hf : UniformInducing f<VAR>hsmul : ∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x<GOAL>UniformContinuousConstVAdd M X
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>VAdd M X<VAR>c : M<VAR>x : UniformSpace.Completion X<GOAL>c +ᵥ x = UniformSpace.Completion.map (fun x => c +ᵥ x) x
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>SMul M X<VAR>c : M<VAR>x : UniformSpace.Completion X<GOAL>c • x = UniformSpace.Completion.map (fun x => c • x) x
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>VAdd M X<VAR>UniformContinuousConstVAdd M X<VAR>c : M<VAR>x : X<GOAL>↑X (c +ᵥ x) = c +ᵥ ↑X x
<VAR>M : Type v<VAR>X : Type x<VAR>UniformSpace X<VAR>SMul M X<VAR>UniformContinuousConstSMul M X<VAR>c : M<VAR>x : X<GOAL>↑X (c • x) = c • ↑X x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>F : Type u_3<VAR>E : ι → Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>(i : ι) → TopologicalSpace (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>Nonempty ι<VAR>s : Set ((i : ι) → E i)<VAR>hs : Bornology.IsVonNBounded 𝕜 s<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>Bornology.IsVonNBounded 𝕜 (⇑f '' s)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>F : Type u_3<VAR>E : ι → Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>(i : ι) → TopologicalSpace (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>ContinuousSMul 𝕜 F<VAR>s : Set ((i : ι) → E i)<VAR>hs : Bornology.IsVonNBounded 𝕜 s<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>Bornology.IsVonNBounded 𝕜 (⇑f '' s)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>VAdd M X<VAR>TopologicalSpace X<VAR>self : ProperConstVAdd M X<VAR>c : M<GOAL>IsProperMap fun x => c +ᵥ x
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>SMul M X<VAR>TopologicalSpace X<VAR>self : ProperConstSMul M X<VAR>c : M<GOAL>IsProperMap fun x => c • x
<VAR>M : Type u_1<VAR>c : M<VAR>X : Type u_2<VAR>SMul M X<VAR>TopologicalSpace X<VAR>h : ProperConstSMul M X<GOAL>IsProperMap fun x => c • x
<VAR>M : Type u_1<VAR>c : M<VAR>X : Type u_2<VAR>VAdd M X<VAR>TopologicalSpace X<VAR>h : ProperConstVAdd M X<GOAL>IsProperMap fun x => c +ᵥ x
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>SMul M X<VAR>TopologicalSpace X<VAR>ProperConstSMul M X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>c : M<GOAL>IsCompact ((fun x => c • x) ⁻¹' s)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>VAdd M X<VAR>TopologicalSpace X<VAR>ProperConstVAdd M X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>c : M<GOAL>IsCompact ((fun x => c +ᵥ x) ⁻¹' s)
<VAR>X : Type u_1<VAR>σ : Type u_2<VAR>TopologicalSpace X<VAR>CommSemiring X<VAR>TopologicalSemiring X<VAR>p : MvPolynomial σ X<GOAL>Continuous fun x => (MvPolynomial.eval x) p
<VAR>R : Type u_1<VAR>TopologicalSpace R<VAR>Star R<VAR>self : ContinuousStar R<GOAL>Continuous star
<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>s : Set R<GOAL>ContinuousOn star s
<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>s : Set R<VAR>x : R<GOAL>ContinuousWithinAt star s x
<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>x : R<GOAL>ContinuousAt star x
<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>a : R<GOAL>Filter.Tendsto star (𝓝 a) (𝓝 (star a))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>f : α → R<VAR>l : Filter α<VAR>y : R<VAR>h : Filter.Tendsto f l (𝓝 y)<GOAL>Filter.Tendsto (fun x => star (f x)) l (𝓝 (star y))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>TopologicalSpace α<VAR>f : α → R<VAR>hf : Continuous f<GOAL>Continuous fun x => star (f x)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>TopologicalSpace α<VAR>f : α → R<VAR>x : α<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => star (f x)) x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>TopologicalSpace α<VAR>f : α → R<VAR>s : Set α<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => star (f x)) s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<VAR>TopologicalSpace α<VAR>f : α → R<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun x => star (f x)) s x
<VAR>R : Type u_2<VAR>TopologicalSpace R<VAR>Star R<VAR>ContinuousStar R<GOAL>∀ (a : R), starContinuousMap a = star a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>ℱ : TopCat.Presheaf C X<VAR>x : ↑X<GOAL>(TopCat.Presheaf.stalkFunctor C x).obj ℱ = ℱ.stalk x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>i : U ⟶ V<VAR>x : ↥U<GOAL>F.map i.op ≫ F.germ x = F.germ ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>i : U ⟶ ⊤<VAR>x : ↥U<GOAL>F.map i.op ≫ F.germ x = F.Γgerm ↑((fun x => ⟨↑x, ⋯⟩) x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>i : U ⟶ V<VAR>x : ↥U<VAR>CategoryTheory.ConcreteCategory C<VAR>s : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))<GOAL>(F.germ x) ((F.map i.op) s) = (F.germ ((fun x => ⟨↑x, ⋯⟩) x)) s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>i : U ⟶ ⊤<VAR>x : ↥U<VAR>CategoryTheory.ConcreteCategory C<VAR>s : (CategoryTheory.forget C).obj (F.obj (Opposite.op ⊤))<GOAL>(F.germ x) ((F.map i.op) s) = (F.Γgerm ↑x) s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>x : ↑X<VAR>Y : C<VAR>f₁ f₂ : F.stalk x ⟶ Y<VAR>ih : ∀ (U : TopologicalSpace.Opens ↑X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂<GOAL>f₁ = f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F G : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>x : ↥U<VAR>f : F ⟶ G<GOAL>F.germ x ≫ (TopCat.Presheaf.stalkFunctor C ↑x).map f = f.app (Opposite.op U) ≫ G.germ x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑Y<VAR>x : ↥((TopologicalSpace.Opens.map f).obj U)<GOAL>((TopCat.Presheaf.pushforward C f).obj F).germ ⟨f ↑x, ⋯⟩ ≫ TopCat.Presheaf.stalkPushforward C f F ↑x = F.germ x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>ℱ : TopCat.Presheaf C X<VAR>x : ↑X<GOAL>TopCat.Presheaf.stalkPushforward C (𝟙 X) ℱ x = (TopCat.Presheaf.stalkFunctor C x).map (TopCat.Presheaf.Pushforward.id ℱ).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y Z : TopCat<VAR>ℱ : TopCat.Presheaf C X<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑X<GOAL>TopCat.Presheaf.stalkPushforward C (f ≫ g) ℱ x = TopCat.Presheaf.stalkPushforward C g ((TopCat.Presheaf.pushforward C f).obj ℱ) (f x) ≫ TopCat.Presheaf.stalkPushforward C f ℱ x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<VAR>F : TopCat.Presheaf C X<VAR>x : ↑X<GOAL>CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>x : ↑X<VAR>U : TopologicalSpace.Opens ↑Y<VAR>hU : f x ∈ U<GOAL>F.germ ⟨f x, hU⟩ ≫ TopCat.Presheaf.stalkPullbackHom C f F x = ((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op U) ≫ ((TopCat.Presheaf.pullback C f).obj F).germ ⟨x, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>Z : C<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>φ ψ : ((TopCat.Presheaf.pullback C f).obj F).obj U ⟶ Z<VAR>h : ∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V), ((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V) ≫ ((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op ≫ φ = ((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V) ≫ ((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op ≫ ψ<GOAL>φ = ψ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>U : TopologicalSpace.Opens ↑X<VAR>x : ↥U<VAR>V : TopologicalSpace.Opens ↑Y<VAR>hV : U ≤ (TopologicalSpace.Opens.map f).obj V<GOAL>((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V) ≫ ((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op ≫ TopCat.Presheaf.germToPullbackStalk C f F U x = F.germ ⟨f ↑x, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>U : TopologicalSpace.Opens ↑X<VAR>x : ↥U<GOAL>TopCat.Presheaf.germToPullbackStalk C f F U x ≫ TopCat.Presheaf.stalkPullbackHom C f F ↑x = ((TopCat.Presheaf.pullback C f).obj F).germ x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>V : (TopologicalSpace.Opens ↑Y)ᵒᵖ<VAR>x : ↥((TopologicalSpace.Opens.map f).obj (Opposite.unop V))<GOAL>((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app V ≫ TopCat.Presheaf.germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x = F.germ ⟨f ↑x, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>x : ↑X<VAR>V : TopologicalSpace.Opens ↑X<VAR>hV : x ∈ V<GOAL>((TopCat.Presheaf.pullback C f).obj F).germ ⟨x, hV⟩ ≫ TopCat.Presheaf.stalkPullbackInv C f F x = TopCat.Presheaf.germToPullbackStalk C f F V ⟨x, hV⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>y : ↥U<VAR>x : ↑X<VAR>h : x ⤳ ↑y<GOAL>F.germ y ≫ F.stalkSpecializes h = F.germ ⟨x, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>U : TopologicalSpace.Opens ↑X<VAR>x y : ↑X<VAR>h : x ⤳ y<VAR>hy : y ∈ U<GOAL>F.germ ⟨y, hy⟩ ≫ F.stalkSpecializes h = F.germ ⟨x, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>x : ↑X<GOAL>F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>x y z : ↑X<VAR>h : x ⤳ y<VAR>h' : y ⤳ z<GOAL>F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>F G : TopCat.Presheaf C X<VAR>f : F ⟶ G<VAR>x y : ↑X<VAR>h : x ⤳ y<GOAL>F.stalkSpecializes h ≫ (TopCat.Presheaf.stalkFunctor C x).map f = (TopCat.Presheaf.stalkFunctor C y).map f ≫ G.stalkSpecializes h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C X<VAR>x y : ↑X<VAR>h : x ⤳ y<GOAL>((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯ ≫ TopCat.Presheaf.stalkPushforward C f F x = TopCat.Presheaf.stalkPushforward C f F y ≫ F.stalkSpecializes h
<VAR>X : TopCat<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>F : TopCat.Presheaf C X<VAR>x y : ↑X<VAR>e : Inseparable x y<GOAL>(F.stalkCongr e).inv = F.stalkSpecializes ⋯
<VAR>X : TopCat<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>F : TopCat.Presheaf C X<VAR>x y : ↑X<VAR>e : Inseparable x y<GOAL>(F.stalkCongr e).hom = F.stalkSpecializes ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>F : TopCat.Presheaf C X<VAR>U V : TopologicalSpace.Opens ↑X<VAR>x : ↑X<VAR>hxU : x ∈ U<VAR>hxV : x ∈ V<VAR>W : TopologicalSpace.Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU : W ⟶ U<VAR>iWV : W ⟶ V<VAR>sU : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))<VAR>sV : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))<VAR>ih : (F.map iWU.op) sU = (F.map iWV.op) sV<GOAL>(F.germ ⟨x, hxU⟩) sU = (F.germ ⟨x, hxV⟩) sV
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimits C<VAR>X : TopCat<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>F : TopCat.Presheaf C X<VAR>x : ↑X<VAR>t : (CategoryTheory.forget C).obj (F.stalk x)<GOAL>∃ U, ∃ (m : x ∈ U), ∃ s, (F.germ ⟨x, m⟩) s = t