isOpen_range_sigmaMk

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#isOpen_range_sigmaMk

English

The range of Sigma.mk i is open.

Русский

Образ Sigma.mk i открыт.

LaTeX

$$$\\text{IsOpen}(\\operatorname{range}(\\Sigma.mk\\ i))$$$

Lean4

theorem isOpen_range_sigmaMk {i : ι} : IsOpen (range (@Sigma.mk ι σ i)) :=
  isOpenMap_sigmaMk.isOpen_range

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

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

Разделы

Аффилиация

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