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

theorem Set.smul_set_pi₀ {M : Type u_3} {ι : Type u_4} {α : ι → Type u_5} [GroupWithZero M] [(i : ι) → MulAction M (α i)] {c : M} (hc : c ≠ 0) (I : Set ι) (s : (i : ι) → Set (α i)) : c • I.pi s = I.pi (c • s)

theorem Set.smul_set_pi₀' {M : Type u_3} {ι : Type u_4} {α : ι → Type u_5} [GroupWithZero M] [(i : ι) → MulAction M (α i)] {c : M} {I : Set ι} (h : c ≠ 0 ∨ I = univ) (s : (i : ι) → Set (α i)) : c • I.pi s = I.pi (c • s)

A slightly more general version of Set.smul_set_pi₀.

def Set.smulZeroClassSet {α : Type u_1} {β : Type u_2} [Zero β] [SMulZeroClass α β] : SMulZeroClass α (Set β)

If scalar multiplication by elements of α sends (0 : β) to zero, then the same is true for (0 : Set β).

Equations

• Set.smulZeroClassSet = { toSMul := Set.smulSet, smul_zero := ⋯ }

theorem Set.smul_zero_subset {α : Type u_1} {β : Type u_2} [Zero β] [SMulZeroClass α β] (s : Set α) : s • 0 ⊆ 0

theorem Set.Nonempty.smul_zero {α : Type u_1} {β : Type u_2} [Zero β] [SMulZeroClass α β] {s : Set α} (hs : s.Nonempty) : s • 0 = 0

theorem Set.zero_mem_smul_set {α : Type u_1} {β : Type u_2} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} (h : 0 ∈ t) : 0 ∈ a • t

theorem Set.zero_mem_smul_set_iff {α : Type u_1} {β : Type u_2} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} [Zero α] [NoZeroSMulDivisors α β] (ha : a ≠ 0) : 0 ∈ a • t ↔ 0 ∈ t

Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β) because 0 * ∅ ≠ 0.

theorem Set.zero_smul_subset {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] (t : Set β) : 0 • t ⊆ 0

theorem Set.Nonempty.zero_smul {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] {t : Set β} (ht : t.Nonempty) : 0 • t = 0

@[simp]

theorem Set.zero_smul_set {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] {s : Set β} (h : s.Nonempty) : 0 • s = 0

A nonempty set is scaled by zero to the singleton set containing 0.

theorem Set.zero_smul_set_subset {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] (s : Set β) : 0 • s ⊆ 0

theorem Set.subsingleton_zero_smul_set {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] (s : Set β) : (0 • s).Subsingleton

theorem Set.zero_mem_smul_iff {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] {s : Set α} {t : Set β} [NoZeroSMulDivisors α β] : 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

noncomputable def Set.distribSMulSet {α : Type u_1} {β : Type u_2} [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Set β)

If the scalar multiplication (· • ·) : α → β → β is distributive, then so is (· • ·) : α → Set β → Set β.

Equations

• Set.distribSMulSet = { toSMulZeroClass := Set.smulZeroClassSet, smul_add := ⋯ }

noncomputable def Set.distribMulActionSet {α : Type u_1} {β : Type u_2} [Monoid α] [AddMonoid β] [DistribMulAction α β] : DistribMulAction α (Set β)

A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Set β.

Equations

• Set.distribMulActionSet = { toMulAction := Set.mulActionSet, smul_zero := ⋯, smul_add := ⋯ }

noncomputable def Set.mulDistribMulActionSet {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [MulDistribMulAction α β] : MulDistribMulAction α (Set β)

A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

Equations

• Set.mulDistribMulActionSet = { toMulAction := Set.mulActionSet, smul_mul := ⋯, smul_one := ⋯ }

instance Set.instNoZeroSMulDivisors {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Set α) (Set β)

instance Set.noZeroSMulDivisors_set {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Set β)

instance Set.instNoZeroDivisors {α : Type u_1} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α)

@[simp]

theorem Set.smul_mem_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : a • x ∈ a • A ↔ x ∈ A

theorem Set.mem_smul_set_iff_inv_smul_mem₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem Set.mem_inv_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem Set.preimage_smul₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (t : Set β) : (fun (x : β) => a • x) ⁻¹' t = a⁻¹ • t

theorem Set.preimage_smul_inv₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (t : Set β) : (fun (x : β) => a⁻¹ • x) ⁻¹' t = a • t

@[simp]

theorem Set.smul_set_subset_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A B : Set β} : a • A ⊆ a • B ↔ A ⊆ B

theorem Set.smul_set_subset_iff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A B : Set β} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem Set.subset_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A B : Set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem Set.smul_set_inter₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {s t : Set β} {a : α} (ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t

theorem Set.smul_set_sdiff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {s t : Set β} {a : α} (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t

theorem Set.smul_set_symmDiff₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {s t : Set β} {a : α} (ha : a ≠ 0) : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem Set.smul_set_univ₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : a • univ = univ

theorem Set.smul_univ₀ {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : ¬s ⊆ 0) : s • univ = univ

theorem Set.smul_univ₀' {α : Type u_1} {β : Type u_2} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : s.Nontrivial) : s • univ = univ

@[simp]

theorem Set.inv_smul_set_distrib₀ {α : Type u_1} [GroupWithZero α] (a : α) (s : Set α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

theorem Set.inv_op_smul_set_distrib₀ {α : Type u_1} [GroupWithZero α] (a : α) (s : Set α) : (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