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_1} [MulZeroClass α] (s : Set α) : s * 0 ⊆ 0

theorem Set.zero_mul_subset {α : Type u_1} [MulZeroClass α] (s : Set α) : 0 * s ⊆ 0

theorem Set.Nonempty.mul_zero {α : Type u_1} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) : s * 0 = 0

theorem Set.Nonempty.zero_mul {α : Type u_1} [MulZeroClass α] {s : Set α} (hs : s.Nonempty) : 0 * s = 0

theorem Set.div_zero_subset {α : Type u_1} [GroupWithZero α] (s : Set α) : s / 0 ⊆ 0

theorem Set.zero_div_subset {α : Type u_1} [GroupWithZero α] (s : Set α) : 0 / s ⊆ 0

theorem Set.Nonempty.div_zero {α : Type u_1} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) : s / 0 = 0

theorem Set.Nonempty.zero_div {α : Type u_1} [GroupWithZero α] {s : Set α} (hs : s.Nonempty) : 0 / s = 0

@[simp]

theorem Set.inv_zero {α : Type u_1} [GroupWithZero α] : 0⁻¹ = 0