ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>f : X → Y<VAR>g : Y → X<VAR>h : Function.LeftInverse f g<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>ClosedEmbedding g
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>hst : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s t : Finset X<VAR>h : Disjoint s t<GOAL>SeparatedNhds ↑s ↑t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<VAR>s : Finset X<VAR>h : x ∉ s<GOAL>SeparatedNhds {x} ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X → Y<VAR>s : Set Y<VAR>hs : IsCompact s<VAR>hf : Continuous f<GOAL>IsCompact (f ⁻¹' s)
<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), T2Space (π i)<VAR>s : Set ((i : ι) → π i)<GOAL>IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' s)
<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>(i : ι) → TopologicalSpace (π i)<VAR>∀ (i : ι), T2Space (π i)<VAR>s : Set ((i : ι) → π i)<GOAL>IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<GOAL>∃ i, V i ⊆ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>K : CompactExhaustion X<VAR>n : ℕ<GOAL>IsClosed (K n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s ∩ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>s : Set X<VAR>hs : IsCompact (closure s)<VAR>f : X → Y<VAR>hf : ContinuousOn f (closure s)<GOAL>f '' closure s = closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X → Y<VAR>h : Continuous f<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X → Y<VAR>h : Continuous f<VAR>hf : Function.Injective f<GOAL>ClosedEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X → Y<VAR>hsurj : Function.Surjective f<VAR>hcont : Continuous f<GOAL>QuotientMap f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>S : Set X<GOAL>IsPreirreducible S ↔ S.Subsingleton
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>S : Set X<VAR>h : IsPreirreducible S<GOAL>S.Subsingleton
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>S : Set X<GOAL>IsIrreducible S ↔ ∃ x, S = {x}
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>PreirreducibleSpace X<VAR>Nontrivial X<VAR>T2Space X<GOAL>False
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>RegularSpace X ↔ ∀ {s : Set X} {a : X}, IsClosed s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : RegularSpace X<VAR>s : Set X<VAR>a : X<GOAL>IsClosed s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>[RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x), ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x<GOAL>RegularSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x<GOAL>RegularSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : X → Sort u_3<VAR>p : (a : X) → ι a → Prop<VAR>s : (a : X) → ι a → Set X<VAR>h₁ : ∀ (a : X), (𝓝 a).HasBasis (p a) (s a)<VAR>h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed (s a i)<GOAL>RegularSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s<GOAL>RegularSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<VAR>s : Set X<GOAL>Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<VAR>s : Set X<GOAL>Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<VAR>s : Set X<VAR>h : s ∈ 𝓝 x<GOAL>∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsClosed s) id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<GOAL>(𝓝 x).lift' closure = 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>ι : Sort u_3<VAR>x : X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>(𝓝 x).HasBasis p fun i => closure (s i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x) closure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) closure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : U ∈ 𝓝ˢ K<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>(𝓝ˢ K).lift' closure = 𝓝ˢ K
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>B : Set (Set X)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ s ∈ B) closure
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>B : Set (Set X)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>x : X<VAR>s : Set X<VAR>h : s ∈ 𝓝 x<GOAL>∃ t ∈ B, x ∈ t ∧ closure t ⊆ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<GOAL>RegularSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>f : Y → X<GOAL>RegularSpace Y
<VAR>X : Type u_3<VAR>T : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ T, RegularSpace X<GOAL>RegularSpace X
<VAR>ι : Sort u_3<VAR>X : Type u_4<VAR>t : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), RegularSpace X<GOAL>RegularSpace X
<VAR>X : Type u_3<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : RegularSpace X<VAR>h₂ : RegularSpace X<GOAL>RegularSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>r : RegularSpace X<VAR>LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>h_KU : K ⊆ U<GOAL>∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>RegularSpace X<VAR>K U : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<GOAL>LocallyCompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : T25Space X<VAR>x y : X<GOAL>x ≠ y → Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T25Space X<VAR>x y : X<GOAL>Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T25Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T25Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T25Space Y<VAR>f : X → Y<VAR>hinj : Function.Injective f<VAR>hcont : Continuous f<GOAL>T25Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T25Space Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>T25Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<GOAL>T3Space X ↔ T0Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T3Space Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>T3Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T3Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : NormalSpace X<VAR>s t : Set X<GOAL>IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s t : Set X<VAR>H1 : IsClosed s<VAR>H2 : IsClosed t<VAR>H3 : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<GOAL>∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>NormalSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<GOAL>T4Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T4Space Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>T4Space X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : CompletelyNormalSpace X<VAR>s t : Set X<GOAL>Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompletelyNormalSpace Y<VAR>e : X → Y<VAR>he : Embedding e<GOAL>CompletelyNormalSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T5Space Y<VAR>e : X → Y<VAR>he : Embedding e<GOAL>T5Space X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : PerfectlyNormalSpace X<VAR>h : Set X<GOAL>IsClosed h → IsGδ h
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>NormalSpace X<VAR>st_dis : Disjoint s t<VAR>t_cl : IsClosed t<VAR>t_gd : IsGδ t<GOAL>HasSeparatingCover s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>x : X<GOAL>connectedComponent x = ⋂ s, ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}<GOAL>TotallySeparatedSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<GOAL>TotallyDisconnectedSpace X ↔ TotallySeparatedSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>TotallyDisconnectedSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ IsClopen s) id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>TotallyDisconnectedSpace X<GOAL>TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>TotallyDisconnectedSpace X<VAR>x : X<VAR>U : Set X<VAR>is_open : IsOpen U<VAR>memU : x ∈ U<GOAL>∃ V, IsClopen V ∧ x ∈ V ∧ V ⊆ U
<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>LocallyCompactSpace H<VAR>T2Space H<VAR>TotallyDisconnectedSpace H<GOAL>TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>LocallyCompactSpace H<VAR>T2Space H<GOAL>TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H
<VAR>Γ : Type u_1<VAR>T : Type u_2<VAR>TopologicalSpace T<VAR>SMul Γ T<VAR>self : ContinuousConstSMul Γ T<VAR>γ : Γ<GOAL>Continuous fun x => γ • x
<VAR>Γ : Type u_1<VAR>T : Type u_2<VAR>TopologicalSpace T<VAR>VAdd Γ T<VAR>self : ContinuousConstVAdd Γ T<VAR>γ : Γ<GOAL>Continuous fun x => γ +ᵥ x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>c : M<GOAL>Filter.Tendsto (fun x => c • f x) l (𝓝 (c • a))
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>c : M<GOAL>Filter.Tendsto (fun x => c +ᵥ f x) l (𝓝 (c +ᵥ a))
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>b : β<VAR>s : Set β<VAR>hg : ContinuousWithinAt g s b<VAR>c : M<GOAL>ContinuousWithinAt (fun x => c • g x) s b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>b : β<VAR>s : Set β<VAR>hg : ContinuousWithinAt g s b<VAR>c : M<GOAL>ContinuousWithinAt (fun x => c +ᵥ g x) s b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>b : β<VAR>hg : ContinuousAt g b<VAR>c : M<GOAL>ContinuousAt (fun x => c +ᵥ g x) b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>b : β<VAR>hg : ContinuousAt g b<VAR>c : M<GOAL>ContinuousAt (fun x => c • g x) b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>s : Set β<VAR>hg : ContinuousOn g s<VAR>c : M<GOAL>ContinuousOn (fun x => c • g x) s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>s : Set β<VAR>hg : ContinuousOn g s<VAR>c : M<GOAL>ContinuousOn (fun x => c +ᵥ g x) s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>hg : Continuous g<VAR>c : M<GOAL>Continuous fun x => c +ᵥ g x
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>TopologicalSpace β<VAR>g : β → α<VAR>hg : Continuous g<VAR>c : M<GOAL>Continuous fun x => c • g x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>VAdd α β<VAR>TopologicalSpace β<VAR>ContinuousConstVAdd α β<VAR>a : α<VAR>s : Set β<VAR>hs : IsCompact s<GOAL>IsCompact (a +ᵥ s)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>SMul α β<VAR>TopologicalSpace β<VAR>ContinuousConstSMul α β<VAR>a : α<VAR>s : Set β<VAR>hs : IsCompact s<GOAL>IsCompact (a • s)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>x y : α<VAR>h : x ⤳ y<VAR>c : M<GOAL>(c +ᵥ x) ⤳ (c +ᵥ y)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>x y : α<VAR>h : x ⤳ y<VAR>c : M<GOAL>(c • x) ⤳ (c • y)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>VAdd M α<VAR>ContinuousConstVAdd M α<VAR>x y : α<VAR>h : Inseparable x y<VAR>c : M<GOAL>Inseparable (c +ᵥ x) (c +ᵥ y)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>SMul M α<VAR>ContinuousConstSMul M α<VAR>x y : α<VAR>h : Inseparable x y<VAR>c : M<GOAL>Inseparable (c • x) (c • y)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Monoid M<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>c : M<VAR>s : Set α<GOAL>c • closure s ⊆ closure (c • s)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>AddMonoid M<VAR>AddAction M α<VAR>ContinuousConstVAdd M α<VAR>c : M<VAR>s : Set α<GOAL>c +ᵥ closure s ⊆ closure (c +ᵥ s)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Monoid M<VAR>MulAction M α<VAR>ContinuousConstSMul M α<VAR>c : M<VAR>x : α<GOAL>c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>AddMonoid M<VAR>AddAction M α<VAR>ContinuousConstVAdd M α<VAR>c : M<VAR>x : α<GOAL>c +ᵥ closure (AddAction.orbit M x) ⊆ closure (AddAction.orbit M x)
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_4<VAR>Monoid N<VAR>α : Type u_5<VAR>β : Type u_6<VAR>MulAction M α<VAR>MulAction N β<VAR>TopologicalSpace β<VAR>T2Space β<VAR>ContinuousConstSMul N β<VAR>σ : M → N<GOAL>IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>c : G<GOAL>Filter.Tendsto (fun x => c +ᵥ f x) l (𝓝 (c +ᵥ a)) ↔ Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>c : G<GOAL>Filter.Tendsto (fun x => c • f x) l (𝓝 (c • a)) ↔ Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<VAR>c : G<GOAL>ContinuousWithinAt (fun x => c +ᵥ f x) s b ↔ ContinuousWithinAt f s b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<VAR>c : G<GOAL>ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<VAR>c : G<GOAL>ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<VAR>c : G<GOAL>ContinuousOn (fun x => c +ᵥ f x) s ↔ ContinuousOn f s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G<GOAL>ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G<GOAL>ContinuousAt (fun x => c +ᵥ f x) b ↔ ContinuousAt f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : G<GOAL>(Continuous fun x => c • f x) ↔ Continuous f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : G<GOAL>(Continuous fun x => c +ᵥ f x) ↔ Continuous f
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>c : G<GOAL>IsOpenMap fun x => c • x
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>c : G<GOAL>IsOpenMap fun x => c +ᵥ x
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>c : G<GOAL>IsOpen (c +ᵥ s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>c : G<GOAL>IsOpen (c • s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>c : G<GOAL>IsClosedMap fun x => c • x
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>c : G<GOAL>IsClosedMap fun x => c +ᵥ x
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>c : G<GOAL>IsClosed (c +ᵥ s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>c : G<GOAL>IsClosed (c • s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>c : G<VAR>s : Set α<GOAL>closure (c +ᵥ s) = c +ᵥ closure s
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>c : G<VAR>s : Set α<GOAL>closure (c • s) = c • closure s
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>c : G<VAR>s : Set α<VAR>hs : Dense s<GOAL>Dense (c +ᵥ s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>c : G<VAR>s : Set α<VAR>hs : Dense s<GOAL>Dense (c • s)
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>AddGroup G<VAR>AddAction G α<VAR>ContinuousConstVAdd G α<VAR>c : G<VAR>s : Set α<GOAL>interior (c +ᵥ s) = c +ᵥ interior s
<VAR>α : Type u_2<VAR>G : Type u_4<VAR>TopologicalSpace α<VAR>Group G<VAR>MulAction G α<VAR>ContinuousConstSMul G α<VAR>c : G<VAR>s : Set α<GOAL>interior (c • s) = c • interior s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>Filter.Tendsto (fun x => c • f x) l (𝓝 (c • a)) ↔ Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G₀<VAR>s : Set β<VAR>hc : c ≠ 0<GOAL>ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : G₀<VAR>s : Set β<VAR>hc : c ≠ 0<GOAL>ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>(Continuous fun x => c • f x) ↔ Continuous f
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.smulOfNeZero c hc) = fun x => c • x
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>⇑(Homeomorph.smulOfNeZero c hc).symm = fun x => c⁻¹ • x
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>IsOpenMap fun x => c • x
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>hs : IsOpen s<VAR>hc : c ≠ 0<GOAL>IsOpen (c • s)
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<VAR>s : Set α<GOAL>interior (c • s) = c • interior s
<VAR>α : Type u_2<VAR>G₀ : Type u_4<VAR>TopologicalSpace α<VAR>GroupWithZero G₀<VAR>MulAction G₀ α<VAR>ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>hc : c ≠ 0<VAR>s : Set α<GOAL>closure (c • s) = c • closure s