countable_prod_swap

Mathlib.Data.Countable.Basic

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

English

If α × β is countable, then β × α is countable.

Русский

Если α × β счётно, то β × α счётно.

LaTeX

$$$ \operatorname{Countable}(\alpha \times \beta) \rightarrow \operatorname{Countable}(\beta \times \alpha) $$$

Lean4

theorem countable_prod_swap [Countable (α × β)] : Countable (β × α) :=
  Countable.of_equiv _ (Equiv.prodComm α β)

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

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

Разделы

Аффилиация

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