not_comp_lt_lift

Mathlib.Order.Booleanisation

URI: https://scilib.ai/kg/mathlib#Booleanisation.not_comp_lt_lift

English

For all a,b in a generalized Boolean algebra, comp(a) is not less than lift(b).

Русский

Для любых a,b в обобщённой булевой алгебре comp(a) не меньше lift(b) с точки зрения строгого порядка.

LaTeX

$$¬(comp\ a < lift\ b)$$

Lean4

@[simp]
theorem not_comp_lt_lift : ¬comp a < lift b := fun h ↦ nomatch h

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

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

Разделы

Аффилиация

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