no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.143258
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
⊢ IsIrreducible S ↔ ∃ x, S = {x}
rw [IsIrreducible, isPreirreducible_iff_subsingleton,
  exists_eq_singleton_iff_nonempty_subsingleton]