English
If f is continuous and the preimage of every open retrocompact set is retrocompact, then the preimage of every constructible set is constructible.
Русский
Если функция f непрерывна и предобраз каждого открытого ретрокомпактного множества является ретрокомпактным, то предобраз любого конструируемого множества является конструируемым.
LaTeX
$$$\\forall f:\\ X \\to Y, \\text{Continuous}(f) \\Rightarrow (\\forall s, IsOpen(s) \\rightarrow IsRetrocompact(s) \\Rightarrow IsRetrocompact(f^{-1}(s))) \\Rightarrow (IsConstructible(s) \\Rightarrow IsConstructible(f^{-1}(s))).$$$
Lean4
/-- If `f` is continuous and is such that preimages of open retrocompact sets are retrocompact,
then preimages of constructible sets are constructible. -/
@[stacks 005I]
theorem preimage {s : Set Y} (hfcont : Continuous f) (hf : ∀ s, IsOpen s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s))
(hs : IsConstructible s) : IsConstructible (f ⁻¹' s) := by
induction hs using IsConstructible.empty_union_induction with
| open_retrocompact U hUopen hUcomp => exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont
| union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht'
| compl s hs hs' => rw [preimage_compl]; exact hs'.compl
