not_nonempty_iff_imp_false — Mathlib

English

For any type α, α is empty iff there is no element of α; equivalently, there exists a function from α to False.

Русский

Для произвольного типа α пустое тогда, когда не существует элемента α; эквивалентно существованию функции α → False.

LaTeX

$$$\neg \mathrm{Nonempty}(\alpha) \iff \alpha \to \mathrm{False}$$$

Lean4

theorem not_nonempty_iff_imp_false {α : Sort*} : ¬Nonempty α ↔ α → False :=
  Nonempty.imp

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