Pointwise operations of sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines pointwise algebraic operations on sets.
Main declarations #
For sets s and t and scalar a:
s • t: Scalar multiplication, set of allx • ywherex ∈ sandy ∈ t.s +ᵥ t: Scalar addition, set of allx +ᵥ ywherex ∈ sandy ∈ t.s -ᵥ t: Scalar subtraction, set of allx -ᵥ ywherex ∈ sandy ∈ t.a • s: Scaling, set of alla • xwherex ∈ s.a +ᵥ s: Translation, set of alla +ᵥ xwherex ∈ s.
For α a semigroup/monoid, set α is a semigroup/monoid.
Appropriate definitions and results are also transported to the additive theory via to_additive.
Implementation notes #
- We put all instances in the locale
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 locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior ofsimp.
Translation/scaling of sets #
@[protected]
The dilation of set x • s is defined as {x • y | y ∈ s} in locale pointwise.
Equations
- set.has_smul_set = {smul := λ (a : α), set.image (has_smul.smul a)}
@[protected]
The translation of set x +ᵥ s is defined as {x +ᵥ y | y ∈ s} in
locale pointwise.
Equations
- set.has_vadd_set = {vadd := λ (a : α), set.image (has_vadd.vadd a)}
@[protected]
The pointwise scalar multiplication of sets s • t is defined as {x • y | x ∈ s, y ∈ t} in
locale pointwise.
Equations
@[protected]
The pointwise scalar addition of sets s +ᵥ t is defined as
{x +ᵥ y | x ∈ s, y ∈ t} in locale pointwise.
Equations
@[simp]
theorem
set.image2_smul
{α : Type u_2}
{β : Type u_3}
[has_smul α β]
{s : set α}
{t : set β} :
set.image2 has_smul.smul s t = s • t
@[simp]
theorem
set.image2_vadd
{α : Type u_2}
{β : Type u_3}
[has_vadd α β]
{s : set α}
{t : set β} :
set.image2 has_vadd.vadd s t = s +ᵥ t
@[protected, instance]
def
set.vadd_comm_class_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class α β (set γ)
@[protected, instance]
def
set.smul_comm_class_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α γ]
[has_smul β γ]
[smul_comm_class α β γ] :
smul_comm_class α β (set γ)
@[protected, instance]
def
set.vadd_comm_class_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class α (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α γ]
[has_smul β γ]
[smul_comm_class α β γ] :
smul_comm_class α (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class_set''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α γ]
[has_smul β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) β (set γ)
@[protected, instance]
def
set.vadd_comm_class_set''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) β (set γ)
@[protected, instance]
def
set.vadd_comm_class
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α γ]
[has_vadd β γ]
[vadd_comm_class α β γ] :
vadd_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.smul_comm_class
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α γ]
[has_smul β γ]
[smul_comm_class α β γ] :
smul_comm_class (set α) (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α β]
[has_smul α γ]
[has_smul β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α β (set γ)
@[protected, instance]
def
set.vadd_assoc_class
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α β]
[has_vadd α γ]
[has_vadd β γ]
[vadd_assoc_class α β γ] :
vadd_assoc_class α β (set γ)
@[protected, instance]
def
set.vadd_assoc_class'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α β]
[has_vadd α γ]
[has_vadd β γ]
[vadd_assoc_class α β γ] :
vadd_assoc_class α (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α β]
[has_smul α γ]
[has_smul β γ]
[is_scalar_tower α β γ] :
is_scalar_tower α (set β) (set γ)
@[protected, instance]
def
set.vadd_assoc_class''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_vadd α β]
[has_vadd α γ]
[has_vadd β γ]
[vadd_assoc_class α β γ] :
vadd_assoc_class (set α) (set β) (set γ)
@[protected, instance]
def
set.is_scalar_tower''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_smul α β]
[has_smul α γ]
[has_smul β γ]
[is_scalar_tower α β γ] :
is_scalar_tower (set α) (set β) (set γ)
@[protected, instance]
def
set.is_central_vadd
{α : Type u_2}
{β : Type u_3}
[has_vadd α β]
[has_vadd αᵃᵒᵖ β]
[is_central_vadd α β] :
is_central_vadd α (set β)
@[protected, instance]
def
set.is_central_scalar
{α : Type u_2}
{β : Type u_3}
[has_smul α β]
[has_smul αᵐᵒᵖ β]
[is_central_scalar α β] :
is_central_scalar α (set β)
@[protected]
def
set.mul_action
{α : Type u_2}
{β : Type u_3}
[monoid α]
[mul_action α β] :
mul_action (set α) (set β)
A multiplicative action of a monoid α on a type β gives a multiplicative action of set α
on set β.
Equations
- set.mul_action = {to_has_smul := set.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}
@[protected]
def
set.add_action
{α : Type u_2}
{β : Type u_3}
[add_monoid α]
[add_action α β] :
add_action (set α) (set β)
An additive action of an additive monoid α on a type β gives an additive action
of set α on set β
Equations
- set.add_action = {to_has_vadd := set.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected]
def
set.add_action_set
{α : Type u_2}
{β : Type u_3}
[add_monoid α]
[add_action α β] :
add_action α (set β)
An additive action of an additive monoid on a type β gives an additive action
on set β.
Equations
- set.add_action_set = {to_has_vadd := set.has_vadd_set add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected]
def
set.mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[mul_action α β] :
mul_action α (set β)
A multiplicative action of a monoid on a type β gives a multiplicative action on set β.
Equations
- set.mul_action_set = {to_has_smul := set.has_smul_set mul_action.to_has_smul, one_smul := _, mul_smul := _}
@[protected]
def
set.distrib_mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[add_monoid β]
[distrib_mul_action α β] :
distrib_mul_action α (set β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on set β.
Equations
@[protected]
def
set.mul_distrib_mul_action_set
{α : Type u_2}
{β : Type u_3}
[monoid α]
[monoid β]
[mul_distrib_mul_action α β] :
mul_distrib_mul_action α (set β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on set β.
Equations
@[protected, instance]
def
set.no_zero_smul_divisors
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[has_smul α β]
[no_zero_smul_divisors α β] :
no_zero_smul_divisors (set α) (set β)
@[protected, instance]
def
set.no_zero_smul_divisors_set
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[has_smul α β]
[no_zero_smul_divisors α β] :
no_zero_smul_divisors α (set β)
@[protected, instance]
def
set.no_zero_divisors
{α : Type u_2}
[has_zero α]
[has_mul α]
[no_zero_divisors α] :
no_zero_divisors (set α)
@[protected, instance]
Equations
@[simp]
theorem
set.image2_vsub
{α : Type u_2}
{β : Type u_3}
[has_vsub α β]
{s t : set β} :
set.image2 has_vsub.vsub s t = s -ᵥ t
@[simp]
theorem
set.singleton_vsub
{α : Type u_2}
{β : Type u_3}
[has_vsub α β]
(t : set β)
(b : β) :
{b} -ᵥ t = has_vsub.vsub b '' t
theorem
set.image_smul_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[mul_one_class α]
[mul_one_class β]
[monoid_hom_class F α β]
(f : F)
(a : α)
(s : set α) :
theorem
set.image_vadd_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[add_zero_class α]
[add_zero_class β]
[add_monoid_hom_class F α β]
(f : F)
(a : α)
(s : set α) :
Note that we have neither smul_with_zero α (set β) nor smul_with_zero (set α) (set β)
because 0 * ∅ ≠ 0.
theorem
set.smul_zero_subset
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set α) :
theorem
set.zero_smul_subset
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(t : set β) :
theorem
set.zero_smul_set_subset
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set β) :
theorem
set.subsingleton_zero_smul_set
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
(s : set β) :
(0 • s).subsingleton
theorem
set.zero_mem_smul_set_iff
{α : Type u_2}
{β : Type u_3}
[has_zero α]
[has_zero β]
[smul_with_zero α β]
{t : set β}
[no_zero_smul_divisors α β]
{a : α}
(ha : a ≠ 0) :
theorem
set.op_vadd_set_add_eq_add_vadd_set
{α : Type u_2}
[add_semigroup α]
(a : α)
(s t : set α) :
theorem
set.pairwise_disjoint_smul_iff
{α : Type u_2}
[left_cancel_semigroup α]
{s t : set α} :
s.pairwise_disjoint (λ (_x : α), _x • t) ↔ set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
theorem
set.pairwise_disjoint_vadd_iff
{α : Type u_2}
[add_left_cancel_semigroup α]
{s t : set α} :
s.pairwise_disjoint (λ (_x : α), _x +ᵥ t) ↔ set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
@[simp]
@[simp]
@[simp]
theorem
set.smul_mem_smul_set_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
set.mem_smul_set_iff_inv_smul_mem₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
set.mem_inv_smul_set_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(A : set β)
(x : β) :
theorem
set.preimage_smul₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
theorem
set.preimage_smul_inv₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
(t : set β) :
@[simp]
theorem
set.set_smul_subset_set_smul_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
set.set_smul_subset_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
set.subset_set_smul_iff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{A B : set β} :
theorem
set.smul_set_inter₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s t : set β}
{a : α}
(ha : a ≠ 0) :
theorem
set.smul_set_sdiff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s t : set β}
{a : α}
(ha : a ≠ 0) :
theorem
set.smul_set_symm_diff₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s t : set β}
{a : α}
(ha : a ≠ 0) :
theorem
set.smul_set_univ₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0) :
theorem
set.smul_univ₀
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s : set α}
(hs : ¬s ⊆ 0) :
theorem
set.smul_univ₀'
{α : Type u_2}
{β : Type u_3}
[group_with_zero α]
[mul_action α β]
{s : set α}
(hs : s.nontrivial) :