exists_true_iff_nonempty

Mathlib.Logic.Nonempty

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

English

For any type α, (exists x : α, True) is equivalent to Nonempty α.

Русский

Пусть α — тип. Существует x : α с True эквивалентно Nonempty α.

LaTeX

$$$ (\exists x : \alpha, \mathrm{True}) \iff \mathrm{Nonempty}(\alpha) $$$

Lean4

theorem exists_true_iff_nonempty {α : Sort*} : (∃ _ : α, True) ↔ Nonempty α :=
  Iff.intro (fun ⟨a, _⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨a, trivial⟩

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

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

Разделы

Аффилиация

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