restrictPreimage_isOpenEmbedding — Mathlib

English

If f is an open embedding, restricting its preimage preserves openness embedding.

Русский

Если f открытое внедрение, ограничение предобраза сохраняет открытую вложенность.

LaTeX

$$$IsOpenEmbedding f \\rightarrow IsOpenEmbedding (s.restrictPreimage f)$$$

Lean4

theorem restrictPreimage_isOpenEmbedding (s : Set β) (h : IsOpenEmbedding f) : IsOpenEmbedding (s.restrictPreimage f) :=
  ⟨h.1.restrictPreimage s, (s.range_restrictPreimage f).symm ▸ continuous_subtype_val.isOpen_preimage _ h.isOpen_range⟩

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