X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
inhabit X
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (↑CofiniteTopology.of.symm x))
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 (↑CofiniteTopology.of ↑default))
      (𝓝 (↑CofiniteTopology.of.symm (↑CofiniteTopology.of ↑default)))
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (↑CofiniteTopology.of.symm x))
use CofiniteTopology.of ↑(default : X)
no goals
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 (↑CofiniteTopology.of ↑default))
      (𝓝 (↑CofiniteTopology.of.symm (↑CofiniteTopology.of ↑default)))
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
  (finite_singleton ((default : X) : OnePoint X)).infinite_compl