existsUnique_false

Mathlib.Logic.ExistsUnique

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

English

There is no unique x with False on any type α.

Русский

Не существует единственного элемента x такого, что False на любом множества α.

LaTeX

$$$$ \\\\neg \\\\exists! x:\\\\alpha, False $$$$

Lean4

@[simp]
theorem existsUnique_false : ¬∃! _ : α, False := fun ⟨_, h, _⟩ ↦ h

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

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

Разделы

Аффилиация

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