Pointwise operations of sets in a ring

This file proves properties of pointwise operations of sets in a ring.

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

noncomputable def Set.hasDistribNeg {α : Type u_2} [Mul α] [HasDistribNeg α] : HasDistribNeg (Set α)

Set α has distributive negation if α has.

Equations

• Set.hasDistribNeg = HasDistribNeg.mk ⋯ ⋯

Note that Set α is not a Distrib because s * t + s * u has cross terms that s * (t + u) lacks.

theorem Set.mul_add_subset {α : Type u_2} [Distrib α] (s : Set α) (t : Set α) (u : Set α) : s * (t + u) ⊆ s * t + s * u

theorem Set.add_mul_subset {α : Type u_2} [Distrib α] (s : Set α) (t : Set α) (u : Set α) : (s + t) * u ⊆ s * u + t * u