isEmpty_Prop

Mathlib.Logic.IsEmpty

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

English

A proposition p is empty iff it is false.

Русский

Высказывание p пусто тогда и только тогда, когда оно ложно.

LaTeX

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

Lean4

@[simp]
theorem isEmpty_Prop {p : Prop} : IsEmpty p ↔ ¬p := by simp only [← not_nonempty_iff, nonempty_prop]

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

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

Разделы

Аффилиация

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