isCoatom_iff

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#Prop.isCoatom_iff

English

An element p of Prop is a coatom if and only if p is false (not true).

Русский

Элемент p в Prop является коатомом тогда и только тогда, когда p ложно.

LaTeX

$$$ \\text{IsCoatom}(p) \\iff \\neg p $$$

Lean4

theorem isCoatom_iff {p : Prop} : IsCoatom p ↔ ¬p := by simp

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

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

Разделы

Аффилиация

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