instCountableULift

Mathlib.Data.Countable.Defs

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

English

If β is countable, then ULift β is countable.

Русский

Если β счётно, то ULift β счётно.

LaTeX

$$$\forall \beta\,(\operatorname{Countable}(\beta)\rightarrow \operatorname{Countable}(\mathrm{ULift}(\beta)))$$$

Lean4

instance {β : Type v} [Countable β] : Countable (ULift.{u} β) :=
  Countable.of_equiv _ Equiv.ulift.symm

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

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

Разделы

Аффилиация

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