ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<GOAL>closure (⋃₀ S) = ⋃ s ∈ S, closure s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → Set X<GOAL>closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>Finite ι<VAR>f : ι → Set X<GOAL>closure (⋃ i, f i) = ⋃ i, closure (f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>f : ℕ → Set X<GOAL>closure (⋃ m, ⋃ (_ : m < n), f m) = ⋃ m, ⋃ (_ : m < n), closure (f m)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>f : ℕ → Set X<GOAL>closure (⋃ m, ⋃ (_ : m ≤ n), f m) = ⋃ m, ⋃ (_ : m ≤ n), closure (f m)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s ⊆ closure s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior sᶜ = (closure s)ᶜ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure sᶜ = (interior s)ᶜ
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : IsOpen t<GOAL>(closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>l : Filter X<GOAL>l ≤ l.lift' closure
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>l : Filter X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : l.HasBasis p s<GOAL>(l.lift' closure).HasBasis p fun i => closure (s i)
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>l : Filter X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : l.HasBasis p s<VAR>hc : ∀ (i : ι), p i → IsClosed (s i)<GOAL>l.lift' closure = l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>l : Filter X<GOAL>l.lift' closure = ⊥ ↔ l = ⊥
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>Dense s ↔ closure s = Set.univ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s = ∅ ↔ Dense sᶜ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : Dense s<GOAL>interior sᶜ = ∅
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>Dense (closure s) ↔ Dense s
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Dense Set.univ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<VAR>U : Set X<VAR>ho : IsOpen U<VAR>hne : U.Nonempty<GOAL>∃ x ∈ s, x ∈ U
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<GOAL>s.Nonempty ↔ Nonempty X
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : Nonempty X<VAR>hs : Dense s<GOAL>s.Nonempty
<VAR>X : Type u<VAR>s₁ s₂ : Set X<VAR>TopologicalSpace X<VAR>h : s₁ ⊆ s₂<VAR>hd : Dense s₁<GOAL>Dense s₂
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<GOAL>Dense {x}ᶜ ↔ ¬IsOpen {x}
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>s_open : IsOpen s<GOAL>s ⊆ interior (closure s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>s_closed : IsClosed s<GOAL>closure (interior s) ⊆ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s \ interior s = frontier s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>Disjoint (interior s) (frontier s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s \ frontier s = interior s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s \ frontier s = interior s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier s = closure s ∩ closure sᶜ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier s ⊆ closure s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier s ⊆ s ↔ IsClosed s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier (closure s) ⊆ frontier s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier (interior s) ⊆ frontier s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>frontier sᶜ = frontier s
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>frontier Set.univ = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>frontier ∅ = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsClosed s<GOAL>frontier s = s \ interior s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<GOAL>frontier s = closure s \ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<GOAL>s ∩ frontier s = ∅
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>Disjoint (frontier s) s ↔ IsOpen s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed (frontier s)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : IsClosed s<GOAL>interior (frontier s) = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s = interior s ∪ frontier s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s = s ∪ frontier s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>ht : IsOpen t<VAR>hd : Disjoint s t<GOAL>Disjoint (frontier s) t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<VAR>hd : Disjoint s t<GOAL>Disjoint s (frontier t)
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>(frontier s)ᶜ = interior s ∪ interior sᶜ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∉ s ∧ IsClosed s) compl
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).lift' interior = 𝓝 x
<VAR>X : Type u<VAR>ι : Sort w<VAR>TopologicalSpace X<VAR>x : X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>(𝓝 x).HasBasis p fun x => interior (s x)
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter X<GOAL>f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>h : x ∈ s<VAR>o : IsOpen s<VAR>sf : 𝓟 s ≤ f<GOAL>𝓝 x ≤ f
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>(∀ᶠ (y : X) in 𝓝 x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>(∃ᶠ (y : X) in 𝓝 x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ interior s ↔ s ∈ 𝓝 x
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Filter.map f (𝓝 x) = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 (f '' s)
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>s ∈ 𝓝 x → x ∈ s
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>h : ∀ᶠ (y : X) in 𝓝 x, p y<GOAL>p x
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>s ∈ 𝓝 x
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<GOAL>s ∈ 𝓝 x ↔ x ∈ s
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsClosed s<VAR>hx : x ∉ s<GOAL>sᶜ ∈ 𝓝 x
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>∀ᶠ (x : X) in 𝓝 x, x ∈ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsOpen s) fun x => x
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>U : Set X<VAR>h : ∀ x ∈ s, U ∈ 𝓝 x<GOAL>∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>U : Set X<VAR>h : U ∈ ⨆ x ∈ s, 𝓝 x<GOAL>∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>h : ∀ᶠ (y : X) in 𝓝 x, p y<GOAL>∀ᶠ (y : X) in 𝓝 x, ∀ᶠ (x : X) in 𝓝 y, p x
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>(∀ᶠ (y : X) in 𝓝 x, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>(∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>(∀ᶠ (x' : X) in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<GOAL>(𝓝 x).bind 𝓝 = 𝓝 x
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : X → α<GOAL>(∀ᶠ (y : X) in 𝓝 x, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 x] g
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : X → α<VAR>h : f =ᶠ[𝓝 x] g<GOAL>f x = g x
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>LE α<VAR>f g : X → α<GOAL>(∀ᶠ (y : X) in 𝓝 x, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 x] g
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : X → α<VAR>h : f =ᶠ[𝓝 x] g<GOAL>∀ᶠ (y : X) in 𝓝 x, f =ᶠ[𝓝 y] g
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>LE α<VAR>f g : X → α<VAR>h : f ≤ᶠ[𝓝 x] g<GOAL>∀ᶠ (y : X) in 𝓝 x, f ≤ᶠ[𝓝 y] g
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>P : Set X → Prop<VAR>hP : ∀ (s t : Set X), s ⊆ t → P s → P t<GOAL>(∀ s ∈ 𝓝 x, P s) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>f : Set X → Set α<VAR>hf : ∀ (s t : Set X), s ⊆ t → f s ⊆ f t<VAR>l : Filter α<GOAL>(∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<GOAL>Filter.Tendsto f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>f : α → X<GOAL>Filter.Tendsto f Filter.atTop (𝓝 x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter α<GOAL>Filter.Tendsto (fun x_1 => x) f (𝓝 x)
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup ι<VAR>Nonempty ι<VAR>u : ι → X<VAR>i₀ : ι<VAR>h : ∀ i ≥ i₀, u i = x<GOAL>Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf ι<VAR>Nonempty ι<VAR>u : ι → X<VAR>i₀ : ι<VAR>h : ∀ i ≤ i₀, u i = x<GOAL>Filter.Tendsto u Filter.atBot (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>pure ≤ 𝓝
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>f : α → X<VAR>a : α<GOAL>Filter.Tendsto f (pure a) (𝓝 (f a))
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>PartialOrder α<VAR>OrderTop α<VAR>f : α → X<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (f ⊤))
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>l : Filter α<VAR>f : α → X<VAR>h : ∀ᶠ (x' : α) in l, f x' = x<GOAL>Filter.Tendsto f l (𝓝 x)
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>l : Filter α<VAR>f : α → X<VAR>hf : f =ᶠ[l] fun x_1 => x<GOAL>Filter.Tendsto f l (𝓝 x)
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<VAR>h : ClusterPt x F<GOAL>(𝓝 x ⊓ F).NeBot
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>ιX : Sort u_3<VAR>ιF : Sort u_4<VAR>pX : ιX → Prop<VAR>sX : ιX → Set X<VAR>pF : ιF → Prop<VAR>sF : ιF → Set X<VAR>F : Filter X<VAR>hX : (𝓝 x).HasBasis pX sX<VAR>hF : F.HasBasis pF sF<GOAL>ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ 𝓝 x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>ClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : X) in 𝓝 x, y ∈ s
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>H : f ≤ 𝓝 x<VAR>f.NeBot<GOAL>ClusterPt x f
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>H : f ≤ 𝓝 x<VAR>_hf : f.NeBot<GOAL>ClusterPt x f
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>H : 𝓝 x ≤ f<GOAL>ClusterPt x f
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : Filter X<VAR>H : ClusterPt x f<VAR>h : f ≤ g<GOAL>ClusterPt x g
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : Filter X<VAR>H : ClusterPt x (f ⊓ g)<GOAL>ClusterPt x f
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f g : Filter X<VAR>H : ClusterPt x (f ⊓ g)<GOAL>ClusterPt x g
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Ultrafilter X<GOAL>ClusterPt x ↑f ↔ ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>f : Filter X<GOAL>ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>x : X<VAR>F : Filter ι<VAR>u : ι → X<GOAL>MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>x : X<VAR>F : Filter ι<VAR>u : ι → X<GOAL>MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ (a : ι) in F, u a ∈ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>x : X<VAR>F : Filter ι<VAR>u : ι → X<GOAL>MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Filter.Tendsto u (↑U) (𝓝 x)
<VAR>X : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter α<VAR>φ : α → β<VAR>u : β → X<GOAL>MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u
<VAR>X : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter α<VAR>φ : β → α<VAR>p : Filter β<VAR>u : α → X<VAR>p.NeBot<VAR>h : Filter.Tendsto φ p F<VAR>H : Filter.Tendsto (u ∘ φ) p (𝓝 x)<GOAL>MapClusterPt x F u
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>F G : Filter X<GOAL>AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>F : Filter X<GOAL>AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>C : Set X<GOAL>AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>C : Set X<GOAL>AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>C : Set X<GOAL>AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F G : Filter X<VAR>h : AccPt x F<VAR>hFG : F ≤ G<GOAL>AccPt x G
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>F : Filter X<VAR>h : AccPt x F<GOAL>ClusterPt x F
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s = {x | s ∈ 𝓝 x}
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s = {x | 𝓝 x ≤ 𝓟 s}
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>interior {x | p x} = {x | ∀ᶠ (y : X) in 𝓝 x, p y}
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>IsOpen {x | ∀ᶠ (y : X) in 𝓝 x, p y}
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<VAR>V : Set X<GOAL>s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
<VAR>X : Type u<VAR>t t' : TopologicalSpace X<GOAL>t = t' ↔ ∀ (x : X), 𝓝 x = 𝓝 x
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, s ∈ 𝓝 x
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in 𝓝 x, y ∈ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsOpen {x} ↔ 𝓝 x = pure x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsOpen {x} ↔ 𝓝[≠] x = ⊥
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : Filter X<GOAL>IsClosed {x | ClusterPt x f}
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ClusterPt x (𝓟 s)
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ (𝓝[s] x).NeBot
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>(𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>s t : Set X<VAR>h : s ⊆ t<GOAL>𝓝[s] x ≤ 𝓝[t] x
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∉ closure s ↔ 𝓝[s] x = ⊥
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>(𝓝[≠] x).NeBot<GOAL>Dense {x}ᶜ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>(𝓝[≠] x).NeBot<GOAL>closure {x}ᶜ = Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>(𝓝[≠] x).NeBot<GOAL>interior {x} = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<VAR>(𝓝[≠] x).NeBot<GOAL>¬IsOpen {x}
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>closure s = {a | ClusterPt a (𝓟 s)}
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ (Filter.comap Subtype.val (𝓝 x)).NeBot
<VAR>X : Type u<VAR>ι : Sort w<VAR>x : X<VAR>t : Set X<VAR>TopologicalSpace X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty
<VAR>X : Type u<VAR>ι : Sort w<VAR>x : X<VAR>t : Set X<VAR>TopologicalSpace X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ pure x ≤ F.lift' closure
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot
<VAR>X : Type u<VAR>x : X<VAR>TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x (F.lift' closure) ↔ ClusterPt x F
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ 𝓝 x → s ∈ u → x ∈ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
<VAR>X : Type u<VAR>s : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : IsClosed t<GOAL>interior (s ∪ t) ⊆ interior s ∪ t
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : IsOpen s<GOAL>s ∩ closure t ⊆ closure (s ∩ t)
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>h : IsOpen t<GOAL>closure s ∩ t ⊆ closure (s ∩ t)
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<VAR>ht : IsOpen t<GOAL>t ⊆ closure (t ∩ s)
<VAR>X : Type u<VAR>x : X<VAR>s₁ s₂ : Set X<VAR>TopologicalSpace X<VAR>h : x ∈ closure (s₁ ∪ s₂)<VAR>h₁ : s₁ᶜ ∈ 𝓝 x<GOAL>x ∈ closure s₂
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<VAR>ht : Dense t<VAR>hso : IsOpen s<GOAL>Dense (s ∩ t)
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<VAR>ht : Dense t<VAR>hto : IsOpen t<GOAL>Dense (s ∩ t)
<VAR>X : Type u<VAR>x : X<VAR>s t : Set X<VAR>TopologicalSpace X<VAR>hs : Dense s<VAR>ht : t ∈ 𝓝 x<GOAL>(s ∩ t).Nonempty
<VAR>X : Type u<VAR>s t : Set X<VAR>TopologicalSpace X<GOAL>closure s \ closure t ⊆ closure (s \ t)
<VAR>X : Type u<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>h : ∃ᶠ (x : X) in 𝓝 x, x ∈ s<VAR>hs : IsClosed s<GOAL>x ∈ s
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>b : Filter α<VAR>hs : IsClosed s<VAR>h : ∃ᶠ (x : α) in b, f x ∈ s<VAR>hf : Filter.Tendsto f b (𝓝 x)<GOAL>x ∈ s
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>b : Filter α<VAR>b.NeBot<VAR>hs : IsClosed s<VAR>hf : Filter.Tendsto f b (𝓝 x)<VAR>h : ∀ᶠ (x : α) in b, f x ∈ s<GOAL>x ∈ s
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>b : Filter α<VAR>h : ∃ᶠ (x : α) in b, f x ∈ s<VAR>hf : Filter.Tendsto f b (𝓝 x)<GOAL>x ∈ closure s
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>s : Set X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>b : Filter α<VAR>b.NeBot<VAR>hf : Filter.Tendsto f b (𝓝 x)<VAR>h : ∀ᶠ (x : α) in b, f x ∈ s<GOAL>x ∈ closure s
<VAR>X : Type u<VAR>α : Type u_1<VAR>x : X<VAR>TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>s : Set α<VAR>h : ∀ a ∉ s, f a = x<GOAL>Filter.Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Filter.Tendsto f l (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : Filter X<VAR>h : ∃ x, f ≤ 𝓝 x<GOAL>f ≤ 𝓝 (lim f)
<VAR>X : Type u<VAR>α : Type u_1<VAR>TopologicalSpace X<VAR>f : Filter α<VAR>g : α → X<VAR>h : ∃ x, Filter.Tendsto g f (𝓝 x)<GOAL>Filter.Tendsto g f (𝓝 (limUnder f g))
<VAR>X : Type u_1<VAR>Y : Type u_2<GOAL>∀ {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y}, Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>t : Set Y<VAR>h : IsOpen t<GOAL>IsOpen (f ⁻¹' t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : X → Y<VAR>h : ∀ (x : X), f x = g x<GOAL>Continuous f ↔ Continuous g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : X → Y<VAR>h : Continuous f<VAR>h' : ∀ (x : X), f x = g x<GOAL>Continuous g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>h : ContinuousAt f x<GOAL>Filter.Tendsto f (𝓝 x) (𝓝 (f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<GOAL>ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>g : X → Y<VAR>h : f =ᶠ[𝓝 x] g<GOAL>ContinuousAt f x ↔ ContinuousAt g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>g : X → Y<VAR>hf : ContinuousAt f x<VAR>h : f =ᶠ[𝓝 x] g<GOAL>ContinuousAt g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>t : Set Y<VAR>h : ContinuousAt f x<VAR>ht : t ∈ 𝓝 (f x)<GOAL>f ⁻¹' t ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>s : Set Y<VAR>hs : s ∈ 𝓝 (f x)<GOAL>∀ᶠ (y : X) in 𝓝 x, f y ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>M₀ : Type u_4<VAR>Zero M₀<VAR>f : X → M₀<GOAL>f =ᶠ[𝓝 x] 0 ↔ x ∉ closure (Function.support f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>lx : Filter X<VAR>ly : Filter Y<VAR>H : ClusterPt x lx<VAR>hfc : ContinuousAt f x<VAR>hf : Filter.Tendsto f lx ly<GOAL>ClusterPt (f x) ly
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>t : Set Y<VAR>hf : Continuous f<GOAL>f ⁻¹' interior t ⊆ interior (f ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous id
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous fun x => x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hg : Continuous g<VAR>hf : Continuous f<GOAL>Continuous (g ∘ f)