English
If f: X → Y is an open embedding and f x ≠ f y for x ≠ y, then there exist disjoint open sets in Y separating f(x) and f(y).
Русский
Если f — открытое вложение, и f(x) ≠ f(y) тогда существуют раздельные открытые множества в Y, разделяющие f(x) и f(y).
LaTeX
$$$\\exists u,v \\subset Y,\\ IsOpen(u) \\wedge IsOpen(v) \\wedge f(x) \\in u \\wedge f(y) \\in v \\wedge Disjoint(u,v)$.$$
Lean4
theorem separated_by_isOpenEmbedding [TopologicalSpace Y] [T2Space X] {f : X → Y} (hf : IsOpenEmbedding f) {x y : X}
(h : x ≠ y) : ∃ u v : Set Y, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v :=
let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
⟨f '' u, f '' v, hf.isOpenMap _ uo, hf.isOpenMap _ vo, mem_image_of_mem _ xu, mem_image_of_mem _ yv,
disjoint_image_of_injective hf.injective uv⟩
