Pointwise actions on sets

This file proves that several kinds of actions of a type α on another type β transfer to actions of α/Set α on Set β.

Implementation notes

• We put all instances in the scope Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the scope to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp).

Translation/scaling of sets

theorem Set.smul_set_prod {β : Type u_3} {M : Type u_5} {α : Type u_6} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) : c • s ×ˢ t = (c • s) ×ˢ (c • t)

theorem Set.vadd_set_prod {β : Type u_3} {M : Type u_5} {α : Type u_6} [VAdd M α] [VAdd M β] (c : M) (s : Set α) (t : Set β) : c +ᵥ s ×ˢ t = (c +ᵥ s) ×ˢ (c +ᵥ t)

theorem Set.smul_set_pi {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [Group G] [(i : ι) → MulAction G (α i)] (c : G) (I : Set ι) (s : (i : ι) → Set (α i)) : c • I.pi s = I.pi (c • s)

theorem Set.vadd_set_pi {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [AddGroup G] [(i : ι) → AddAction G (α i)] (c : G) (I : Set ι) (s : (i : ι) → Set (α i)) : c +ᵥ I.pi s = I.pi (c +ᵥ s)

theorem Set.smul_set_pi_of_isUnit {M : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [Monoid M] [(i : ι) → MulAction M (α i)] {c : M} (hc : IsUnit c) (I : Set ι) (s : (i : ι) → Set (α i)) : c • I.pi s = I.pi (c • s)

theorem Set.vadd_set_pi_of_isAddUnit {M : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [AddMonoid M] [(i : ι) → AddAction M (α i)] {c : M} (hc : IsAddUnit c) (I : Set ι) (s : (i : ι) → Set (α i)) : c +ᵥ I.pi s = I.pi (c +ᵥ s)

theorem Set.smul_set_subset_mul {α : Type u_2} [Mul α] {s t : Set α} {a : α} : a ∈ s → a • t ⊆ s * t

theorem Set.vadd_set_subset_add {α : Type u_2} [Add α] {s t : Set α} {a : α} : a ∈ s → a +ᵥ t ⊆ s + t

theorem Set.op_smul_set_subset_mul {α : Type u_2} [Mul α] {s t : Set α} {a : α} : a ∈ t → MulOpposite.op a • s ⊆ s * t

theorem Set.op_vadd_set_subset_add {α : Type u_2} [Add α] {s t : Set α} {a : α} : a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t

theorem Set.image_op_smul {α : Type u_2} [Mul α] {s t : Set α} : MulOpposite.op '' s • t = t * s

theorem Set.image_op_vadd {α : Type u_2} [Add α] {s t : Set α} : AddOpposite.op '' s +ᵥ t = t + s

@[simp]

theorem Set.iUnion_op_smul_set {α : Type u_2} [Mul α] (s t : Set α) : ⋃ a ∈ t, MulOpposite.op a • s = s * t

@[simp]

theorem Set.iUnion_op_vadd_set {α : Type u_2} [Add α] (s t : Set α) : ⋃ a ∈ t, AddOpposite.op a +ᵥ s = s + t

theorem Set.mul_subset_iff_left {α : Type u_2} [Mul α] {s t u : Set α} : s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

theorem Set.add_subset_iff_left {α : Type u_2} [Add α] {s t u : Set α} : s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u

theorem Set.mul_subset_iff_right {α : Type u_2} [Mul α] {s t u : Set α} : s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u

theorem Set.add_subset_iff_right {α : Type u_2} [Add α] {s t u : Set α} : s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u

theorem Set.pair_mul {α : Type u_2} [Mul α] (a b : α) (s : Set α) : {a, b} * s = a • s ∪ b • s

theorem Set.pair_add {α : Type u_2} [Add α] (a b : α) (s : Set α) : {a, b} + s = (a +ᵥ s) ∪ (b +ᵥ s)

theorem Set.mul_pair {α : Type u_2} [Mul α] (s : Set α) (a b : α) : s * {a, b} = MulOpposite.op a • s ∪ MulOpposite.op b • s

theorem Set.add_pair {α : Type u_2} [Add α] (s : Set α) (a b : α) : s + {a, b} = (AddOpposite.op a +ᵥ s) ∪ (AddOpposite.op b +ᵥ s)

theorem Set.range_mul {α : Type u_2} [Mul α] {ι : Sort u_6} (a : α) (f : ι → α) : (range fun (i : ι) => a * f i) = a • range f

theorem Set.range_add {α : Type u_2} [Add α] {ι : Sort u_6} (a : α) (f : ι → α) : (range fun (i : ι) => a + f i) = a +ᵥ range f

theorem Set.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (a • s) = f a • ⇑f '' s

theorem Set.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (a +ᵥ s) = f a +ᵥ ⇑f '' s

theorem Set.image_op_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (MulOpposite.op a • s) = MulOpposite.op (f a) • ⇑f '' s

theorem Set.image_op_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (AddOpposite.op a +ᵥ s) = AddOpposite.op (f a) +ᵥ ⇑f '' s

theorem Set.op_smul_set_mul_eq_mul_smul_set {α : Type u_2} [Semigroup α] (a : α) (s t : Set α) : MulOpposite.op a • s * t = s * a • t

theorem Set.op_vadd_set_add_eq_add_vadd_set {α : Type u_2} [AddSemigroup α] (a : α) (s t : Set α) : (AddOpposite.op a +ᵥ s) + t = s + (a +ᵥ t)

theorem Set.pairwiseDisjoint_smul_iff {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s : Set α} {t : Set β} : (s.PairwiseDisjoint fun (x : α) => x • t) ↔ InjOn (fun (p : α × β) => p.1 • p.2) (s ×ˢ t)

theorem Set.pairwiseDisjoint_vadd_iff {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s : Set α} {t : Set β} : (s.PairwiseDisjoint fun (x : α) => x +ᵥ t) ↔ InjOn (fun (p : α × β) => p.1 +ᵥ p.2) (s ×ˢ t)

instance Set.smulCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Set γ)

instance Set.vaddCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Set γ)

instance Set.smulCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Set β) (Set γ)

instance Set.vaddCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Set β) (Set γ)

