sup_inf_le — Mathlib

English

In a lattice, the join of a with the meet of b and c is below the meet of the joins: a ∨ (b ∧ c) ≤ (a ∨ b) ∧ (a ∨ c).

Русский

В решётке объединение с пересечением даёт не больше пересечения двух объединений: a ∨ (b ∧ c) ≤ (a ∨ b) ∧ (a ∨ c).

LaTeX

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

Lean4

theorem sup_inf_le : a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c) :=
  le_inf (sup_le_sup_left inf_le_left _) (sup_le_sup_left inf_le_right _)

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