ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 fun x => g (f x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X → X<VAR>h : Continuous f<VAR>n : ℕ<GOAL>Continuous f^[n]
<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>x : X<VAR>g : Y → Z<VAR>hg : ContinuousAt g (f x)<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (g ∘ f) 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>x : X<VAR>hg : ContinuousAt g (f x)<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => g (f 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>x : X<VAR>y : Y<VAR>g : Y → Z<VAR>hg : ContinuousAt g y<VAR>hf : ContinuousAt f x<VAR>hy : f x = y<GOAL>ContinuousAt (g ∘ f) x
<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>x : 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>hf : Continuous f<VAR>x : X<VAR>y : Y<VAR>h : f x = y<GOAL>Filter.Tendsto f (𝓝 x) (𝓝 y)
<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 : Continuous f<GOAL>ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Continuous f ↔ ∀ (x : X), ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<GOAL>ContinuousAt (fun x => y) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>y : Y<GOAL>Continuous fun x => y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>y : Y<VAR>h : f =ᶠ[𝓝 x] fun x => y<GOAL>ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (x y : X), f x = f y<GOAL>Continuous f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>ContinuousAt id x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>y : X<GOAL>ContinuousAt (fun x => x) y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>f : X → X<VAR>hf : ContinuousAt f x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>ContinuousAt f^[n] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (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 : IsClosed t<GOAL>IsClosed (f ⁻¹' t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hx : x ∈ closure s<GOAL>f x ∈ closure (f '' s)
<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 ↔ ∀ (g : Ultrafilter X), ↑g ≤ 𝓝 x → Filter.Tendsto f (↑g) (𝓝 (f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Filter.Tendsto f (↑g) (𝓝 (f x))
<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<GOAL>closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
<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<GOAL>frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>h : Set.MapsTo f s t<VAR>hc : Continuous f<GOAL>Set.MapsTo f (closure s) (closure t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>h : Continuous f<GOAL>f '' closure s ⊆ closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>h : Continuous f<GOAL>closure (f '' closure s) = closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>h : Continuous f<GOAL>closure s ⊆ f ⁻¹' closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>t : Set Y<VAR>hf : Continuous f<VAR>hx : x ∈ closure s<VAR>ht : Set.MapsTo f s t<GOAL>f x ∈ closure t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>h : Set.MapsTo f s t<VAR>hc : Continuous f<VAR>ht : IsClosed t<GOAL>Set.MapsTo f (closure s) t
<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>l : Filter X<VAR>l' : Filter Y<VAR>h : Filter.Tendsto f l l'<GOAL>Filter.Tendsto f (l.lift' closure) (l'.lift' closure)
<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>x : X<GOAL>Filter.Tendsto f ((𝓝 x).lift' closure) ((𝓝 (f x)).lift' closure)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>hf : Function.Surjective f<GOAL>DenseRange f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>DenseRange id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<GOAL>DenseRange f ↔ closure (Set.range f) = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>h : DenseRange f<GOAL>closure (Set.range f) = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>p : X → Prop<GOAL>DenseRange Subtype.val ↔ Dense {x | p x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : Dense s<GOAL>DenseRange Subtype.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Continuous f<VAR>hs : Dense s<GOAL>Set.range f ⊆ closure (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf' : DenseRange f<VAR>hf : Continuous f<VAR>hs : Dense s<GOAL>Dense (f '' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>s : Set X<VAR>hf : DenseRange f<VAR>hs : IsOpen s<GOAL>s ⊆ closure (f '' (f ⁻¹' s))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf' : DenseRange f<VAR>hf : Continuous f<VAR>hs : Dense s<VAR>t : Set Y<VAR>ht : Set.MapsTo f s t<GOAL>Dense t
<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>α : Type u_4<VAR>g : Y → Z<VAR>f : α → Y<VAR>hg : DenseRange g<VAR>hf : DenseRange f<VAR>cg : Continuous g<GOAL>DenseRange (g ∘ f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>hf : DenseRange f<GOAL>Nonempty α ↔ Nonempty X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>h : Nonempty X<VAR>hf : DenseRange f<GOAL>Nonempty α
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_4<VAR>f : α → X<VAR>s : Set X<VAR>hf : DenseRange f<VAR>ho : IsOpen s<VAR>hs : s.Nonempty<GOAL>∃ a, f a ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>α : Type u_4<VAR>f : α → X<VAR>s : Set X<VAR>h : DenseRange f<VAR>hs : s ∈ 𝓝 x<GOAL>∃ a, f a ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
<VAR>α : Type u_2<VAR>s : Set α<GOAL>IsOpen (Set.Iic (𝓟 s))
<VAR>α : Type u_2<VAR>s : Set α<GOAL>IsOpen {l | s ∈ l}
<VAR>α : Type u_2<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range (Set.Iic ∘ 𝓟))
<VAR>α : Type u_2<VAR>s : Set (Filter α)<GOAL>IsOpen s ↔ ∃ T, s = ⋃ t ∈ T, Set.Iic (𝓟 t)
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>𝓝 l = l.lift' (Set.Iic ∘ 𝓟)
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>𝓝 l = l.lift' fun s => {l' | s ∈ l'}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>la : Filter α<VAR>lb : Filter β<VAR>f : α → Filter β<GOAL>Filter.Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>(𝓝 l).HasBasis p fun i => Set.Iic (𝓟 (s i))
<VAR>X : Type u_4<VAR>l : Filter X<GOAL>Filter.Tendsto pure l (𝓝 l)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>(𝓝 l).HasBasis p fun i => {l' | s i ∈ l'}
<VAR>α : Type u_2<VAR>l : Filter α<VAR>S : Set (Filter α)<GOAL>S ∈ 𝓝 l ↔ ∃ t ∈ l, Set.Iic (𝓟 t) ⊆ S
<VAR>α : Type u_2<VAR>l : Filter α<VAR>S : Set (Filter α)<GOAL>S ∈ 𝓝 l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S
<VAR>α : Type u_2<GOAL>𝓝 ⊥ = pure ⊥
<VAR>α : Type u_2<GOAL>𝓝 ⊤ = ⊤
<VAR>α : Type u_2<VAR>s : Set α<GOAL>𝓝 (𝓟 s) = 𝓟 (Set.Iic (𝓟 s))
<VAR>α : Type u_2<VAR>x : α<GOAL>𝓝 (pure x) = 𝓟 {⊥, pure x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → Filter α<GOAL>𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)
<VAR>α : Type u_2<VAR>l₁ l₂ : Filter α<GOAL>𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂
<VAR>α : Type u_2<GOAL>Monotone 𝓝
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>⋂₀ {s | s ∈ 𝓝 l} = Set.Iic l
<VAR>α : Type u_2<VAR>l₁ l₂ : Filter α<GOAL>𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
<VAR>α : Type u_2<VAR>s : Set (Filter α)<VAR>l : Filter α<GOAL>l ∈ interior s ↔ ∃ t ∈ l, Set.Iic (𝓟 t) ⊆ s
<VAR>α : Type u_2<VAR>s : Set (Filter α)<VAR>l : Filter α<GOAL>l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>closure {l} = Set.Ici l
<VAR>α : Type u_2<VAR>l₁ l₂ : Filter α<GOAL>l₁ ⤳ l₂ ↔ l₁ ≤ l₂
<VAR>α : Type u_2<VAR>Preorder α<GOAL>𝓝 Filter.atTop = ⨅ x, 𝓟 (Set.Iic (𝓟 (Set.Ici x)))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder β<VAR>l : Filter α<VAR>f : α → Filter β<GOAL>Filter.Tendsto f l (𝓝 Filter.atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Ici y ∈ f a
<VAR>α : Type u_2<VAR>Preorder α<GOAL>𝓝 Filter.atBot = ⨅ x, 𝓟 (Set.Iic (𝓟 (Set.Iic x)))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder β<VAR>l : Filter α<VAR>f : α → Filter β<GOAL>Filter.Tendsto f l (𝓝 Filter.atBot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Iic y ∈ f a
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 (𝓝 x) = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 (Set.Iic (𝓟 s))
<VAR>X : Type u_4<VAR>TopologicalSpace X<GOAL>Inducing 𝓝
<VAR>X : Type u_4<VAR>TopologicalSpace X<GOAL>Continuous 𝓝
<VAR>α : Type u_2<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : α → X<VAR>l : Filter α<VAR>x : X<VAR>h : Filter.Tendsto f l (𝓝 x)<GOAL>Filter.Tendsto (𝓝 ∘ f) l (𝓝 (𝓝 x))
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>s : Set X<VAR>h : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (𝓝 ∘ f) s x
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>h : ContinuousAt f x<GOAL>ContinuousAt (𝓝 ∘ f) x
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (𝓝 ∘ f) s
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : Continuous f<GOAL>Continuous (𝓝 ∘ f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : IsOpen s<GOAL>IsGδ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsGδ ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsGδ Set.univ
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>I : Set ι<VAR>hI : I.Countable<VAR>f : ι → Set X<VAR>hf : ∀ i ∈ I, IsOpen (f i)<GOAL>IsGδ (⋂ i ∈ I, f i)
<VAR>X : Type u_1<VAR>ι' : Sort u_4<VAR>TopologicalSpace X<VAR>Countable ι'<VAR>f : ι' → Set X<VAR>hf : ∀ (i : ι'), IsOpen (f i)<GOAL>IsGδ (⋂ i, f i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n
<VAR>X : Type u_1<VAR>ι' : Sort u_4<VAR>TopologicalSpace X<VAR>Countable ι'<VAR>s : ι' → Set X<VAR>hs : ∀ (i : ι'), IsGδ (s i)<GOAL>IsGδ (⋂ i, s i)
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : (i : ι) → i ∈ s → Set X<VAR>ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)<GOAL>IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>h : ∀ s ∈ S, IsGδ s<VAR>hS : S.Countable<GOAL>IsGδ (⋂₀ S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsGδ s<VAR>ht : IsGδ t<GOAL>IsGδ (s ∩ t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsGδ s<VAR>ht : IsGδ t<GOAL>IsGδ (s ∪ t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<VAR>h : ∀ s ∈ S, IsGδ s<GOAL>IsGδ (⋃₀ S)
<VAR>X : Type u_1<VAR>ι : Type u_3<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<VAR>h : ∀ i ∈ s, IsGδ (f i)<GOAL>IsGδ (⋃ i ∈ s, f i)
<VAR>X : Type u_1<VAR>ι' : Sort u_4<VAR>TopologicalSpace X<VAR>Finite ι'<VAR>f : ι' → Set X<VAR>h : ∀ (i : ι'), IsGδ (f i)<GOAL>IsGδ (⋃ i, f i)
<VAR>X : Type u_5<VAR>UniformSpace X<VAR>(𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsGδ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>UniformSpace Y<VAR>(𝓤 Y).IsCountablyGenerated<VAR>f : X → Y<GOAL>IsGδ {x | ContinuousAt f x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ho : IsOpen s<VAR>hd : Dense s<GOAL>s ∈ residual X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ho : IsGδ s<VAR>hd : Dense s<GOAL>s ∈ residual X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
<VAR>X : Type u_5<VAR>TopologicalSpace X<GOAL>IsNowhereDense ∅
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsNowhereDense s ↔ interior s = ∅
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsNowhereDense s<GOAL>IsNowhereDense (closure s)
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsNowhereDense s<GOAL>∃ t, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ
<VAR>X : Type u_5<VAR>TopologicalSpace X<GOAL>IsMeagre ∅
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsMeagre s<VAR>hts : t ⊆ s<GOAL>IsMeagre t
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsMeagre s<GOAL>IsMeagre (s ∩ t)
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : ℕ → Set X<VAR>hs : ∀ (n : ℕ), IsMeagre (s n)<GOAL>IsMeagre (⋃ n, s n)
<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.Opens α<GOAL>IsOpen self.carrier
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>p : TopologicalSpace.Opens α → Prop<GOAL>(∀ (U : TopologicalSpace.Opens α), p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p { carrier := U, is_open' := hU }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>U.carrier = ↑U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : Set α<VAR>hU : IsOpen U<GOAL>↑{ carrier := U, is_open' := hU } = U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<VAR>U : Set α<VAR>h : IsOpen U<GOAL>x ∈ { carrier := U, is_open' := h } ↔ x ∈ U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>Nonempty ↥U ↔ (↑U).Nonempty
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>(↑U).Nonempty ↔ ∃ x, x ∈ U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U V : TopologicalSpace.Opens α<VAR>h : ↑U = ↑V<GOAL>U = V
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U V : TopologicalSpace.Opens α<GOAL>↑U = ↑V ↔ U = V
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>IsOpen ↑U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>{ carrier := ↑U, is_open' := ⋯ } = U
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>GaloisConnection SetLike.coe TopologicalSpace.Opens.interior
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U V : Set α<VAR>hU : IsOpen U<VAR>hV : IsOpen V<GOAL>{ carrier := U, is_open' := hU } ⊓ { carrier := V, is_open' := hV } = { carrier := U ⊓ V, is_open' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Opens α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Opens α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>{ carrier := ∅, is_open' := ⋯ } = ⊥
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>↑U = ∅ ↔ U = ⊥
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<GOAL>x ∈ ⊤
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>{ carrier := Set.univ, is_open' := ⋯ } = ⊤
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>↑U = Set.univ ↔ U = ⊤
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>S : Set (TopologicalSpace.Opens α)<GOAL>↑(sSup S) = ⋃ i ∈ S, ↑i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : ι → TopologicalSpace.Opens α<VAR>s : Finset ι<GOAL>↑(s.sup f) = s.sup (SetLike.coe ∘ f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : ι → TopologicalSpace.Opens α<VAR>s : Finset ι<GOAL>↑(s.inf f) = s.inf (SetLike.coe ∘ f)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_5<VAR>s : ι → TopologicalSpace.Opens α<GOAL>↑(⨆ i, s i) = ⋃ i, ↑(s i)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_5<VAR>s : ι → TopologicalSpace.Opens α<GOAL>⨆ i, s i = { carrier := ⋃ i, ↑(s i), is_open' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_5<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), IsOpen (s i)<GOAL>⨆ i, { carrier := s i, is_open' := ⋯ } = { carrier := ⋃ i, s i, is_open' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_5<VAR>x : α<VAR>s : ι → TopologicalSpace.Opens α<GOAL>x ∈ iSup s ↔ ∃ i, x ∈ s i
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Us : Set (TopologicalSpace.Opens α)<VAR>x : α<GOAL>x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>OpenEmbedding Subtype.val
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U V : TopologicalSpace.Opens α<VAR>i : U ≤ V<GOAL>OpenEmbedding (Set.inclusion ⋯)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>¬(↑U).Nonempty ↔ U = ⊥
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>U : TopologicalSpace.Opens α<GOAL>U ≠ ⊥ ↔ (↑U).Nonempty
<VAR>α : Type u_5<VAR>t : TopologicalSpace α<VAR>h : t = ⊤<VAR>U : TopologicalSpace.Opens α<GOAL>U = ⊥ ∨ U = ⊤
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>B : Set (TopologicalSpace.Opens α)<GOAL>TopologicalSpace.Opens.IsBasis B ↔ ∀ {U : TopologicalSpace.Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>B : Set (TopologicalSpace.Opens α)<GOAL>TopologicalSpace.Opens.IsBasis B ↔ ∀ (U : TopologicalSpace.Opens α), ∃ Us ⊆ B, U = sSup Us
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Type u_5<VAR>b : ι → TopologicalSpace.Opens α<VAR>hb : TopologicalSpace.Opens.IsBasis (Set.range b)<VAR>hb' : ∀ (i : ι), IsCompact ↑(b i)<VAR>U : Set α<GOAL>IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)
<VAR>α : Type u_5<VAR>t₁ t₂ : TopologicalSpace α<VAR>Us : Set (TopologicalSpace.Opens α)<VAR>hUs : TopologicalSpace.Opens.IsBasis Us<GOAL>t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen ↑U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Opens α<GOAL>CompleteLattice.IsCompactElement s ↔ IsCompact ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>TopologicalSpace.Opens.comap (ContinuousMap.id α) = FrameHom.id (TopologicalSpace.Opens α)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>s t : TopologicalSpace.Opens β<VAR>h : s ≤ t<GOAL>(TopologicalSpace.Opens.comap f) s ≤ (TopologicalSpace.Opens.comap f) t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>U : TopologicalSpace.Opens β<GOAL>↑((TopologicalSpace.Opens.comap f) U) = ⇑f ⁻¹' ↑U
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : C(β, γ)<VAR>f : C(α, β)<GOAL>TopologicalSpace.Opens.comap (g.comp f) = (TopologicalSpace.Opens.comap f).comp (TopologicalSpace.Opens.comap g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : C(β, γ)<VAR>f : C(α, β)<VAR>U : TopologicalSpace.Opens γ<GOAL>(TopologicalSpace.Opens.comap f) ((TopologicalSpace.Opens.comap g) U) = (TopologicalSpace.Opens.comap (g.comp f)) U
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>T0Space β<GOAL>Function.Injective TopologicalSpace.Opens.comap
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>⇑f.opensCongr = ⇑(TopologicalSpace.Opens.comap f.symm.toContinuousMap)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>f.opensCongr.symm = f.symm.opensCongr
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<VAR>self : TopologicalSpace.OpenNhdsOf x<GOAL>x ∈ self.carrier
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<GOAL>Function.Injective TopologicalSpace.OpenNhdsOf.toOpens
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<VAR>U : TopologicalSpace.OpenNhdsOf x<GOAL>x ∈ U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<VAR>U : TopologicalSpace.OpenNhdsOf x<GOAL>IsOpen ↑U
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun x => True) SetLike.coe
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ⊆ seqClosure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>seqClosure s ⊆ closure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsSeqClosed s<GOAL>seqClosure s = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : seqClosure s = s<GOAL>IsSeqClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsSeqClosed s ↔ seqClosure s = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hc : IsClosed s<GOAL>IsSeqClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FrechetUrysohnSpace X<VAR>s : Set X<GOAL>seqClosure s = closure s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FrechetUrysohnSpace X<VAR>s : Set X<VAR>a : X<GOAL>a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>FrechetUrysohnSpace X<VAR>f : X → Y<VAR>a : X<VAR>b : Y<GOAL>Filter.Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (𝓝 a) → Filter.Tendsto (f ∘ u) Filter.atTop (𝓝 b)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (𝓝 a) → Filter.Tendsto (f ∘ u) Filter.atTop (𝓝 (f a))) → ContinuousAt f a<GOAL>FrechetUrysohnSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>FrechetUrysohnSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>FrechetUrysohnSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SequentialSpace X<VAR>M : Set X<GOAL>IsSeqClosed M ↔ IsClosed M
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>hs : IsSeqClosed s<VAR>hf : SeqContinuous f<GOAL>IsSeqClosed (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<GOAL>SeqContinuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SequentialSpace X<VAR>f : X → Y<VAR>hf : SeqContinuous f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SequentialSpace X<VAR>f : X → Y<GOAL>Continuous f ↔ SeqContinuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>SequentialSpace X<VAR>f : X → Y<GOAL>SequentialSpace Y