instNonempty_mathlib

Mathlib.Data.ULift

URI: https://scilib.ai/kg/mathlib#ULift.instNonempty_mathlib

English

If α is Nonempty, then ULift α is Nonempty.

Русский

Если α непусто, то ULift α непусто.

LaTeX

$$$\\forall {\\alpha : \\mathrm{Type} \\;v}, \\operatorname{Nonempty}(\\alpha) \\Rightarrow \\operatorname{Nonempty}(\\mathrm{ULift}(\\alpha))$$$

Lean4

instance [Nonempty α] : Nonempty (ULift α) :=
  Equiv.ulift.nonempty

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

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

Разделы

Аффилиация

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