English
If f is an open embedding with retrocompact range, then the image f''s of constructible s is constructible.
Русский
Пусть f — открытое вложение с ретрокомпактным диапазоном; образ f''s множества конструируемого является конструируемым.
LaTeX
$$$\\forall f:\\ X \\to Y, IsOpenEmbedding(f) \\Rightarrow IsRetrocompact(\\text{range}(f)) \\Rightarrow IsConstructible(s) \\Rightarrow IsConstructible(f''s).$$$
Lean4
@[stacks 09YD]
theorem image_of_isOpenEmbedding (hfopen : IsOpenEmbedding f) (hfcomp : IsRetrocompact (range f))
(hs : IsConstructible s) : IsConstructible (f '' s) := by
induction hs using IsConstructible.empty_union_induction with
| open_retrocompact U hUopen hUcomp =>
exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <| hfopen.isOpenMap _ hUopen
| union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
| compl s hs hs' =>
rw [← range_diff_image hfopen.injective]
exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'
