Pointwise operations of sets #
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 #
@[simp]
theorem
Set.image2_vadd
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.image2 VAdd.vadd s t = s +ᵥ t
@[simp]
theorem
Set.image2_smul
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.image2 SMul.smul s t = s • t
@[simp]
theorem
Set.vadd_nonempty
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s +ᵥ t) ↔ Set.Nonempty s ∧ Set.Nonempty t
@[simp]
theorem
Set.smul_nonempty
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.vadd
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s +ᵥ t)
theorem
Set.Nonempty.smul
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s • t)
theorem
Set.Nonempty.of_vadd_left
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s +ᵥ t) → Set.Nonempty s
theorem
Set.Nonempty.of_smul_left
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) → Set.Nonempty s
theorem
Set.Nonempty.of_vadd_right
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s +ᵥ t) → Set.Nonempty t
theorem
Set.Nonempty.of_smul_right
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) → Set.Nonempty t
@[simp]
theorem
Set.vadd_set_nonempty
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set β}
{a : α}
:
Set.Nonempty (a +ᵥ s) ↔ Set.Nonempty s
@[simp]
theorem
Set.smul_set_nonempty
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set β}
{a : α}
:
Set.Nonempty (a • s) ↔ Set.Nonempty s
theorem
Set.Nonempty.vadd_set
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
{s : Set β}
{a : α}
:
Set.Nonempty s → Set.Nonempty (a +ᵥ s)
theorem
Set.Nonempty.smul_set
{α : Type u_2}
{β : Type u_3}
[SMul α β]
{s : Set β}
{a : α}
:
Set.Nonempty s → Set.Nonempty (a • s)
theorem
Set.vaddCommClass_set.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α β (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 γ)
instance
Set.vaddCommClass_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α (Set β) (Set γ)
theorem
Set.vaddCommClass_set'.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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 γ)
theorem
Set.vaddCommClass_set''.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (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
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Set α) (Set β) (Set γ)
theorem
Set.vaddCommClass.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Set α) (Set β) (Set γ)
instance
Set.smulCommClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass (Set α) (Set β) (Set γ)
instance
Set.vAddAssocClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α β (Set γ)
theorem
Set.vAddAssocClass.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α β (Set γ)
instance
Set.isScalarTower
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower α β (Set γ)
theorem
Set.vAddAssocClass'.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α (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 γ)
instance
Set.vAddAssocClass''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass (Set α) (Set β) (Set γ)
theorem
Set.vAddAssocClass''.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass (Set α) (Set β) (Set γ)
instance
Set.isScalarTower''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower (Set α) (Set β) (Set γ)
theorem
Set.isCentralVAdd.proof_1
{α : Type u_1}
{β : Type u_2}
[VAdd α β]
[VAdd αᵃᵒᵖ β]
[IsCentralVAdd α β]
:
IsCentralVAdd α (Set β)
instance
Set.isCentralVAdd
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
[VAdd αᵃᵒᵖ β]
[IsCentralVAdd α β]
:
IsCentralVAdd α (Set β)
instance
Set.isCentralScalar
{α : Type u_2}
{β : Type u_3}
[SMul α β]
[SMul αᵐᵒᵖ β]
[IsCentralScalar α β]
:
IsCentralScalar α (Set β)
theorem
Set.addAction.proof_2
{α : Type u_1}
{β : Type u_2}
[AddMonoid α]
[AddAction α β]
:
∀ (x x_1 : Set α) (x_2 : Set β),
Set.image2 (fun x x_3 => x +ᵥ x_3) (Set.image2 (fun x x_3 => x + x_3) x x_1) x_2 = Set.image2 (fun x x_3 => x +ᵥ x_3) x (Set.image2 (fun x x_3 => x +ᵥ x_3) x_1 x_2)
theorem
Set.addAction.proof_1
{α : Type u_2}
{β : Type u_1}
[AddMonoid α]
[AddAction α β]
(s : Set β)
:
Set.image2 (fun x x_1 => x +ᵥ x_1) {0} s = s
def
Set.distribMulActionSet
{α : Type u_2}
{β : Type u_3}
[Monoid α]
[AddMonoid β]
[DistribMulAction α β]
:
DistribMulAction α (Set β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on Set β.
Instances For
def
Set.mulDistribMulActionSet
{α : Type u_2}
{β : Type u_3}
[Monoid α]
[Monoid β]
[MulDistribMulAction α β]
:
MulDistribMulAction α (Set β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.
Instances For
instance
Set.instNoZeroSMulDivisorsSetSetZeroZeroSmul
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMul α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors (Set α) (Set β)
instance
Set.noZeroSMulDivisors_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMul α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (Set β)
instance
Set.instNoZeroDivisorsSetMulZero
{α : Type u_2}
[Zero α]
[Mul α]
[NoZeroDivisors α]
:
NoZeroDivisors (Set α)
@[simp]
theorem
Set.image2_vsub
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
:
Set.image2 VSub.vsub s t = s -ᵥ t
@[simp]
theorem
Set.vsub_nonempty
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.vsub
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s -ᵥ t)
theorem
Set.Nonempty.of_vsub_left
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) → Set.Nonempty s
theorem
Set.Nonempty.of_vsub_right
{α : Type u_2}
{β : Type u_3}
[VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) → Set.Nonempty t
theorem
Set.image_vadd_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddZeroClass α]
[AddZeroClass β]
[AddMonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
theorem
Set.image_smul_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[MulOneClass α]
[MulOneClass β]
[MonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β)
because 0 * ∅ ≠ 0.
theorem
Set.smul_zero_subset
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Set α)
:
theorem
Set.zero_smul_subset
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(t : Set β)
:
theorem
Set.Nonempty.smul_zero
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{s : Set α}
(hs : Set.Nonempty s)
:
theorem
Set.Nonempty.zero_smul
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{t : Set β}
(ht : Set.Nonempty t)
:
theorem
Set.zero_smul_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{s : Set β}
(h : Set.Nonempty s)
:
A nonempty set is scaled by zero to the singleton set containing 0.
theorem
Set.zero_smul_set_subset
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Set β)
:
theorem
Set.subsingleton_zero_smul_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Set β)
:
Set.Subsingleton (0 • s)
theorem
Set.zero_mem_smul_iff
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{s : Set α}
{t : Set β}
[NoZeroSMulDivisors α β]
:
0 ∈ s • t ↔ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
theorem
Set.zero_mem_smul_set_iff
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{t : Set β}
[NoZeroSMulDivisors α β]
{a : α}
(ha : a ≠ 0)
:
theorem
Set.op_vadd_set_add_eq_add_vadd_set
{α : Type u_2}
[AddSemigroup α]
(a : α)
(s : Set α)
(t : Set α)
:
theorem
Set.pairwiseDisjoint_vadd_iff
{α : Type u_2}
[AddLeftCancelSemigroup α]
{s : Set α}
{t : Set α}
:
theorem
Set.pairwiseDisjoint_smul_iff
{α : Type u_2}
[LeftCancelSemigroup α]
{s : Set α}
{t : Set α}
:
abbrev
Set.vadd_univ.match_1
{α : Type u_1}
{s : Set α}
(motive : Set.Nonempty s → Prop)
:
(hs : Set.Nonempty s) → ((a : α) → (ha : a ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive hs
Instances For
@[simp]
theorem
Set.vadd_univ
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddAction α β]
{s : Set α}
(hs : Set.Nonempty s)
:
@[simp]
theorem
Set.smul_univ
{α : Type u_2}
{β : Type u_3}
[Group α]
[MulAction α β]
{s : Set α}
(hs : Set.Nonempty s)
:
theorem
Set.smul_set_univ₀
{α : Type u_2}
{β : Type u_3}
[GroupWithZero α]
[MulAction α β]
{a : α}
(ha : a ≠ 0)
:
theorem
Set.smul_univ₀'
{α : Type u_2}
{β : Type u_3}
[GroupWithZero α]
[MulAction α β]
{s : Set α}
(hs : Set.Nontrivial s)
: