English
In a generalized boolean algebra, x \ (y \ z) decomposes as (x \ y) ⊔ (x ⊓ y ⊓ z).
Русский
В обобщённой булевой алгебре разложение x \ (y \ z) равно (x \ y) ⊔ (x ⊓ y ⊓ z).
LaTeX
$$$$ x \setminus (y \setminus z) = (x \setminus y) \vee (x \wedge y \wedge z) $$$$
Lean4
theorem sdiff_sdiff_right : x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z :=
by
rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
apply sdiff_unique
·
calc
x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by rw [sup_inf_right]
_ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
_ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self', inf_sup_right, sup_comm y,
inf_sdiff_sup_right, inf_sup_left x z y]
_ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
_ = x := by rw [sup_inf_sdiff, sup_comm (x ⊓ z), sup_inf_self, sup_comm, inf_sup_self]
·
calc
x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
_ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
_ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
_ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
_ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
_ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
