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 ofsimp).
Translation/scaling of sets #
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
@[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.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.image_smul_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Mul α]
[Mul β]
[FunLike F α β]
[MulHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
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}
[Mul α]
[IsLeftCancelMul α]
{s 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}
[Add α]
[IsLeftCancelAdd α]
{s 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 β)
@[implicit_reducible]
A multiplicative action of a monoid on a type β gives a multiplicative action on Set β.
Instances For
@[simp]
@[simp]
@[simp]
theorem
Set.mem_smul_set_inv
{α : Type u_2}
[Group α]
{a b : α}
{s : Set α}
:
a ∈ b • s⁻¹ ↔ b ∈ a • s
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[deprecated Set.smul_inter_nonempty_iff (since := "2025-12-10")]
theorem
Set.smul_inter_ne_empty_iff
{α : Type u_2}
[Group α]
{s t : Set α}
{x : α}
:
x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
@[deprecated Set.smul_inter_nonempty_iff (since := "2025-12-10")]
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
@[deprecated Set.smul_inter_nonempty_iff' (since := "2025-12-10")]
theorem
Set.smul_inter_ne_empty_iff'
{α : Type u_2}
[Group α]
{s t : Set α}
{x : α}
:
x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x
@[deprecated Set.smul_inter_nonempty_iff' (since := "2025-12-10")]
theorem
Set.vadd_inter_ne_empty_iff'
{α : Type u_2}
[AddGroup α]
{s t : Set α}
{x : α}
:
(x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ (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
@[deprecated Set.op_smul_inter_nonempty_iff (since := "2025-12-10")]
theorem
Set.op_smul_inter_ne_empty_iff
{α : Type u_2}
[Group α]
{s t : Set α}
{x : αᵐᵒᵖ}
:
x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x
@[deprecated Set.op_smul_inter_nonempty_iff (since := "2025-12-10")]
theorem
Set.op_vadd_inter_ne_empty_iff
{α : Type u_2}
[AddGroup α]
{s t : Set α}
{x : αᵃᵒᵖ}
:
(x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ -a + b = AddOpposite.unop x
@[simp]
@[simp]
theorem
Set.inv_smul_set_distrib
{α : Type u_2}
[Group α]
(a : α)
(s : Set α)
:
(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
@[simp]
@[simp]
theorem
Set.inv_op_smul_set_distrib
{α : Type u_2}
[Group α]
(a : α)
(s : Set α)
:
(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
@[simp]
@[simp]
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.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul
{α : Type u_2}
[Group α]
(s t : Set α)
(a b : α)
:
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 : α)
:
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.vadd_graphOn
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddCommGroup β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(x : α × β)
(s : Set α)
(f : F)
:
theorem
Set.vadd_graphOn_univ
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddCommGroup β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(x : α × β)
(f : F)
:
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 α)
: