le_inf_sup

Mathlib.Order.Lattice

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

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_inf_sup : a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c) :=
  sup_le (inf_le_inf_left _ le_sup_left) (inf_le_inf_left _ le_sup_right)

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

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

Разделы

Аффилиация

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