English
The distributive law: (x ⊓ y) \ z = (x \ z) ⊓ (y \ z).
Русский
Дистрибутивность: (x ⊓ y) \ z = (x \ z) ⊓ (y \ z).
LaTeX
$$$$ (x \land y) \setminus z = (x \setminus z) \land (y \setminus z) $$$$
Lean4
theorem inf_sdiff : (x ⊓ y) \ z = x \ z ⊓ y \ z :=
sdiff_unique
(calc
_ = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) := by
rw [sup_inf_left, sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]
_ = (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) := by ac_rfl
_ = x ⊓ y ⊔ x \ z ⊓ y \ z := by rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]
_ = x ⊓ y := sup_eq_left.2 (inf_le_inf sdiff_le sdiff_le))
(calc
x ⊓ y ⊓ z ⊓ (x \ z ⊓ y \ z) = x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z := by ac_rfl
_ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq])