instance Set.smulCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) β (Set γ)

instance Set.vaddCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Set α) β (Set γ)

instance Set.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) (Set β) (Set γ)

instance Set.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Set α) (Set β) (Set γ)

instance Set.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Set γ)

instance Set.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Set γ)

instance Set.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Set β) (Set γ)

instance Set.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Set β) (Set γ)

instance Set.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Set α) (Set β) (Set γ)

instance Set.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Set α) (Set β) (Set γ)

instance Set.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Set β)

instance Set.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Set β)

@[instance_reducible]

noncomputable def Set.mulAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] : MulAction (Set α) (Set β)

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

@[instance_reducible]

noncomputable def Set.addAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] : AddAction (Set α) (Set β)

An additive action of an additive monoid α on a type β gives an additive action of Set α on Set β

@[instance_reducible]

def Set.mulActionSet {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] : MulAction α (Set β)

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

@[instance_reducible]

def Set.addActionSet {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] : AddAction α (Set β)

An additive action of an additive monoid on a type β gives an additive action on Set β.

theorem IsSMulRegular.set {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} (h : IsSMulRegular β a) : IsSMulRegular (Set β) a

If a is regular on β, it is regular on Set β.

theorem IsSMulRegular.smul_set_subset_smul_set_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s t : Set β} {a : α} (h : IsSMulRegular β a) : a • s ⊆ a • t ↔ s ⊆ t

theorem IsVAddRegular.vadd_set_subset_vadd_set_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s t : Set β} {a : α} (h : IsVAddRegular β a) : a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t

theorem IsSMulRegular.smul_set_inter {α : Type u_2} {β : Type u_3} [SMul α β] {s t : Set β} {a : α} (h : IsSMulRegular β a) : a • (s ∩ t) = a • s ∩ a • t

theorem IsVAddRegular.vadd_set_inter {α : Type u_2} {β : Type u_3} [VAdd α β] {s t : Set β} {a : α} (h : IsVAddRegular β a) : a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

theorem IsSMulRegular.smul_set_sdiff {α : Type u_2} {β : Type u_3} [SMul α β] {s t : Set β} {a : α} (h : IsSMulRegular β a) : a • (s \ t) = a • s \ a • t

theorem IsVAddRegular.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [VAdd α β] {s t : Set β} {a : α} (h : IsVAddRegular β a) : a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)

theorem IsSMulRegular.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [SMul α β] {s t : Set β} {a : α} (h : IsSMulRegular β a) : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem IsVAddRegular.vadd_set_symmDiff {α : Type u_2} {β : Type u_3} [VAdd α β] {s t : Set β} {a : α} (h : IsVAddRegular β a) : a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)

@[simp]

theorem Set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s : Set β} {a : α} {x : β} : a • x ∈ a • s ↔ x ∈ s

@[simp]

theorem Set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s : Set β} {a : α} {x : β} : a +ᵥ x ∈ a +ᵥ s ↔ x ∈ s

@[simp]

theorem Set.smul_set_subset_smul_set_iff {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s t : Set β} {a : α} : a • s ⊆ a • t ↔ s ⊆ t

@[simp]

theorem Set.vadd_set_subset_vadd_set_iff {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s t : Set β} {a : α} : a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t

theorem Set.smul_set_inter {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s t : Set β} {a : α} : a • (s ∩ t) = a • s ∩ a • t

