instUncountablePLift

Mathlib.Data.Countable.Defs

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

English

If α is uncountable, then PLift α is uncountable.

Русский

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

LaTeX

$$$Uncountable(PLift(\\alpha))$$$

Lean4

instance [Uncountable α] : Uncountable (PLift α) :=
  .of_equiv _ Equiv.plift.symm

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

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

Разделы

Аффилиация

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