isEmpty_ulift

Mathlib.Logic.IsEmpty

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

English

IsEmpty (ULift α) is equivalent to IsEmpty α.

Русский

IsEmpty (ULift α) эквивалентно IsEmpty α.

LaTeX

$$IsEmpty(\\ULift\\alpha) \\leftrightarrow \\IsEmpty(\\alpha)$$

Lean4

@[simp]
theorem isEmpty_ulift {α} : IsEmpty (ULift α) ↔ IsEmpty α := by simp only [← not_nonempty_iff, nonempty_ulift]

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

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

Разделы

Аффилиация

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