# 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

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

`Set α` has distributive negation if `α` has.

Equations

- Set.hasDistribNeg = { toInvolutiveNeg := Set.involutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

Instances For

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

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