isOpen_range_coe

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.isOpen_range_coe

English

The range of the inclusion i: X → OnePoint X is an open subset of OnePoint X.

Русский

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

LaTeX

$$$\\mathrm{IsOpen}(\\mathrm{range}((\\uparrow): X \\to \\mathrm{OnePoint} X)).$$$

Lean4

theorem isOpen_range_coe : IsOpen (range ((↑) : X → OnePoint X)) :=
  isOpenEmbedding_coe.isOpen_range

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru