sdiff_inf_distrib — Mathlib

English

In a generalized coheyting algebra, a \ (b ⊓ c) distributes as a \ b ⊔ a \ c.

Русский

В обобщённой ко-гейтинговой алгебре разность относительно пересечения распадается как a \ b ⊔ a \ c.

LaTeX

$$$\forall a,b,c:\alpha,\; a \ (b \wedge c) = (a \ b) \ ⊔ (a \ c)$$$

Lean4

theorem sdiff_inf_distrib (a b c : α) : a \ (b ⊓ c) = a \ b ⊔ a \ c :=
  eq_of_forall_ge_iff fun d => by
    rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
    simp_rw [sdiff_le_comm]

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