theorem Set.vadd_set_inter {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s t : Set β} {a : α} : a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

theorem Set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s t : Set β} {a : α} : a • (s \ t) = a • s \ a • t

theorem Set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s t : Set β} {a : α} : a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)

theorem Set.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] {s t : Set β} {a : α} : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem Set.vadd_set_symmDiff {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] {s t : Set β} {a : α} : a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)

instance Set.instIsLeftCancelSMul {α : Type u_2} {β : Type u_3} [SMul α β] [IsLeftCancelSMul α β] : IsLeftCancelSMul α (Set β)

instance Set.instIsLeftCancelVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [IsLeftCancelVAdd α β] : IsLeftCancelVAdd α (Set β)

theorem Set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} : x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem Set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} : x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A

theorem Set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} : x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem Set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} : x ∈ -a +ᵥ A ↔ a +ᵥ x ∈ A

@[simp]

theorem Set.mem_smul_set_inv {α : Type u_2} [Group α] {a b : α} {s : Set α} : a ∈ b • s⁻¹ ↔ b ∈ a • s

@[simp]

theorem Set.mem_vadd_set_neg {α : Type u_2} [AddGroup α] {a b : α} {s : Set α} : a ∈ b +ᵥ -s ↔ b ∈ a +ᵥ s

theorem Set.preimage_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) : (fun (x : β) => a • x) ⁻¹' t = a⁻¹ • t

theorem Set.preimage_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) : (fun (x : β) => a +ᵥ x) ⁻¹' t = -a +ᵥ t

theorem Set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) : (fun (x : β) => a⁻¹ • x) ⁻¹' t = a • t

theorem Set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) : (fun (x : β) => -a +ᵥ x) ⁻¹' t = a +ᵥ t

theorem Set.smul_set_subset_iff_subset_inv_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A B : Set β} {a : α} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem Set.vadd_set_subset_iff_subset_neg_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A B : Set β} {a : α} : a +ᵥ A ⊆ B ↔ A ⊆ -a +ᵥ B

theorem Set.subset_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A B : Set β} {a : α} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem Set.subset_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A B : Set β} {a : α} : A ⊆ a +ᵥ B ↔ -a +ᵥ A ⊆ B

theorem Set.smul_set_iInter {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {ι : Sort u_5} (a : α) (t : ι → Set β) : a • ⋂ (i : ι), t i = ⋂ (i : ι), a • t i

theorem Set.vadd_set_iInter {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {ι : Sort u_5} (a : α) (t : ι → Set β) : a +ᵥ ⋂ (i : ι), t i = ⋂ (i : ι), a +ᵥ t i

@[simp]

theorem Set.smul_set_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} : a • univ = univ

@[simp]

theorem Set.vadd_set_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} : a +ᵥ univ = univ

@[simp]

theorem Set.smul_set_eq_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} : a • s = univ ↔ s = univ

@[simp]

theorem Set.vadd_set_eq_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} : a +ᵥ s = univ ↔ s = univ

@[simp]

theorem Set.smul_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set α} (hs : s.Nonempty) : s • univ = univ

@[simp]

theorem Set.vadd_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set α} (hs : s.Nonempty) : s +ᵥ univ = univ

theorem Set.smul_set_compl {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} : a • sᶜ = (a • s)ᶜ

theorem Set.vadd_set_compl {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} : a +ᵥ sᶜ = (a +ᵥ s)ᶜ

theorem Set.smul_inter_nonempty_iff {α : Type u_2} [Group α] {s t : Set α} {x : α} : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

theorem Set.vadd_inter_nonempty_iff {α : Type u_2} [AddGroup α] {s t : Set α} {x : α} : ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a + -b = x

theorem Set.smul_inter_nonempty_iff' {α : Type u_2} [Group α] {s t : Set α} {x : α} : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x

theorem Set.vadd_inter_nonempty_iff' {α : Type u_2} [AddGroup α] {s t : Set α} {x : α} : ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a - b = x

