compl_lt_self

Mathlib.Order.BooleanAlgebra.Basic

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

English

Let A be a nontrivial Boolean algebra. Then x^c < x iff x = ⊤.

Русский

Пусть A не тривиальна. Тогда x^c < x тогда и только тогда, когда x = ⊤.

LaTeX

$$$x^{c} < x \iff x = \top$$$

Lean4

@[simp]
theorem compl_lt_self [Nontrivial α] : xᶜ < x ↔ x = ⊤ := by simpa using lt_compl_self (a := xᶜ)

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

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

Разделы

Аффилиация

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