ofBoolAlg_symmDiff — Mathlib

English

For a ≤ b in AsBoolAlg α, the product equals the left factor: ofBoolAlg(a)·ofBoolAlg(b) = ofBoolAlg(a) implies a ≤ b.

Русский

Если a ≤ b в AsBoolAlg α, то произведение равно левому множителю: ofBoolAlg(a)·ofBoolAlg(b) = ofBoolAlg(a) ≡ a ≤ b.

LaTeX

$$$\mathrm{ofBoolAlg}(a) \cdot \mathrm{ofBoolAlg}(b) = \mathrm{ofBoolAlg}(a) \iff a \le b$$$

Lean4

@[simp]
theorem ofBoolAlg_symmDiff (a b : AsBoolAlg α) : ofBoolAlg (a ∆ b) = ofBoolAlg a + ofBoolAlg b :=
  by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact of_boolalg_symmDiff_aux _ _

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