sup_inf_assoc_of_le — Mathlib

English

In a modular lattice, for x ≤ z, (x ∨ y) ∧ z = x ∨ (y ∧ z).

Русский

В модульной решётке, при x ≤ z выполняется (x ∨ y) ∧ z = x ∨ (y ∧ z).

LaTeX

$$$ x \\le z \\Rightarrow (x \\lor y) \\land z = x \\lor (y \\land z) $$$

Lean4

theorem sup_inf_assoc_of_le {x : α} (y : α) {z : α} (h : x ≤ z) : (x ⊔ y) ⊓ z = x ⊔ y ⊓ z :=
  le_antisymm (IsModularLattice.sup_inf_le_assoc_of_le y h)
    (le_inf (sup_le_sup_left inf_le_left _) (sup_le h inf_le_right))

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