hasDistribNeg — Mathlib

English

For sets s,t,u in a distributive algebra, s * (t + u) is contained in s * t ∪ s * u.

Русский

Для множеств s,t,u в распределенной алгебре произведение s с суммой (t + u) подмножество от произведения s с t и s с u.

LaTeX

$$$s * (t + u) \subseteq s * t + s * u$$$

Lean4

/-- `Set α` has distributive negation if `α` has. -/
protected noncomputable def hasDistribNeg [Mul α] [HasDistribNeg α] : HasDistribNeg (Set α)
    where
  __ := Set.involutiveNeg
  neg_mul _ _ := by simp_rw [← image_neg_eq_neg]; exact image2_image_left_comm neg_mul
  mul_neg _ _ := by simp_rw [← image_neg_eq_neg]; exact image_image2_right_comm mul_neg

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