existsUnique_const — Mathlib

English

If α is nonempty and subsingleton, then (∃! _ : α, b) is equivalent to b.

Русский

Если α непусто и является одиночной, то (существует уникальный элемент α, удовлетворяющий b) эквивалентно b.

LaTeX

$$$$ (\\\\exists! x:\\\\alpha, b) \\\\Leftrightarrow b $$$$

Lean4

theorem existsUnique_const {b : Prop} (α : Sort*) [i : Nonempty α] [Subsingleton α] : (∃! _ : α, b) ↔ b := by simp

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