English
If a subset s is quasi-separated and f is an embedding, then the image f''s is quasi-separated.
Русский
Если множество s квазиразделимо, и f — вложение, то образ f''s тоже квазиразделим.
LaTeX
$$$IsQuasiSeparated(s)\\quad\\text{and}\\quad IsEmbedding(f)\\ \\Rightarrow \\ IsQuasiSeparated(f''s)$$$
Lean4
theorem image_of_isEmbedding {s : Set α} (H : IsQuasiSeparated s) (h : IsEmbedding f) : IsQuasiSeparated (f '' s) :=
by
intro U V hU hU' hU'' hV hV' hV''
convert (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image h.continuous
· symm
rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left]
exact Set.inter_subset_left.trans (hU.trans (Set.image_subset_range _ _))
· intro x hx
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
exact hU hx
· rw [h.isCompact_iff]
convert hU''
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
exact hU.trans (Set.image_subset_range _ _)
· intro x hx
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
exact hV hx
· rw [h.isCompact_iff]
convert hV''
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
exact hV.trans (Set.image_subset_range _ _)
