English
If f: X → Y is continuous and f x ≠ f y in Y, then there exist open sets u,v in X separating x and y with disjoint preimages under f.
Русский
Пусть f: X → Y непрерывно, и f(x) ≠ f(y). Тогда существуют открытые множества u,v в X, содержащие x и y соответственно, such что u ∩ v = ∅ после отображения через f.
LaTeX
$$$\\exists u,v \\subset X,\\ IsOpen(u) \\wedge IsOpen(v) \\wedge x∈u \\wedge y∈v \\wedge Disjoint(u,v)$ после применения preimage под f.$$
Lean4
theorem separated_by_continuous [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) {x y : X}
(h : f x ≠ f y) : ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v :=
let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
⟨f ⁻¹' u, f ⁻¹' v, uo.preimage hf, vo.preimage hf, xu, yv, uv.preimage _⟩
