sdiff_sdiff_sup_sdiff' — Mathlib

English

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

Русский

Для x и y в булевой алгебре: x ⊔ y = (x \ y) ⊔ (y \ x) ⊔ (x ⊓ y).

LaTeX

$$$$ x \lor y = (x \setminus y) \lor (y \setminus x) \lor (x \land y) $$$$

Lean4

theorem sdiff_sdiff_sup_sdiff' : z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y :=
  calc
    z \ (x \ y ⊔ y \ x) = z \ (x \ y) ⊓ z \ (y \ x) := sdiff_sup
    _ = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by rw [sdiff_sdiff_right, sdiff_sdiff_right]
    _ = (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by ac_rfl
    _ = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x := by rw [← sup_inf_right]
    _ = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y := by ac_rfl

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