English
Let f: X → Y be a map between topological spaces. Then f is open if and only if for every subset s ⊆ X, the image of the interior of s is contained in the interior of the image of s; i.e., f''(int s) ⊆ int(f''s).
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Тогда f открыто тогда и только тогда, когда для любого множества s ⊆ X образ внутренности s содержится в внутренности образа s; то есть f''(int s) ⊆ int(f''s).
LaTeX
$$$\\text{Open}(f) \\iff \\forall s\\subseteq X,\\ f''(\\operatorname{int} s) \\subseteq \\operatorname{int}(f''s)$$$
Lean4
theorem isOpenMap_iff_image_interior : IsOpenMap f ↔ ∀ s, f '' interior s ⊆ interior (f '' s) :=
⟨IsOpenMap.image_interior_subset, fun hs u hu =>
subset_interior_iff_isOpen.mp <| by simpa only [hu.interior_eq] using hs u⟩