theorem Set.op_smul_inter_nonempty_iff {α : Type u_2} [Group α] {s t : Set α} {x : αᵐᵒᵖ} : (x • s ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x

theorem Set.op_vadd_inter_nonempty_iff {α : Type u_2} [AddGroup α] {s t : Set α} {x : αᵃᵒᵖ} : ((x +ᵥ s) ∩ t).Nonempty ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ -a + b = AddOpposite.unop x

@[simp]

theorem Set.iUnion_inv_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : ⋃ (g : α), g⁻¹ • s = ⋃ (g : α), g • s

@[simp]

theorem Set.iUnion_neg_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : ⋃ (g : α), -g +ᵥ s = ⋃ (g : α), g +ᵥ s

theorem Set.iUnion_smul_eq_ofPred_exists {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : ⋃ (g : α), g • s = {a : β | ∃ (g : α), g • a ∈ s}

theorem Set.iUnion_vadd_eq_ofPred_exists {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : ⋃ (g : α), g +ᵥ s = {a : β | ∃ (g : α), g +ᵥ a ∈ s}

@[deprecated Set.iUnion_smul_eq_ofPred_exists (since := "2026-07-09")]

theorem Set.iUnion_smul_eq_setOf_exists {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : ⋃ (g : α), g • s = {a : β | ∃ (g : α), g • a ∈ s}

Alias of Set.iUnion_smul_eq_ofPred_exists.

@[deprecated Set.iUnion_vadd_eq_ofPred_exists (since := "2026-07-09")]

theorem Set.iUnion_vadd_eq_setOf_exists {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : ⋃ (g : α), g +ᵥ s = {a : β | ∃ (g : α), g +ᵥ a ∈ s}

Alias of Set.iUnion_vadd_eq_ofPred_exists.

@[simp]

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

@[simp]

theorem Set.neg_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) : -(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s

@[simp]

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

@[simp]

theorem Set.neg_op_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) : -(AddOpposite.op a +ᵥ s) = -a +ᵥ -s

@[simp]

theorem Set.disjoint_smul_set {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint (a • s) (a • t) ↔ Disjoint s t

@[simp]

theorem Set.disjoint_vadd_set {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint (a +ᵥ s) (a +ᵥ t) ↔ Disjoint s t

theorem Set.disjoint_smul_set_left {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

theorem Set.disjoint_vadd_set_left {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint (a +ᵥ s) t ↔ Disjoint s (-a +ᵥ t)

theorem Set.disjoint_smul_set_right {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t

theorem Set.disjoint_vadd_set_right {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint s (a +ᵥ t) ↔ Disjoint (-a +ᵥ s) t

theorem Set.pairwise_disjoint_smul_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : Pairwise (Function.onFun Disjoint fun (a : α) => a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

theorem Set.pairwise_disjoint_vadd_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : Pairwise (Function.onFun Disjoint fun (a : α) => a +ᵥ s) ↔ ∀ (a : α), ((a +ᵥ s) ∩ s).Nonempty → a = 0

theorem Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul {α : Type u_2} [Group α] (s t : Set α) (a b : α) : ∃ (z : α), a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Any intersection of translates of two sets s and t can be covered by a single translate of (s⁻¹ * s) ∩ (t⁻¹ * t).

This is useful to show that the intersection of approximate subgroups is an approximate subgroup.

theorem Set.exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add {α : Type u_2} [AddGroup α] (s t : Set α) (a b : α) : ∃ (z : α), (a +ᵥ s) ∩ (b +ᵥ t) ⊆ z +ᵥ (-s + s) ∩ (-t + t)

Any intersection of translates of two sets s and t can be covered by a single translate of (-s + s) ∩ (-t + t).

This is useful to show that the intersection of approximate subgroups is an approximate subgroup.

@[simp]

theorem Set.mem_invOf_smul_set {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] {s : Set β} {a : α} {b : β} [Invertible a] : b ∈ ⅟a • s ↔ a • b ∈ s

theorem Set.smul_graphOn {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [CommGroup β] [FunLike F α β] [MonoidHomClass F α β] (x : α × β) (s : Set α) (f : F) : x • graphOn (⇑f) s = graphOn (fun (a : α) => x.2 / f x.1 * f a) (x.1 • s)

theorem Set.vadd_graphOn {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [AddCommGroup β] [FunLike F α β] [AddMonoidHomClass F α β] (x : α × β) (s : Set α) (f : F) : x +ᵥ graphOn (⇑f) s = graphOn (fun (a : α) => x.2 - f x.1 + f a) (x.1 +ᵥ s)

theorem Set.smul_graphOn_univ {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [CommGroup β] [FunLike F α β] [MonoidHomClass F α β] (x : α × β) (f : F) : x • graphOn (⇑f) univ = graphOn (fun (a : α) => x.2 / f x.1 * f a) univ

theorem Set.vadd_graphOn_univ {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [AddCommGroup β] [FunLike F α β] [AddMonoidHomClass F α β] (x : α × β) (f : F) : x +ᵥ graphOn (⇑f) univ = graphOn (fun (a : α) => x.2 - f x.1 + f a) univ

theorem Set.smul_div_smul_comm {α : Type u_2} [CommGroup α] (a : α) (s : Set α) (b : α) (t : Set α) : a • s / b • t = (a / b) • (s / t)

theorem Set.vadd_sub_vadd_comm {α : Type u_2} [AddCommGroup α] (a : α) (s : Set α) (b : α) (t : Set α) : (a +ᵥ s) - (b +ᵥ t) = (a - b) +ᵥ s - t