preimage_of_isOpenEmbedding — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{IsLocallyConstructible}(f^{-1}(s)) \\text{ given } \\operatorname{IsLocallyConstructible}(s) \\text{ and } \\text{IsOpenEmbedding}(f).$$$

Lean4

theorem preimage_of_isOpenEmbedding {s : Set Y} (hs : IsLocallyConstructible s) (hf : IsOpenEmbedding f) :
    IsLocallyConstructible (f ⁻¹' s) := by
  intro x
  obtain ⟨U, hxU, hU, H⟩ := hs (f x)
  exact
    ⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
      (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩

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