α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
x✝ : x ≠ y
⊢ (∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) ↔ Disjoint (𝓝 x) (𝓝 y)
α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ T2Space α ↔ ∀ (x y : α), x ≠ y → Disjoint (𝓝 x) (𝓝 y)
refine (t2Space_iff α).trans (forall₃_congr fun x y _ => ?_)
no goals
α : Type u
β : Type v
inst✝ : TopologicalSpace α
x y : α
x✝ : x ≠ y
⊢ (∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) ↔ Disjoint (𝓝 x) (𝓝 y)
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), exists_prop, ← exists_and_left,
  and_assoc, and_comm, and_left_comm]