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.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]
@[simp]
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 α)
:
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 α)
:
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 β)
A multiplicative action of a monoid on a type β gives a multiplicative action on Set β.
Equations
- Set.mulActionSet = { toSMul := Set.smulSet, mul_smul := ⋯, one_smul := ⋯ }
Instances For
An additive action of an additive monoid on a type β gives an additive action on Set β.
Equations
- Set.addActionSet = { toVAdd := Set.vaddSet, add_vadd := ⋯, zero_vadd := ⋯ }
Instances For
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.