English
The difference distributes over a join: y \ (x ⊔ z) = (y \ x) ⊓ (y \ z).
Русский
Разность распределяется по объединению: y \ (x ⊔ z) = (y \ x) ⊓ (y \ z).
LaTeX
$$$y \setminus (x \cup z) = (y \setminus x) \wedge (y \setminus z)$$$
Lean4
theorem sdiff_sup : y \ (x ⊔ z) = y \ x ⊓ y \ z :=
sdiff_unique
(calc
y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) := by
rw [sup_inf_left, inf_sup_left y]
_ = (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) := by ac_rfl
_ = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) := by rw [sup_inf_sdiff, sup_inf_sdiff]
_ = (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) := by ac_rfl
_ = y := by rw [sup_inf_self, sup_inf_self, inf_idem])
(calc
y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) := by
rw [inf_sup_left, inf_sup_right]
_ = y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) := by ac_rfl
_ = ⊥ := by rw [inf_inf_sdiff, bot_inf_eq, bot_sup_eq, inf_comm (y \ z), inf_inf_sdiff, inf_bot_eq])
