isOpenMap_iff_nhds_le — Mathlib

English

Let X, Y be topological spaces and f: X → Y. Then f is an open map if and only if for every x ∈ X, the neighborhood filter of f(x) is contained in the image under f of the neighborhood filter of x.

Русский

Пусть X, Y — топологические пространства и f: X → Y. Тогда отображение f открыто тогда и только тогда, когда для каждого x ∈ X окрестностный фильтр 𝒩(f(x)) содержится в образе фильтра 𝒩(x) под отображением f.

LaTeX

$$$\\text{Open}(f) \\iff \\forall x:X, \\ 𝓝(f(x)) \\le (𝓝(x)).map f$$$

Lean4

theorem isOpenMap_iff_nhds_le : IsOpenMap f ↔ ∀ x : X, 𝓝 (f x) ≤ (𝓝 x).map f :=
  ⟨fun hf => hf.nhds_le, IsOpenMap.of_nhds_le⟩

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