sup_mul_distrib — Mathlib

English

In a quantale, right multiplication distributes over binary sup: for all x, y, z, (x ⊔ y) * z = (x * z) ⊔ (y * z).

Русский

Вклаторе (кватале) правое умножение распределено над бинарной сводкой: для любых x, y, z верно (x ⊔ y) · z = (x · z) ⊔ (y · z).

LaTeX

$$$$ (x \lor y) \cdot z = (x \cdot z) \lor (y \cdot z) $$$$

Lean4

@[to_additive]
theorem sup_mul_distrib : (x ⊔ y) * z = (x * z) ⊔ (y * z) := by
  rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]

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