English
Let f: X → Y be a map between topological spaces. The map f is open if and only if for every x ∈ X and every filter l on Y, whenever l clusters at f(x), then l comapped back to x clusters at x; i.e., ClusterPt (f x) l → ClusterPt x (comap f l).
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Отображение открыто тогда и только тогда, когда для каждого x ∈ X и каждого фильтра l на Y, если l является кластерной точкой f(x), то x имеет кластерную точку относительно обратного образа l; то есть ClusterPt (f x) l → ClusterPt x (comap f l).
LaTeX
$$$\\text{Open}(f) \\iff ∀ x:X, ∀ l:\\text{Filter } Y,\\ ClusterPt (f x)\\,l \\rightarrow ClusterPt x (\\mathrm{comap}\\ f\\ l)$$$
Lean4
theorem isOpenMap_iff_clusterPt_comap : IsOpenMap f ↔ ∀ x l, ClusterPt (f x) l → ClusterPt x (comap f l) :=
by
refine ⟨fun hf _ _ ↦ hf.clusterPt_comap, fun h ↦ ?_⟩
simp only [isOpenMap_iff_nhds_le, le_map_iff]
intro x s hs
contrapose! hs
rw [← mem_interior_iff_mem_nhds, mem_interior_iff_not_clusterPt_compl, not_not] at hs ⊢
exact (h _ _ hs).mono <| by simp [subset_preimage_image]
