no goals
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ T0Space α ↔ ∀ (a b : α), a ≠ b → ¬a ∈ closure {b} ∨ ¬b ∈ closure {a}
simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]