instCountablePSum

Mathlib.Data.Countable.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

instance [Countable α] [Countable β] : Countable (α ⊕' β) :=
  Countable.of_equiv (PLift α ⊕ PLift β) (Equiv.plift.sumPSum Equiv.plift)

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

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

Разделы

Аффилиация

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