le_sup_inf

Mathlib.Order.Lattice

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

English

In a lattice, a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c).

Русский

В решётке выполняется неравенство a ∧ b ∨ a ∧ c ≤ a ∧ (b ∨ c).

LaTeX

$$$ a \wedge b \vee a \wedge c \le a \wedge (b \vee c)$$$

Lean4

theorem le_sup_inf : ∀ {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z := fun {x y z} => DistribLattice.le_sup_inf x y z

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

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

Разделы

Аффилиация

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