isEmpty_plift

Mathlib.Logic.IsEmpty

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

English

IsEmpty (PLift α) is equivalent to IsEmpty α.

Русский

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

LaTeX

$$IsEmpty(\\PLift\\alpha) \\leftrightarrow \\IsEmpty(\\alpha)$$

Lean4

@[simp]
theorem isEmpty_plift {α} : IsEmpty (PLift α) ↔ IsEmpty α := by simp only [← not_nonempty_iff, nonempty_plift]

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

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

Разделы

Аффилиация

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