continuous_sigmaMk

Mathlib.Topology.Constructions

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

English

For any index i, the canonical injection Sigma.mk i : σ_i → Sigma σ is continuous.

Русский

Для любого индекса i каноническое вложение Sigma.mk i: σ_i → Sigma σ непрерывно.

LaTeX

$$$\\text{Continuous}(\\Sigma.mk\\ i):\\; \\sigma(i) \\to \\Sigma\\sigma$$$

Lean4

@[continuity, fun_prop]
theorem continuous_sigmaMk {i : ι} : Continuous (@Sigma.mk ι σ i) :=
  continuous_iSup_rng continuous_coinduced_rng

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

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

Разделы

Аффилиация

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