English
In a generalized boolean algebra, the two pieces x ∧ y and y ∖ x are disjoint; i.e., (x ∧ y) ∧ (y ∖ x) = ⊥.
Русский
В обобщённой булевой алгебре части x ∧ y и y ∖ x не пересекаются; то есть (x ∧ y) ∧ (y ∖ x) = ⊥.
LaTeX
$$$(x \wedge y) \wedge (y \setminus x) = \bot$$$
Lean4
@[simp]
theorem sdiff_inf_sdiff : x \ y ⊓ y \ x = ⊥ :=
Eq.symm <|
calc
⊥ = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y := by rw [← inf_inf_sdiff, sup_inf_sdiff]
_ = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y := by rw [inf_sup_left]
_ = (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y := by ac_rfl
_ = x ⊓ y \ x ⊓ x \ y := by rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
_ = x ⊓ x \ y ⊓ y \ x := by ac_rfl
_ = x \ y ⊓ y \ x := by rw [inf_of_le_right sdiff_le']
