isOpenMap — Mathlib

English

An inducing map with an open range is an open map.

Русский

Воспроизводящее отображение с открытым образом области является открытым отображением.

LaTeX

$$$IsInducing(f) \\land IsOpen(\\mathrm{range}(f)) \\rightarrow IsOpenMap f$$$

Lean4

/-- An inducing map with an open range is an open map. -/
protected theorem isOpenMap (hi : IsInducing f) (ho : IsOpen (range f)) : IsOpenMap f :=
  IsOpenMap.of_nhds_le fun _ => (hi.map_nhds_of_mem _ <| IsOpen.mem_nhds ho <| mem_range_self _).ge

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