continuous_sum_swap

Mathlib.Topology.Constructions.SumProd

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

English

The swapping map on X ⊕ Y is continuous.

Русский

Перемещающее отображение Sum.swap непрерывно.

LaTeX

$$$\\\\operatorname{Continuous}(\\\\mathrm{Sum.swap})$$$

Lean4

@[fun_prop, continuity]
theorem continuous_sum_swap : Continuous (@Sum.swap X Y) :=
  Continuous.sumElim continuous_inr continuous_inl

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

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

Разделы

Аффилиация

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