English
If x and y are not inseparable, there exist open neighborhoods U and V with x ∈ U, y ∈ V, and U ∩ V = ∅.
Русский
Если x и y не inseparable, существуют открытые окрестности U и V с x ∈ U, y ∈ V и U ∩ V = ∅.
LaTeX
$$$\\forall X [TopologicalSpace X] [R1Space X],\\ (\\neg Inseparable x y) \\Rightarrow \\exists U,V: IsOpen U \\land IsOpen V \\land x \\in U \\land y \\in V \\land Disjoint U V.$$$
Lean4
theorem r1_separation {x y : X} (h : ¬Inseparable x y) :
∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v :=
by
rw [← disjoint_nhds_nhds_iff_not_inseparable, (nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)] at h
obtain ⟨u, ⟨hxu, hu⟩, v, ⟨hyv, hv⟩, huv⟩ := h
exact ⟨u, v, hu, hv, hxu, hyv, huv⟩
