preimage_of_isClosedEmbedding — Mathlib

English

If f is a closed embedding and hf' ensures compactness of the range complement, then the preimage of a constructible set is constructible.

Русский

Если f — замкнутое вложение и hf' обеспечивает компактность дополняRange, то предобраз конструируемого множества конструируем.

LaTeX

$$$\\forall f:\\ X \\to Y, IsClosedEmbedding(f) \\Rightarrow IsCompact((range f)^{c}) \\Rightarrow IsConstructible(s) \\Rightarrow IsConstructible(f^{-1}(s)).$$$

Lean4

@[stacks 09YE]
theorem preimage_of_isClosedEmbedding {s : Set Y} (hf : IsClosedEmbedding f) (hf' : IsCompact (range f)ᶜ)
    (hs : IsConstructible s) : IsConstructible (f ⁻¹' s) :=
  hs.preimage hf.continuous fun _t _ ht ↦ ht.preimage_of_isClosedEmbedding hf hf'

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