prop_iff

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#IsEmpty.prop_iff

English

For any p : Prop, IsEmpty p ⇔ ¬p.

Русский

Для любого p : Prop, IsEmpty p ⇔ ¬p.

LaTeX

$$$IsEmpty(p) \\leftrightarrow \\neg p$$$

Lean4

protected theorem prop_iff {p : Prop} : IsEmpty p ↔ ¬p :=
  isEmpty_iff

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

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

Разделы

Аффилиация

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