ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>S : Set (Set (Set α))<GOAL>TopologicalSpace.generateFrom (⋃₀ S) = ⨅ s ∈ S, TopologicalSpace.generateFrom s
<VAR>α : Type u<VAR>T : Set (TopologicalSpace α)<GOAL>{s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
<VAR>α : Type u<VAR>a b : TopologicalSpace α<GOAL>TopologicalSpace.generateFrom ({s | IsOpen s} ∪ {s | IsOpen s}) = a ⊓ b
<VAR>α : Type u<VAR>ι : Sort v<VAR>f : ι → TopologicalSpace α<GOAL>TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) = ⨅ i, f i
<VAR>α : Type u<VAR>a b : TopologicalSpace α<GOAL>TopologicalSpace.generateFrom ({s | IsOpen s} ∩ {s | IsOpen s}) = a ⊔ b
<VAR>α : Type u<VAR>ι : Sort v<VAR>f : ι → TopologicalSpace α<GOAL>TopologicalSpace.generateFrom (⋂ i, {s | IsOpen s}) = ⨆ i, f i
<VAR>α : Type u<VAR>ι : Sort v<VAR>f : ι → Set (Set α)<VAR>hf : ∀ (i : ι), {s | IsOpen s} = f i<GOAL>TopologicalSpace.generateFrom (⋂ i, f i) = ⨆ i, TopologicalSpace.generateFrom (f i)
<VAR>α : Type u<VAR>ι : Sort v<VAR>t : ι → TopologicalSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ (i : ι), IsOpen s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<GOAL>Function.Injective DFunLike.coe
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>t : ↑I<GOAL>F (t, 0) = x₀
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>t : ↑I<GOAL>F (t, 1) = x₁
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<GOAL>F.eval 0 = p₀
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<GOAL>F.eval 1 = p₁
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<VAR>x : ↑I × ↑I<GOAL>(Path.Homotopy.refl p) x = p x.2
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>x : ↑I × ↑I<GOAL>F.symm x = F (σ x.1, x.2)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<GOAL>F.symm.symm = F
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<GOAL>Function.Bijective Path.Homotopy.symm
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ p₂ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>G : p₁.Homotopy p₂<VAR>x : ↑I × ↑I<GOAL>(F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ p₂ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>G : p₁.Homotopy p₂<GOAL>(F.trans G).symm = G.symm.trans F.symm
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ q₀ q₁ : Path x₀ x₁<VAR>F : p₀.Homotopy p₁<VAR>h₀ : p₀ = q₀<VAR>h₁ : p₁ = q₁<VAR>a : ↑I × ↑I<GOAL>(F.cast h₀ h₁) a = F a
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ : X<VAR>p₀ q₀ : Path x₀ x₁<VAR>p₁ q₁ : Path x₁ x₂<VAR>F : p₀.Homotopy q₀<VAR>G : p₁.Homotopy q₁<VAR>x : ↑I × ↑I<GOAL>(F.hcomp G) x = if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ : X<VAR>p₀ q₀ : Path x₀ x₁<VAR>p₁ q₁ : Path x₁ x₂<VAR>F : p₀.Homotopy q₀<VAR>G : p₁.Homotopy q₁<VAR>t : ↑I<GOAL>(F.hcomp G) (t, ⟨1 / 2, ⋯⟩) = x₁
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p q : Path x₀ x₁<VAR>F : p.Homotopy q<VAR>x : ↑I × ↑I<GOAL>F.symm₂ x = F (x.1, σ x.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p q : Path x₀ x₁<VAR>F : p.Homotopy q<VAR>f : C(X, Y)<GOAL>∀ (a : ↑I × ↑I), (F.map f) a = (⇑f ∘ ⇑F) a
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<GOAL>p.Homotopic p
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>h : p₀.Homotopic p₁<GOAL>p₁.Homotopic p₀
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p₀ p₁ p₂ : Path x₀ x₁<VAR>h₀ : p₀.Homotopic p₁<VAR>h₁ : p₁.Homotopic p₂<GOAL>p₀.Homotopic p₂
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<GOAL>Equivalence Path.Homotopic
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p q : Path x₀ x₁<VAR>h : p.Homotopic q<VAR>f : C(X, Y)<GOAL>(p.map ⋯).Homotopic (q.map ⋯)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ : X<VAR>p₀ p₁ : Path x₀ x₁<VAR>q₀ q₁ : Path x₁ x₂<VAR>hp : p₀.Homotopic p₁<VAR>hq : q₀.Homotopic q₁<GOAL>(p₀.trans q₀).Homotopic (p₁.trans q₁)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ : X<VAR>P₀ : Path x₀ x₁<VAR>P₁ : Path x₁ x₂<GOAL>⟦P₀.trans P₁⟧ = Path.Homotopic.Quotient.comp ⟦P₀⟧ ⟦P₁⟧
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>P₀ : Path x₀ x₁<VAR>f : C(X, Y)<GOAL>⟦P₀.map ⋯⟧ = Path.Homotopic.Quotient.mapFn ⟦P₀⟧ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ x₃ : X<VAR>p₁ : Path x₀ x₁<VAR>p₂ : Path x₂ x₃<VAR>hp : ∀ (t : ↑I), p₁ t = p₂ t<GOAL>HEq ⟦p₁⟧ ⟦p₂⟧
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<GOAL>∀ (a : ↑I × Y), p.toHomotopyConst a = p a.1
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>Nonempty Y<GOAL>(ContinuousMap.const Y x₀).Homotopic (ContinuousMap.const Y x₁) ↔ Joined x₀ x₁
<VAR>X : Type u<VAR>UniformSpace X<GOAL>↑(UniformSpaceCat.of X) = X
<VAR>X Y Z : UniformSpaceCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.forget UniformSpaceCat).map (f ≫ g) = (CategoryTheory.forget UniformSpaceCat).map g ∘ (CategoryTheory.forget UniformSpaceCat).map f
<VAR>X : UniformSpaceCat<GOAL>(CategoryTheory.forget UniformSpaceCat).map (𝟙 X) = id
<VAR>X Y : UniformSpaceCat<VAR>f : ↑X → ↑Y<VAR>hf : UniformContinuous f<GOAL>↑⟨f, hf⟩ = f
<VAR>X Y : UniformSpaceCat<VAR>f g : X ⟶ Y<GOAL>(CategoryTheory.forget UniformSpaceCat).map f = (CategoryTheory.forget UniformSpaceCat).map g → f = g
<VAR>self : CpltSepUniformSpace<GOAL>CompleteSpace self.α
<VAR>self : CpltSepUniformSpace<GOAL>T0Space self.α
<VAR>X : Type u<VAR>UniformSpace X<VAR>CompleteSpace X<VAR>T0Space X<GOAL>(CpltSepUniformSpace.of X).α = X
<VAR>X : UniformSpaceCat<VAR>x : (CategoryTheory.forget UniformSpaceCat).obj X<GOAL>(CategoryTheory.forget UniformSpaceCat).map X.completionHom x = ↑((CategoryTheory.forget UniformSpaceCat).obj X) x
<VAR>X : UniformSpaceCat<VAR>Y : CpltSepUniformSpace<VAR>f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y<VAR>x : (CategoryTheory.forget CpltSepUniformSpace).obj (UniformSpaceCat.completionFunctor.obj X)<GOAL>(UniformSpaceCat.extensionHom f) x = UniformSpace.Completion.extension ((CategoryTheory.forget UniformSpaceCat).map f) x
<VAR>X : UniformSpaceCat<VAR>Y : CpltSepUniformSpace<VAR>f : (CpltSepUniformSpace.of (UniformSpace.Completion ↑X)).toUniformSpace ⟶ Y.toUniformSpace<GOAL>UniformSpaceCat.extensionHom (X.completionHom ≫ f) = f
<VAR>B X : TopCat<VAR>π : X ⟶ B<GOAL>CategoryTheory.EffectiveEpi π ↔ QuotientMap ⇑π
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<GOAL>IsGenericPoint x S ↔ closure {x} = S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<GOAL>closure {x} = S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsGenericPoint x (closure {x})
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<GOAL>IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x y : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<GOAL>x ⤳ y ↔ y ∈ S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x y : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<VAR>h' : y ∈ S<GOAL>x ⤳ y
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<GOAL>x ∈ S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<GOAL>IsClosed S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<GOAL>IsIrreducible S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x y : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<VAR>h' : IsGenericPoint y S<GOAL>Inseparable x y
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x y : α<VAR>S : Set α<VAR>T0Space α<VAR>h : IsGenericPoint x S<VAR>h' : IsGenericPoint y S<GOAL>x = y
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S U : Set α<VAR>h : IsGenericPoint x S<VAR>hU : IsOpen U<GOAL>x ∈ U ↔ (S ∩ U).Nonempty
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S U : Set α<VAR>h : IsGenericPoint x S<VAR>hU : IsOpen U<GOAL>Disjoint S U ↔ x ∉ U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S Z : Set α<VAR>h : IsGenericPoint x S<VAR>hZ : IsClosed Z<GOAL>x ∈ Z ↔ S ⊆ Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>S : Set α<VAR>h : IsGenericPoint x S<VAR>f : α → β<VAR>hf : Continuous f<GOAL>IsGenericPoint (f x) (closure (f '' S))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>S : Set α<VAR>hS : IsClosed S<VAR>hxS : x ∈ S<GOAL>IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
<VAR>α : Type u_3<VAR>TopologicalSpace α<GOAL>QuasiSober α ↔ ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>self : QuasiSober α<VAR>S : Set α<GOAL>IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSober α<VAR>S : Set α<VAR>hS : IsIrreducible S<GOAL>IsGenericPoint hS.genericPoint (closure S)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSober α<VAR>S : Set α<VAR>hS : IsIrreducible S<GOAL>closure {hS.genericPoint} = closure S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSober α<VAR>IrreducibleSpace α<GOAL>IsGenericPoint (genericPoint α) ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSober α<VAR>IrreducibleSpace α<GOAL>closure {genericPoint α} = ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>QuasiSober α<VAR>IrreducibleSpace α<VAR>x : α<GOAL>genericPoint α ⤳ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : ClosedEmbedding f<VAR>QuasiSober β<GOAL>QuasiSober α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>QuasiSober β<GOAL>QuasiSober α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<GOAL>QuasiSober α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>self : TopologicalSpace.IsTopologicalBasis s<VAR>t₁ : Set α<GOAL>t₁ ∈ s → ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>self : TopologicalSpace.IsTopologicalBasis s<GOAL>⋃₀ s = Set.univ
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>self : TopologicalSpace.IsTopologicalBasis s<GOAL>t = TopologicalSpace.generateFrom s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>h : TopologicalSpace.IsTopologicalBasis s<GOAL>TopologicalSpace.IsTopologicalBasis (insert ∅ s)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>h : TopologicalSpace.IsTopologicalBasis s<GOAL>TopologicalSpace.IsTopologicalBasis (s \ {∅})
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>hs : t = TopologicalSpace.generateFrom s<GOAL>TopologicalSpace.IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>hsg : t = TopologicalSpace.generateFrom s<VAR>hsi : FiniteInter s<GOAL>TopologicalSpace.IsTopologicalBasis s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>r : Set (Set α)<VAR>hsg : t = TopologicalSpace.generateFrom r<VAR>hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r<GOAL>TopologicalSpace.IsTopologicalBasis (insert Set.univ r)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id<GOAL>TopologicalSpace.IsTopologicalBasis s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set (Set α)<VAR>h_open : ∀ u ∈ s, IsOpen u<VAR>h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u<GOAL>TopologicalSpace.IsTopologicalBasis s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<GOAL>s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<GOAL>IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun t => t ∈ b ∧ a ∈ t) fun t => t
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>hs : s ∈ b<GOAL>IsOpen s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>hs : s ∈ b<VAR>ha : a ∈ s<GOAL>s ∈ 𝓝 a
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>a : α<VAR>u : Set α<VAR>au : a ∈ u<VAR>ou : IsOpen u<GOAL>∃ v ∈ b, a ∈ v ∧ v ⊆ u
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>u : Set α<VAR>ou : IsOpen u<GOAL>u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>u : Set α<VAR>ou : IsOpen u<GOAL>∃ S ⊆ B, u = ⋃₀ S
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>u : Set α<GOAL>IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>u : Set α<VAR>ou : IsOpen u<GOAL>∃ β f, u = ⋃ i, f i ∧ ∀ (i : β), f i ∈ B
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<GOAL>∀ {t_1 : Set α}, TopologicalSpace.IsTopologicalBasis B → IsOpen s → (∀ U ∈ B, U ⊆ s → U ⊆ t_1) → s ⊆ t_1
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<GOAL>∀ {t_1 : Set α}, TopologicalSpace.IsTopologicalBasis B → IsOpen s → IsOpen t_1 → (∀ U ∈ B, U ⊆ s ↔ U ⊆ t_1) → s = t_1
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>s : Set α<VAR>a : α<GOAL>a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>b : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>s : Set α<GOAL>Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>B : Set (Set α)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>f : α → β<GOAL>IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>hb : TopologicalSpace.IsTopologicalBasis B<VAR>u : Set α<VAR>hu : u.Nonempty<VAR>ou : IsOpen u<GOAL>∃ v ∈ B, v.Nonempty ∧ v ⊆ u
<VAR>α : Type u<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.IsTopologicalBasis {U | IsOpen U}
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>f : α → β<VAR>T : Set (Set β)<VAR>hf : Inducing f<VAR>h : TopologicalSpace.IsTopologicalBasis T<GOAL>TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
<VAR>α : Type u<VAR>β : Type u_1<VAR>s : TopologicalSpace β<VAR>f : α → β<VAR>T : Set (Set β)<VAR>h : TopologicalSpace.IsTopologicalBasis T<GOAL>TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
<VAR>β : Type u_1<VAR>t₁ t₂ : TopologicalSpace β<VAR>B₁ B₂ : Set (Set β)<VAR>h₁ : TopologicalSpace.IsTopologicalBasis B₁<VAR>h₂ : TopologicalSpace.IsTopologicalBasis B₂<GOAL>TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x x_1 => x ∩ x_1) B₁ B₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>γ : Type u_2<VAR>s : TopologicalSpace β<VAR>B₁ : Set (Set α)<VAR>B₂ : Set (Set β)<VAR>h₁ : TopologicalSpace.IsTopologicalBasis B₁<VAR>h₂ : TopologicalSpace.IsTopologicalBasis B₂<VAR>f₁ : γ → α<VAR>f₂ : γ → β<GOAL>TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x x_1 => f₁ ⁻¹' x ∩ f₂ ⁻¹' x_1) B₁ B₂)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>B₁ : Set (Set α)<VAR>B₂ : Set (Set β)<VAR>h₁ : TopologicalSpace.IsTopologicalBasis B₁<VAR>h₂ : TopologicalSpace.IsTopologicalBasis B₂<GOAL>TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>Uo : ∀ (i : ι), IsOpen (U i)<VAR>Uc : ⋃ i, U i = Set.univ<VAR>b : (i : ι) → Set (Set ↑(U i))<VAR>hb : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (b i)<GOAL>TopologicalSpace.IsTopologicalBasis (⋃ i, Set.image Subtype.val '' b i)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>B : Set (Set β)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>f : α → β<GOAL>Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>B : Set (Set β)<VAR>hB : TopologicalSpace.IsTopologicalBasis B<VAR>f : α → β<VAR>hf : ∀ s ∈ B, IsOpen (f ⁻¹' s)<GOAL>Continuous f
<VAR>α : Type u<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.SeparableSpace α ↔ ∃ s, s.Countable ∧ Dense s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>self : TopologicalSpace.SeparableSpace α<GOAL>∃ s, s.Countable ∧ Dense s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<GOAL>∃ s, s.Countable ∧ Dense s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>Nonempty α<GOAL>∃ u, DenseRange u
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>Nonempty α<GOAL>DenseRange (TopologicalSpace.denseSeq α)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Type u_2<VAR>Countable ι<VAR>u : ι → α<VAR>hu : DenseRange u<GOAL>TopologicalSpace.SeparableSpace α
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : DenseRange f<VAR>h' : Continuous f<GOAL>TopologicalSpace.SeparableSpace β
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : QuotientMap f<GOAL>TopologicalSpace.SeparableSpace β
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>DiscreteTopology α<GOAL>TopologicalSpace.SeparableSpace α ↔ Countable α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<GOAL>Countable ι
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>a : Set ι<VAR>h : a.PairwiseDisjoint s<VAR>ho : ∀ i ∈ a, IsOpen (s i)<VAR>hne : ∀ i ∈ a, (s i).Nonempty<GOAL>a.Countable
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>a : Set ι<VAR>h : a.PairwiseDisjoint s<VAR>ha : ∀ i ∈ a, (interior (s i)).Nonempty<GOAL>a.Countable
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s u : Set α<VAR>hs : TopologicalSpace.IsSeparable s<VAR>hu : u ⊆ s<GOAL>TopologicalSpace.IsSeparable u
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Sort u_2<VAR>Countable ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), TopologicalSpace.IsSeparable (s i)<GOAL>TopologicalSpace.IsSeparable (⋃ i, s i)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Sort u_2<VAR>Countable ι<VAR>s : ι → Set α<GOAL>TopologicalSpace.IsSeparable (⋃ i, s i) ↔ ∀ (i : ι), TopologicalSpace.IsSeparable (s i)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<GOAL>∀ {t_1 : Set α}, TopologicalSpace.IsSeparable (s ∪ t_1) ↔ TopologicalSpace.IsSeparable s ∧ TopologicalSpace.IsSeparable t_1
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s u : Set α<VAR>hs : TopologicalSpace.IsSeparable s<VAR>hu : TopologicalSpace.IsSeparable u<GOAL>TopologicalSpace.IsSeparable (s ∪ u)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<GOAL>TopologicalSpace.IsSeparable (closure s) ↔ TopologicalSpace.IsSeparable s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>hs : s.Countable<GOAL>TopologicalSpace.IsSeparable s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>TopologicalSpace.IsSeparable s
<VAR>ι : Type u_2<VAR>Countable ι<VAR>X : ι → Type u_3<VAR>s : (i : ι) → Set (X i)<VAR>(i : ι) → TopologicalSpace (X i)<VAR>h : ∀ (i : ι), TopologicalSpace.IsSeparable (s i)<GOAL>TopologicalSpace.IsSeparable (Set.univ.pi s)
<VAR>ι : Type u_2<VAR>Countable ι<VAR>α : ι → Type u_3<VAR>s : (i : ι) → Set (α i)<VAR>(i : ι) → TopologicalSpace (α i)<VAR>h : ∀ (i : ι), TopologicalSpace.IsSeparable (s i)<GOAL>TopologicalSpace.IsSeparable {f | ∀ (i : ι), f i ∈ s i}
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>s : Set α<GOAL>∀ {t_1 : Set β}, TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable t_1 → TopologicalSpace.IsSeparable (s ×ˢ t_1)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>s : Set α<VAR>hs : TopologicalSpace.IsSeparable s<VAR>f : α → β<VAR>hf : Continuous f<GOAL>TopologicalSpace.IsSeparable (f '' s)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>hs : Dense s<GOAL>TopologicalSpace.IsSeparable s ↔ TopologicalSpace.SeparableSpace α
<VAR>α : Type u<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.IsSeparable Set.univ ↔ TopologicalSpace.SeparableSpace α
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.SeparableSpace α<VAR>f : α → β<VAR>hf : Continuous f<GOAL>TopologicalSpace.IsSeparable (Set.range f)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>s : Set α<VAR>TopologicalSpace.SeparableSpace ↑s<GOAL>TopologicalSpace.IsSeparable s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>h : TopologicalSpace.SeparableSpace α<VAR>s : Set α<GOAL>TopologicalSpace.IsSeparable s
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>t : ι → TopologicalSpace β<VAR>T : ι → Set (Set β)<VAR>h_basis : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)<GOAL>TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>X : ι → Type u_3<VAR>t : (i : ι) → TopologicalSpace (X i)<VAR>T : (i : ι) → Set (Set (X i))<VAR>cond : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)<VAR>f : (i : ι) → β → X i<GOAL>TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>T : (i : ι) → Set (Set (X i))<VAR>cond : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)<GOAL>TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<GOAL>TopologicalSpace.IsTopologicalBasis {s | ∃ x, s = {x}}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>B : Set (Set α)<VAR>h : TopologicalSpace.IsTopologicalBasis B<VAR>p : α → Prop<GOAL>TopologicalSpace.IsTopologicalBasis (Set.preimage Subtype.val '' B)
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (π i)<VAR>i : ι<GOAL>IsOpenMap (Function.eval i)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hs : Dense s<GOAL>∃ t ⊆ s, t.Countable ∧ Dense t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>s : Set α<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hs : Dense s<GOAL>∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.SeparableSpace α<VAR>PartialOrder α<GOAL>∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>self : FirstCountableTopology α<VAR>a : α<GOAL>(𝓝 a).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>FirstCountableTopology β<VAR>f : α → β<GOAL>FirstCountableTopology α
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_1<VAR>TopologicalSpace β<VAR>FirstCountableTopology β<VAR>f : α → β<VAR>hf : Inducing f<GOAL>FirstCountableTopology α