lt_compl_self

Mathlib.Order.Heyting.Basic

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

English

In a nontrivial Heyting algebra, a < aᶜ iff a = ⊥.

Русский

В ненулевой Хейтинговой алгебре a < aᶜ тогда и только тогда, когда a = ⊥.

LaTeX

$$$a < a^{\complement} \iff a = \bot$$$

Lean4

@[simp]
theorem lt_compl_self [Nontrivial α] : a < aᶜ ↔ a = ⊥ := by rw [lt_iff_le_and_ne]; simp

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

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

Разделы

Аффилиация

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