isOpenMap_coe — Mathlib

English

The inclusion i: X → OnePoint X is an open map, i.e., it sends open sets of X to open sets of OnePoint X.

Русский

Вложение i: X → OnePoint X является открытым отображением: открытые множества X переходят в открытые множества в OnePoint X.

LaTeX

$$$\\text{IsOpenMap}((\\uparrow): X \\to \\mathrm{OnePoint} X).$$$

Lean4

theorem isOpenMap_coe : IsOpenMap ((↑) : X → OnePoint X) := fun _ => isOpen_image_coe.2

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