lift_le_lift

Mathlib.Order.Booleanisation

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

English

For GeneralizedBooleanAlgebra α, lift a ≤ lift b iff a ≤ b.

Русский

Пусть α — обобщённая булева алгебра, тогда lift a ≤ lift b тогда и только тогда, когда a ≤ b.

LaTeX

$$$\\text{lift } a \\le\\text{ lift } b \\iff a \\le b$$$

Lean4

@[simp]
theorem lift_le_lift : lift a ≤ lift b ↔ a ≤ b :=
  ⟨by rintro ⟨_⟩; assumption, LE.lift⟩

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

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

Разделы

Аффилиация

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