existsUnique_prop

Mathlib.Logic.ExistsUnique

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

English

For any Prop p and q, (∃! _ : p, q) is equivalent to p ∧ q.

Русский

Для любых предикатов p и q, (существует уникальный x: p, q) эквивалентно p ∧ q.

LaTeX

$$$$ (\\\\exists! x, q) \\Leftrightarrow p \\\\land q $$$$

Lean4

theorem existsUnique_prop {p q : Prop} : (∃! _ : p, q) ↔ p ∧ q := by simp

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

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

Разделы

Аффилиация

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