isConstructible_preimage_iff_of_isOpenEmbedding

English

If f is an open embedding with retrocompact range, then for s subset range f, IsConstructible(f^{-1}(s)) is equivalent to IsConstructible(s).

Русский

Если f — открытое вложение с ретрокомпактным диапазоном, то для s ⊆ range f выполняется сопоставление IsConstructible(f^{-1}(s)) ⇔ IsConstructible(s).

LaTeX

$$$IsConstructible(f^{-1}(s)) \\iff IsConstructible(s) \\quad \\text{when } s \\subseteq \\text{range}(f) \\text{ and } f \\text{ is open embedding}.$$$

Lean4

theorem isConstructible_preimage_iff_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f)
    (hfcomp : IsRetrocompact (range f)) (hsf : s ⊆ range f) : IsConstructible (f ⁻¹' s) ↔ IsConstructible s
    where
  mp hs := by simpa [image_preimage_eq_range_inter, inter_eq_right.2 hsf] using hs.image_of_isOpenEmbedding hf hfcomp
  mpr := .preimage_of_isOpenEmbedding hf

Похожие утверждения