inf_sup_assoc_of_le — Mathlib

English

In a modular lattice, if x ≤ z then (x ⊓ z) ⊔ y equals x ⊓ (z ⊔ y) under appropriate conditions.

Русский

В модульной решётке при x ≤ z выполняется (x ⊓ z) ⊔ y = x ⊓ (z ⊔ y) при соответствующих условиях.

LaTeX

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

Lean4

theorem inf_sup_assoc_of_le {x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ y ⊔ z = x ⊓ (y ⊔ z) := by
  rw [inf_comm, sup_comm, ← sup_inf_assoc_of_le y h, inf_comm, sup_comm]

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