instCountablePLift

Mathlib.Data.Countable.Defs

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

English

If α is countable, then PLift α is countable.

Русский

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

LaTeX

$$$\text{Countable}(\mathrm{PLift}\;\alpha)$ whenever $\text{Countable}(\alpha)$.$$

Lean4

instance [Countable α] : Countable (PLift α) :=
  Equiv.plift.injective.countable

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

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

Разделы

Аффилиация

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