of_nhds_le — Mathlib

English

If a function f satisfies nhds(f x) ≤ map f (nhds x) for all x, then f is an open map.

Русский

Если для всех x выполняется nhds(f(x)) ≤ map f (nhds(x)), то f является открытым отображением.

LaTeX

$$$$\\big( \\forall x, \\ nhds(f(x)) \\le map(f)(nhds(x)) \\big) \\rightarrow IsOpenMap(f)$$$$

Lean4

theorem of_nhds_le (hf : ∀ x, 𝓝 (f x) ≤ map f (𝓝 x)) : IsOpenMap f := fun _s hs =>
  isOpen_iff_mem_nhds.2 fun _y ⟨_x, hxs, hxy⟩ => hxy ▸ hf _ (image_mem_map <| hs.mem_nhds hxs)

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