nonempty_ulift

Mathlib.Logic.Nonempty

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

English

Nonempty of ULift α is equivalent to Nonempty α.

Русский

Непусто ULift α эквивалентно непусто α.

LaTeX

$$$\operatorname{Nonempty}(\mathrm{ULift}\,\alpha) \iff \operatorname{Nonempty} \alpha$$$

Lean4

@[simp]
theorem nonempty_ulift : Nonempty (ULift α) ↔ Nonempty α :=
  Iff.intro (fun ⟨⟨a⟩⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨⟨a⟩⟩

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

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

Разделы

Аффилиация

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