instIsSimpleOrderProp

Mathlib.Order.Atoms

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

English

The truth-values Prop form a simple order: every element is either bottom (false) or top (true).

Русский

Значения истиности в Prop образуют простую порядку: каждое значение либо равно ⊥ (ложь), либо равно ⊤ (истина).

LaTeX

$$$ \\text{IsSimpleOrder}(\\text{Prop}) $$$

Lean4

instance : IsSimpleOrder Prop where eq_bot_or_eq_top p := by simp [em']

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

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

Разделы

Аффилиация

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