no goals
X : Type u_1
Y : Type ?u.28647
Z : Type ?u.28650
α : Type ?u.28653
ι : Type ?u.28656
π : ι → Type ?u.28661
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ ¬(x ~ᵢ y) ↔ ∃ s, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)
simp [inseparable_iff_forall_open, ← xor_iff_not_iff]