exists_iff

Mathlib.Logic.Unique

URI: https://scilib.ai/kg/mathlib#Unique.exists_iff

English

If α has a unique element a0, then there exists a with p(a) iff p(a0).

Русский

Пусть α — тип с единственным элементом a0. Тогда существует a: α, такой что p(a) ⇔ p(a0).

LaTeX

$$$(\exists a:\alpha, p(a)) \iff p(a_0)$$$

Lean4

theorem exists_iff {p : α → Prop} : Exists p ↔ p default :=
  ⟨fun ⟨a, ha⟩ ↦ eq_default a ▸ ha, Exists.intro default⟩

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

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

Разделы

Аффилиация

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