sup_eq_sdiff_sup_sdiff_sup_inf — 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 sup_eq_sdiff_sup_sdiff_sup_inf : x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y :=
  Eq.symm <|
    calc
      x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) := by rw [sup_inf_left]
      _ = (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) := by ac_rfl
      _ = x ⊔ y := by simp

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