isOpen_iff_image_isOpen — Mathlib

English

For an open embedding f, IsOpen s is equivalent to IsOpen (f'' s).

Русский

Для открытого вложения f множество s открыто тогда и только тогда, когда образ f''s открыт в целевом пространстве.

LaTeX

$$$ \text{IsOpenEmbedding } f \rightarrow \forall s, \text{IsOpen } s \leftrightarrow \text{IsOpen } (f'' s) $$$

Lean4

theorem isOpen_iff_image_isOpen (hf : IsOpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s)
    where
  mp := hf.isOpenMap s
  mpr h := by convert ← h.preimage hf.isEmbedding.continuous; apply preimage_image_eq _ hf.injective

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