isEmpty_iff

Mathlib.Logic.IsEmpty

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

English

For any α, IsEmpty α is equivalent to α → False.

Русский

Для любого типа α равносильно: IsEmpty α ⇔ α → False.

LaTeX

$$$IsEmpty(\\alpha) \\leftrightarrow (\\alpha \\rightarrow \\mathrm{False})$$$

Lean4

theorem isEmpty_iff : IsEmpty α ↔ α → False :=
  ⟨@IsEmpty.false α, IsEmpty.mk⟩

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

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

Разделы

Аффилиация

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