ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_1<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>f : α → β<VAR>hf : Embedding f<GOAL>FirstCountableTopology α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>FirstCountableTopology α<VAR>u : ℕ → α<VAR>x : α<VAR>hx : MapClusterPt x Filter.atTop u<GOAL>∃ ψ, StrictMono ψ ∧ Filter.Tendsto (u ∘ ψ) Filter.atTop (𝓝 x)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>self : SecondCountableTopology α<GOAL>∃ b, b.Countable ∧ t = TopologicalSpace.generateFrom b
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>hc : b.Countable<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>b : Set (Set α)<VAR>hc : b.Countable<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<GOAL>∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<GOAL>(TopologicalSpace.countableBasis α).Countable
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<GOAL>∅ ∉ TopologicalSpace.countableBasis α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<GOAL>TopologicalSpace.IsTopologicalBasis (TopologicalSpace.countableBasis α)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<GOAL>t = TopologicalSpace.generateFrom (TopologicalSpace.countableBasis α)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hs : s ∈ TopologicalSpace.countableBasis α<GOAL>IsOpen s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hs : s ∈ TopologicalSpace.countableBasis α<GOAL>s.Nonempty
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace β<VAR>SecondCountableTopology β<VAR>f : α → β<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>ι : Sort u_1<VAR>Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), SecondCountableTopology α<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Sort u_1<VAR>Countable ι<VAR>U : ι → Set α<VAR>∀ (i : ι), SecondCountableTopology ↑(U i)<VAR>Uo : ∀ (i : ι), IsOpen (U i)<VAR>hc : ⋃ i, U i = Set.univ<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<GOAL>∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ I, IsOpen (s i)<GOAL>∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>S : Set (Set α)<VAR>H : ∀ s ∈ S, IsOpen s<GOAL>∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>f : α → Set α<VAR>hf : ∀ (x : α), f x ∈ 𝓝 x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (E i)<VAR>s : (i : ι) → Set (Set (E i))<VAR>hs : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (s i)<GOAL>TopologicalSpace.IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)
<VAR>α : Type u<VAR>β : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (Set α)<VAR>hs : TopologicalSpace.IsTopologicalBasis s<VAR>t : Set (Set β)<VAR>ht : TopologicalSpace.IsTopologicalBasis t<GOAL>TopologicalSpace.IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>π : X → Y<VAR>V : Set (Set X)<VAR>hV : TopologicalSpace.IsTopologicalBasis V<VAR>h' : QuotientMap π<VAR>h : IsOpenMap π<GOAL>TopologicalSpace.IsTopologicalBasis (Set.image π '' V)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>π : X → Y<VAR>SecondCountableTopology X<VAR>h' : QuotientMap π<VAR>h : IsOpenMap π<GOAL>SecondCountableTopology Y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Setoid X<VAR>V : Set (Set X)<VAR>hV : TopologicalSpace.IsTopologicalBasis V<VAR>h : IsOpenMap Quotient.mk'<GOAL>TopologicalSpace.IsTopologicalBasis (Set.image Quotient.mk' '' V)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Setoid X<VAR>SecondCountableTopology X<VAR>h : IsOpenMap Quotient.mk'<GOAL>SecondCountableTopology (Quotient S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>SecondCountableTopology β<VAR>hf : Inducing f<GOAL>SecondCountableTopology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>SecondCountableTopology β<VAR>hf : Embedding f<GOAL>SecondCountableTopology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SecondCountableTopology β<VAR>f : α → β<VAR>hf : Embedding f<GOAL>TopologicalSpace.SeparableSpace α
<VAR>X : TopCat<VAR>x : ↑X<GOAL>(𝟙 X) x = x
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑X<GOAL>(f ≫ g) x = g (f x)
<VAR>X : TopCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : TopCat<VAR>f : X ≅ Y<VAR>x : ↑X<GOAL>f.inv (f.hom x) = x
<VAR>X Y : TopCat<VAR>f : X ≅ Y<VAR>y : ↑Y<GOAL>f.hom (f.inv y) = y
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>↑(TopCat.of X) = X
<VAR>X Y : Type u<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<VAR>x : (CategoryTheory.forget TopCat).obj (TopCat.of X)<GOAL>f x = f x
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>f x = f.toFun x
<VAR>X Y : TopCat<VAR>f : ↑X ≃ₜ ↑Y<GOAL>(TopCat.isoOfHomeo f).hom = f.toContinuousMap
<VAR>X Y : TopCat<VAR>f : ↑X ≃ₜ ↑Y<GOAL>(TopCat.isoOfHomeo f).inv = f.symm.toContinuousMap
<VAR>X Y : TopCat<VAR>f : X ≅ Y<VAR>a : ↑X<GOAL>(TopCat.homeoOfIso f) a = f.hom a
<VAR>X Y : TopCat<VAR>f : X ≅ Y<VAR>a : ↑Y<GOAL>(TopCat.homeoOfIso f).symm a = f.inv a
<VAR>X Y : TopCat<VAR>f : ↑X ≃ₜ ↑Y<GOAL>TopCat.homeoOfIso (TopCat.isoOfHomeo f) = f
<VAR>X Y : TopCat<VAR>f : X ≅ Y<GOAL>TopCat.isoOfHomeo (TopCat.homeoOfIso f) = f
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>OpenEmbedding ⇑(f ≫ g) ↔ OpenEmbedding ⇑f
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>OpenEmbedding ((CategoryTheory.forget TopCat).map f ≫ (CategoryTheory.forget TopCat).map g) ↔ OpenEmbedding ⇑f
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>OpenEmbedding ⇑(f ≫ g) ↔ OpenEmbedding ⇑g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>OpenEmbedding ((CategoryTheory.forget TopCat).map f ≫ (CategoryTheory.forget TopCat).map g) ↔ OpenEmbedding ⇑g
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>CountableInterFilter f<VAR>hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>CountableInterFilter f<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>p : Set X → Prop<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<GOAL>p s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<GOAL>IsLindelof (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>ht : IsLindelof t<VAR>hs : IsClosed s<GOAL>IsLindelof (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsOpen t<GOAL>IsLindelof (s \ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<GOAL>IsLindelof t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<GOAL>IsLindelof (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : Continuous f<GOAL>IsLindelof (f '' s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>f : Filter X<VAR>CountableInterFilter f<VAR>hs : IsLindelof s<VAR>hf₂ : f ≤ 𝓟 s<VAR>ht₁ : IsOpen t<VAR>ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t<GOAL>t ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, U ↑x ⋯
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>l : Filter X<VAR>CountableInterFilter l<VAR>hs : IsLindelof s<GOAL>Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>l : Filter X<VAR>CountableInterFilter l<VAR>hs : IsLindelof s<GOAL>Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<GOAL>∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty<GOAL>(s ∩ ⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ i ∈ b, IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i ∈ b, c i<GOAL>∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsLindelof s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsLindelof s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsLindelof ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsLindelof {x}
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<GOAL>IsLindelof s
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<GOAL>IsLindelof (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<GOAL>IsLindelof (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Finset ι<VAR>f : ι → Set X<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<GOAL>IsLindelof (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : ℕ → Set X<VAR>hK : ∀ (n : ℕ), IsLindelof (K n)<VAR>n : ℕ<GOAL>IsLindelof (Set.Accumulate K n)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hf : S.Countable<VAR>hc : ∀ s ∈ S, IsLindelof s<GOAL>IsLindelof (⋃₀ S)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsLindelof s<GOAL>IsLindelof (⋃₀ S)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Sort u_2<VAR>f : ι → Set X<VAR>Countable ι<VAR>h : ∀ (i : ι), IsLindelof (f i)<GOAL>IsLindelof (⋃ i, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Countable<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology X<VAR>hs : IsLindelof s<GOAL>s.Countable
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology X<GOAL>IsLindelof s ↔ s.Countable
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>ht : IsLindelof t<GOAL>IsLindelof (s ∪ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>a : X<GOAL>IsLindelof (insert a s)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>b : ι → Set X<VAR>hb : TopologicalSpace.IsTopologicalBasis (Set.range b)<VAR>hb' : ∀ (i : ι), IsLindelof (b i)<VAR>U : Set X<GOAL>IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.coLindelof X).HasBasis IsLindelof compl
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coLindelof X ↔ ∃ t, IsLindelof t ∧ tᶜ ⊆ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coLindelof X ↔ ∃ t, IsLindelof t ∧ sᶜ ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<GOAL>sᶜ ∈ Filter.coLindelof X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Filter.coLindelof X ≤ Filter.cofinite
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>y : Y<VAR>hf : Filter.Tendsto f (Filter.coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<GOAL>IsLindelof (insert y (Set.range f))
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Filter.coLindelof X ≤ Filter.coclosedLindelof X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>hs' : IsClosed s<GOAL>sᶜ ∈ Filter.coclosedLindelof X
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>self : LindelofSpace X<GOAL>IsLindelof Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsLindelof Set.univ ↔ LindelofSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>h : LindelofSpace X<GOAL>IsLindelof Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<VAR>f : Filter X<VAR>f.NeBot<VAR>CountableInterFilter f<GOAL>∃ x, ClusterPt x f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, U x = Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ ⋂ i ∈ u, t i = ∅<GOAL>LindelofSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>LindelofSpace X<VAR>h : IsClosed s<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsSigmaCompact s<GOAL>IsLindelof s
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>self : NonLindelofSpace X<GOAL>¬IsLindelof Set.univ
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NonLindelofSpace X<GOAL>¬IsLindelof Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NonLindelofSpace X<VAR>hs : IsLindelof s<GOAL>s ≠ Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<GOAL>Filter.coLindelof X = ⊥
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.coLindelof X).NeBot → NonLindelofSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.coLindelof X).NeBot ↔ NonLindelofSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>¬LindelofSpace X ↔ NonLindelofSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<VAR>DiscreteTopology X<GOAL>Countable X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, t.Countable ∧ ⋃ x ∈ t, interior (U x) = Set.univ
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>Filter.comap f (Filter.coLindelof Y) ≤ Filter.coLindelof X
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>LindelofSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsLindelof (Set.range f)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>LindelofSpace X<GOAL>IsLindelof (Set.diagonal X)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsLindelof s ↔ IsLindelof (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>IsLindelof s ↔ IsLindelof (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (Set.range f)<VAR>K : Set Y<VAR>hK : IsLindelof K<GOAL>IsLindelof (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<VAR>K : Set Y<VAR>hK : IsLindelof K<GOAL>IsLindelof (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>Filter.Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>s : Set { x // p x }<GOAL>IsLindelof s ↔ IsLindelof (Subtype.val '' s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsLindelof s ↔ IsLindelof Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsLindelof s ↔ LindelofSpace ↑s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>LindelofSpace ↑s<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLindelof s<VAR>hs' : DiscreteTopology ↑s<GOAL>s.Countable
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NonLindelofSpace X<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>NonLindelofSpace Y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : LindelofSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>LindelofSpace X
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>LindelofSpace X<VAR>hf : Continuous f<VAR>hsur : Function.Surjective f<GOAL>LindelofSpace Y
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>self : HereditarilyLindelofSpace X<GOAL>IsHereditarilyLindelof Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsHereditarilyLindelof s<VAR>ht : t ⊆ s<GOAL>IsLindelof t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsHereditarilyLindelof s<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>HereditarilyLindelofSpace X<VAR>s : Set X<GOAL>IsLindelof s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>HereditarilyLindelofSpace X<VAR>ι : Type u<VAR>U : ι → Set X<VAR>h : ∀ (i : ι), IsOpen (U i)<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
<VAR>X : Type u_1<VAR>p : OnePoint X → Prop<GOAL>(∀ (x : OnePoint X), p x) ↔ p OnePoint.infty ∧ ∀ (x : X), p ↑x
<VAR>X : Type u_1<VAR>p : OnePoint X → Prop<GOAL>(∃ x, p x) ↔ p OnePoint.infty ∨ ∃ x, p ↑x
<VAR>X : Type u_1<GOAL>Function.Injective OnePoint.some
<VAR>X : Type u_1<VAR>x y : X<GOAL>↑x = ↑y ↔ x = y
<VAR>X : Type u_1<VAR>x : X<GOAL>↑x ≠ OnePoint.infty
<VAR>X : Type u_1<VAR>x : X<GOAL>OnePoint.infty ≠ ↑x
<VAR>X : Type u_1<GOAL>IsCompl (Set.range OnePoint.some) {OnePoint.infty}
<VAR>X : Type u_1<GOAL>Set.range OnePoint.some ∪ {OnePoint.infty} = Set.univ
<VAR>X : Type u_1<GOAL>insert OnePoint.infty (Set.range OnePoint.some) = Set.univ
<VAR>X : Type u_1<GOAL>Set.range OnePoint.some ∩ {OnePoint.infty} = ∅
<VAR>X : Type u_1<GOAL>(Set.range OnePoint.some)ᶜ = {OnePoint.infty}
<VAR>X : Type u_1<GOAL>{OnePoint.infty}ᶜ = Set.range OnePoint.some
<VAR>X : Type u_1<VAR>s : Set X<GOAL>(OnePoint.some '' s)ᶜ = OnePoint.some '' sᶜ ∪ {OnePoint.infty}
<VAR>X : Type u_1<VAR>x : OnePoint X<GOAL>x ≠ OnePoint.infty ↔ ∃ y, ↑y = x
<VAR>X : Type u_1<VAR>x : OnePoint X<GOAL>x ∉ Set.range OnePoint.some ↔ x = OnePoint.infty
<VAR>X : Type u_1<GOAL>OnePoint.infty ∉ Set.range OnePoint.some
<VAR>X : Type u_1<VAR>s : Set X<GOAL>OnePoint.infty ∉ OnePoint.some '' s
<VAR>X : Type u_1<GOAL>OnePoint.some ⁻¹' {OnePoint.infty} = ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<GOAL>IsOpen s ↔ (OnePoint.infty ∈ s → IsCompact (OnePoint.some ⁻¹' s)ᶜ) ∧ IsOpen (OnePoint.some ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>h : OnePoint.infty ∈ s<GOAL>IsOpen s ↔ IsCompact (OnePoint.some ⁻¹' s)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>h : OnePoint.infty ∈ s<GOAL>IsOpen s ↔ IsClosed (OnePoint.some ⁻¹' s)ᶜ ∧ IsCompact (OnePoint.some ⁻¹' s)ᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>h : OnePoint.infty ∉ s<GOAL>IsOpen s ↔ IsOpen (OnePoint.some ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>h : OnePoint.infty ∈ s<GOAL>IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>h : OnePoint.infty ∉ s<GOAL>IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s) ∧ IsCompact (OnePoint.some ⁻¹' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsOpen (OnePoint.some '' s) ↔ IsOpen s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsOpen (OnePoint.some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed (OnePoint.some '' s) ↔ IsClosed s ∧ IsCompact s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h₁ : IsClosed s<VAR>h₂ : IsCompact s<GOAL>OnePoint.infty ∈ OnePoint.opensOfCompl s h₁ h₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous OnePoint.some
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsOpenMap OnePoint.some
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>OpenEmbedding OnePoint.some
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsOpen (Set.range OnePoint.some)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsClosed {OnePoint.infty}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 ↑x = Filter.map OnePoint.some (𝓝 x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : X<GOAL>𝓝[OnePoint.some '' s] ↑x = Filter.map OnePoint.some (𝓝[s] x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>x : X<GOAL>𝓝[s] ↑x = Filter.map OnePoint.some (𝓝[OnePoint.some ⁻¹' s] x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>Filter.comap OnePoint.some (𝓝 ↑x) = 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>𝓝[≠] OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>𝓝 OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X) ⊔ pure OnePoint.infty
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Filter.Tendsto OnePoint.some (Filter.coclosedCompact X) (𝓝 OnePoint.infty)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(𝓝 OnePoint.infty).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => OnePoint.some '' sᶜ ∪ {OnePoint.infty}
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Filter.comap OnePoint.some (𝓝 OnePoint.infty) = Filter.coclosedCompact X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : Filter (OnePoint X)<GOAL>f ≤ 𝓝 OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' sᶜ ∪ {OnePoint.infty} ∈ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : Ultrafilter (OnePoint X)<GOAL>↑f ≤ 𝓝 OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' s ∉ f