not_comp_le_lift

Mathlib.Order.Booleanisation

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

English

It is not the case that comp a ≤ lift b (in a GeneralizedBooleanAlgebra).

Русский

Не выполняется comp a ≤ lift b.

LaTeX

$$¬(\\operatorname{comp} a ≤ \\operatorname{lift} b)$$

Lean4

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

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

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

Разделы

Аффилиация

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