isOpen_iff_preimage_isOpen — Mathlib

English

If f is an open embedding, then IsOpenMap f ↔ IsOpenMap (g ∘ f).

Русский

Если f — открытое вложение, то IsOpenMap f эквивалственно IsOpenMap (g ∘ f).

LaTeX

$$$ \text{IsOpenEmbedding } g \rightarrow (\text{IsOpenMap } f \leftrightarrow \text{IsOpenMap } (g \circ f)) $$$

Lean4

theorem isOpen_iff_preimage_isOpen (hf : IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ range f) :
    IsOpen s ↔ IsOpen (f ⁻¹' s) := by
  rw [hf.isOpen_iff_image_isOpen, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]

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