sup_inf_inf_sdiff — Mathlib

English

For elements x, y, z in a generalized boolean algebra, (x ⊓ y ⊓ z) ⊔ (y \ z) = (x ⊓ y) ⊔ (y \ z).

Русский

Для элементов x, y, z обобщённой булевой алгебры выполняется (x ⊓ y ⊓ z) ⊔ (y \ z) = (x ⊓ y) ⊔ (y \ z).

LaTeX

$$$$ (x \wedge y \wedge z) \vee (y \setminus z) = (x \wedge y) \vee (y \setminus z) $$$$

Lean4

theorem sup_inf_inf_sdiff : x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z := by
  rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]

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