instCountablePProd

Mathlib.Data.Countable.Basic

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

English

If α and β are countable, then the PProd α β is countable.

Русский

Если α и β счётны, то PProd α β счётен.

LaTeX

$$$ \operatorname{Countable}(\alpha) \land \operatorname{Countable}(\beta) \Rightarrow \operatorname{Countable}(\mathrm{PProd}\ \alpha \ \beta) $$$

Lean4

instance [Countable α] [Countable β] : Countable (PProd α β) :=
  Countable.of_equiv (PLift α × PLift β) (Equiv.plift.prodPProd Equiv.plift)

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

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

Разделы

Аффилиация

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