prod

Mathlib.Logic.Denumerable

URI: https://scilib.ai/kg/mathlib#Denumerable.prod

English

If α and β are denumerable, then their product α × β is denumerable.

Русский

Если α и β денумерируемы, то их произведение α × β денумерируемо.

LaTeX

$$$ \text{Denumerable}(\alpha \times \beta) $$$

Lean4

/-- If `α` and `β` are denumerable, then so is their product. -/
instance prod : Denumerable (α × β) :=
  ofEquiv _ (Equiv.sigmaEquivProd α β).symm

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

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

Разделы

Аффилиация

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