isClosedMap_swap

Mathlib.Topology.Constructions.SumProd

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

← MathLib Explorer

English

The swap map on X × Y is continuous.

Русский

Переключение координат на X × Y непрерывно.

LaTeX

$$Continuous (Prod.swap : X × Y → Y × X)$$

Lean4

theorem isClosedMap_swap : IsClosedMap (Prod.swap : X × Y → Y × X) := fun s hs ↦
  by
  rw [image_swap_eq_preimage_swap]
  exact hs.preimage continuous_swap

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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