isClosed_range_sigmaMk

Mathlib.Topology.Constructions

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

English

The range of Sigma.mk i is closed.

Русский

Образ Sigma.mk i замкнут.

LaTeX

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

Lean4

theorem isClosed_range_sigmaMk {i : ι} : IsClosed (range (@Sigma.mk ι σ i)) :=
  isClosedMap_sigmaMk.isClosed_range

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

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

Разделы

Аффилиация

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