preimage_of_isOpenEmbedding — Mathlib

English

If f is an open embedding and s is constructible, then the preimage f^{-1}(s) is constructible.

Русский

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

LaTeX

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

Lean4

@[stacks 005J]
theorem preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f) (hs : IsConstructible s) :
    IsConstructible (f ⁻¹' s) :=
  hs.preimage hf.continuous fun _t _ ht ↦ ht.preimage_of_isOpenEmbedding hf

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