Pointwise operations of sets in a group with zero #

This file proves properties of pointwise operations of sets in a group with zero.

Tags #

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

Note that Set is not a MulZeroClass because 0 * ∅ ≠ 0.

theorem Set.mul_zero_subset {α : Type u_2} [MulZeroClass α] (s : Set α) :

s * 0 ⊆ 0

theorem Set.zero_mul_subset {α : Type u_2} [MulZeroClass α] (s : Set α) :

0 * s ⊆ 0

theorem Set.Nonempty.mul_zero {α : Type u_2} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) :

s * 0 = 0

theorem Set.Nonempty.zero_mul {α : Type u_2} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) :

0 * s = 0

theorem Set.div_zero_subset {α : Type u_2} [GroupWithZero α] (s : Set α) :

s / 0 ⊆ 0

theorem Set.zero_div_subset {α : Type u_2} [GroupWithZero α] (s : Set α) :

0 / s ⊆ 0

theorem Set.Nonempty.div_zero {α : Type u_2} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) :

s / 0 = 0

theorem Set.Nonempty.zero_div {α : Type u_2} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) :

0 / s = 0