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.vadd_nonempty
{α : Type u_2}
{β : Type u_1}
[inst : 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_1}
[inst : SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.vadd
{α : Type u_1}
{β : Type u_2}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s +ᵥ t)
theorem
Set.Nonempty.smul
{α : Type u_1}
{β : Type u_2}
[inst : 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_1}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s +ᵥ t) → Set.Nonempty s
theorem
Set.Nonempty.of_smul_left
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) → Set.Nonempty s
theorem
Set.Nonempty.of_vadd_right
{α : Type u_2}
{β : Type u_1}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s +ᵥ t) → Set.Nonempty t
theorem
Set.Nonempty.of_smul_right
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set α}
{t : Set β}
:
Set.Nonempty (s • t) → Set.Nonempty t
theorem
Set.unionᵢ_vadd_left_image
{α : Type u_2}
{β : Type u_1}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => a +ᵥ t) = s +ᵥ t
theorem
Set.unionᵢ_smul_left_image
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set α}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => a • t) = s • t
theorem
Set.unionᵢ_vadd_right_image
{α : Type u_2}
{β : Type u_1}
[inst : VAdd α β]
{s : Set α}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x +ᵥ a) '' s) = s +ᵥ t
theorem
Set.unionᵢ_smul_right_image
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set α}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x • a) '' s) = s • t
theorem
Set.unionᵢ_vadd
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : VAdd α β]
(s : ι → Set α)
(t : Set β)
:
(Set.unionᵢ fun i => s i) +ᵥ t = Set.unionᵢ fun i => s i +ᵥ t
theorem
Set.unionᵢ_smul
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : SMul α β]
(s : ι → Set α)
(t : Set β)
:
(Set.unionᵢ fun i => s i) • t = Set.unionᵢ fun i => s i • t
theorem
Set.vadd_unionᵢ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : VAdd α β]
(s : Set α)
(t : ι → Set β)
:
(s +ᵥ Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s +ᵥ t i
theorem
Set.smul_unionᵢ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : SMul α β]
(s : Set α)
(t : ι → Set β)
:
(s • Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s • t i
theorem
Set.unionᵢ₂_vadd
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) +ᵥ t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j +ᵥ t
theorem
Set.unionᵢ₂_smul
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) • t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j • t
theorem
Set.vadd_unionᵢ₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
(s +ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s +ᵥ t i j
theorem
Set.smul_unionᵢ₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
(s • Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s • t i j
theorem
Set.interᵢ_vadd_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : VAdd α β]
(s : ι → Set α)
(t : Set β)
:
(Set.interᵢ fun i => s i) +ᵥ t ⊆ Set.interᵢ fun i => s i +ᵥ t
theorem
Set.interᵢ_smul_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : SMul α β]
(s : ι → Set α)
(t : Set β)
:
(Set.interᵢ fun i => s i) • t ⊆ Set.interᵢ fun i => s i • t
theorem
Set.vadd_interᵢ_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : VAdd α β]
(s : Set α)
(t : ι → Set β)
:
(s +ᵥ Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s +ᵥ t i
theorem
Set.smul_interᵢ_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
[inst : SMul α β]
(s : Set α)
(t : ι → Set β)
:
(s • Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s • t i
theorem
Set.interᵢ₂_vadd_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) +ᵥ t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j +ᵥ t
theorem
Set.interᵢ₂_smul_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) • t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j • t
theorem
Set.vadd_interᵢ₂_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
(s +ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s +ᵥ t i j
theorem
Set.smul_interᵢ₂_subset
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
(s • Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s • t i j
@[simp]
theorem
Set.unionᵢ_vadd_set
{α : Type u_1}
{β : Type u_2}
[inst : VAdd α β]
(s : Set α)
(t : Set β)
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => a +ᵥ t) = s +ᵥ t
@[simp]
theorem
Set.unionᵢ_smul_set
{α : Type u_1}
{β : Type u_2}
[inst : SMul α β]
(s : Set α)
(t : Set β)
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => a • t) = s • t
@[simp]
theorem
Set.vadd_set_nonempty
{α : Type u_2}
{β : Type u_1}
[inst : VAdd α β]
{s : Set β}
{a : α}
:
Set.Nonempty (a +ᵥ s) ↔ Set.Nonempty s
@[simp]
theorem
Set.smul_set_nonempty
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set β}
{a : α}
:
Set.Nonempty (a • s) ↔ Set.Nonempty s
theorem
Set.vadd_set_Union
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VAdd α β]
(a : α)
(s : ι → Set β)
:
(a +ᵥ Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => a +ᵥ s i
theorem
Set.smul_set_Union
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : SMul α β]
(a : α)
(s : ι → Set β)
:
(a • Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => a • s i
theorem
Set.vadd_set_unionᵢ₂
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(a : α)
(s : (i : ι) → κ i → Set β)
:
(a +ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => a +ᵥ s i j
theorem
Set.smul_set_unionᵢ₂
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(a : α)
(s : (i : ι) → κ i → Set β)
:
(a • Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => a • s i j
theorem
Set.vadd_set_interᵢ_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VAdd α β]
(a : α)
(t : ι → Set β)
:
(a +ᵥ Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => a +ᵥ t i
theorem
Set.smul_set_interᵢ_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : SMul α β]
(a : α)
(t : ι → Set β)
:
(a • Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => a • t i
theorem
Set.vadd_set_interᵢ₂_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VAdd α β]
(a : α)
(t : (i : ι) → κ i → Set β)
:
(a +ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => a +ᵥ t i j
theorem
Set.smul_set_interᵢ₂_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : SMul α β]
(a : α)
(t : (i : ι) → κ i → Set β)
:
(a • Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => a • t i j
theorem
Set.Nonempty.vadd_set
{α : Type u_2}
{β : Type u_1}
[inst : VAdd α β]
{s : Set β}
{a : α}
:
Set.Nonempty s → Set.Nonempty (a +ᵥ s)
theorem
Set.Nonempty.smul_set
{α : Type u_2}
{β : Type u_1}
[inst : SMul α β]
{s : Set β}
{a : α}
:
Set.Nonempty s → Set.Nonempty (a • s)
@[simp]
theorem
Set.unionᵢ_op_vadd_set
{α : Type u_1}
[inst : Add α]
(s : Set α)
(t : Set α)
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => { unop := a } +ᵥ s) = s + t
@[simp]
theorem
Set.unionᵢ_op_smul_set
{α : Type u_1}
[inst : Mul α]
(s : Set α)
(t : Set α)
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => { unop := a } • s) = s * t
def
Set.vaddCommClass_set.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass α β (Set γ)
Equations
- (_ : VAddCommClass α β (Set γ)) = (_ : VAddCommClass α β (Set γ))
instance
Set.vaddCommClass_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass α β (Set γ)
instance
Set.smulCommClass_set
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α γ]
[inst : SMul β γ]
[inst : SMulCommClass α β γ]
:
SMulCommClass α β (Set γ)
instance
Set.vaddCommClass_set'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass α (Set β) (Set γ)
def
Set.vaddCommClass_set'.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass α (Set β) (Set γ)
Equations
- (_ : VAddCommClass α (Set β) (Set γ)) = (_ : VAddCommClass α (Set β) (Set γ))
instance
Set.smulCommClass_set'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α γ]
[inst : SMul β γ]
[inst : SMulCommClass α β γ]
:
SMulCommClass α (Set β) (Set γ)
def
Set.vaddCommClass_set''.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass (Set α) β (Set γ)
Equations
- (_ : VAddCommClass (Set α) β (Set γ)) = (_ : VAddCommClass (Set α) β (Set γ))
instance
Set.vaddCommClass_set''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass (Set α) β (Set γ)
instance
Set.smulCommClass_set''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α γ]
[inst : SMul β γ]
[inst : SMulCommClass α β γ]
:
SMulCommClass (Set α) β (Set γ)
def
Set.vaddCommClass.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass (Set α) (Set β) (Set γ)
Equations
- (_ : VAddCommClass (Set α) (Set β) (Set γ)) = (_ : VAddCommClass (Set α) (Set β) (Set γ))
instance
Set.vaddCommClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddCommClass α β γ]
:
VAddCommClass (Set α) (Set β) (Set γ)
instance
Set.smulCommClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α γ]
[inst : SMul β γ]
[inst : SMulCommClass α β γ]
:
SMulCommClass (Set α) (Set β) (Set γ)
def
Set.vAddAssocClass.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass α β (Set γ)
Equations
- (_ : VAddAssocClass α β (Set γ)) = (_ : VAddAssocClass α β (Set γ))
instance
Set.vAddAssocClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass α β (Set γ)
instance
Set.isScalarTower
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α β]
[inst : SMul α γ]
[inst : SMul β γ]
[inst : IsScalarTower α β γ]
:
IsScalarTower α β (Set γ)
def
Set.vAddAssocClass'.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass α (Set β) (Set γ)
Equations
- (_ : VAddAssocClass α (Set β) (Set γ)) = (_ : VAddAssocClass α (Set β) (Set γ))
instance
Set.vAddAssocClass'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass α (Set β) (Set γ)
instance
Set.isScalarTower'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α β]
[inst : SMul α γ]
[inst : SMul β γ]
[inst : IsScalarTower α β γ]
:
IsScalarTower α (Set β) (Set γ)
def
Set.vAddAssocClass''.proof_1
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass (Set α) (Set β) (Set γ)
Equations
- (_ : VAddAssocClass (Set α) (Set β) (Set γ)) = (_ : VAddAssocClass (Set α) (Set β) (Set γ))
instance
Set.vAddAssocClass''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : VAdd α β]
[inst : VAdd α γ]
[inst : VAdd β γ]
[inst : VAddAssocClass α β γ]
:
VAddAssocClass (Set α) (Set β) (Set γ)
instance
Set.isScalarTower''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[inst : SMul α β]
[inst : SMul α γ]
[inst : SMul β γ]
[inst : IsScalarTower α β γ]
:
IsScalarTower (Set α) (Set β) (Set γ)
def
Set.isCentralVAdd.proof_1
{α : Type u_1}
{β : Type u_2}
[inst : VAdd α β]
[inst : VAdd αᵃᵒᵖ β]
[inst : IsCentralVAdd α β]
:
IsCentralVAdd α (Set β)
Equations
- (_ : IsCentralVAdd α (Set β)) = (_ : IsCentralVAdd α (Set β))
instance
Set.isCentralVAdd
{α : Type u_1}
{β : Type u_2}
[inst : VAdd α β]
[inst : VAdd αᵃᵒᵖ β]
[inst : IsCentralVAdd α β]
:
IsCentralVAdd α (Set β)
instance
Set.isCentralScalar
{α : Type u_1}
{β : Type u_2}
[inst : SMul α β]
[inst : SMul αᵐᵒᵖ β]
[inst : IsCentralScalar α β]
:
IsCentralScalar α (Set β)
def
Set.addAction.proof_2
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoid α]
[inst : 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)
Equations
- One or more equations did not get rendered due to their size.
def
Set.addAction.proof_1
{α : Type u_2}
{β : Type u_1}
[inst : AddMonoid α]
[inst : AddAction α β]
(s : Set β)
:
Set.image2 (fun x x_1 => x +ᵥ x_1) {0} s = s
Equations
- (_ : Set.image2 (fun x x_1 => x +ᵥ x_1) {0} s = s) = (_ : Set.image2 (fun x x_1 => x +ᵥ x_1) {0} s = s)
def
Set.addActionSet.proof_2
{α : Type u_2}
{β : Type u_1}
[inst : AddMonoid α]
[inst : AddAction α β]
:
def
Set.distribMulActionSet
{α : Type u_1}
{β : Type u_2}
[inst : Monoid α]
[inst : AddMonoid β]
[inst : DistribMulAction α β]
:
DistribMulAction α (Set β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on Set β.
Equations
- One or more equations did not get rendered due to their size.
def
Set.mulDistribMulActionSet
{α : Type u_1}
{β : Type u_2}
[inst : Monoid α]
[inst : Monoid β]
[inst : MulDistribMulAction α β]
:
MulDistribMulAction α (Set β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.
Equations
- One or more equations did not get rendered due to their size.
instance
Set.instNoZeroSMulDivisorsSetSetZeroZeroSmul
{α : Type u_1}
{β : Type u_2}
[inst : Zero α]
[inst : Zero β]
[inst : SMul α β]
[inst : NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors (Set α) (Set β)
instance
Set.noZeroSMulDivisors_set
{α : Type u_1}
{β : Type u_2}
[inst : Zero α]
[inst : Zero β]
[inst : SMul α β]
[inst : NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (Set β)
instance
Set.instNoZeroDivisorsSetMulZero
{α : Type u_1}
[inst : Zero α]
[inst : Mul α]
[inst : NoZeroDivisors α]
:
NoZeroDivisors (Set α)
@[simp]
theorem
Set.vsub_nonempty
{α : Type u_1}
{β : Type u_2}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.vsub
{α : Type u_2}
{β : Type u_1}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s -ᵥ t)
theorem
Set.Nonempty.of_vsub_left
{α : Type u_1}
{β : Type u_2}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) → Set.Nonempty s
theorem
Set.Nonempty.of_vsub_right
{α : Type u_1}
{β : Type u_2}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
Set.Nonempty (s -ᵥ t) → Set.Nonempty t
theorem
Set.unionᵢ_vsub_left_image
{α : Type u_1}
{β : Type u_2}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x -ᵥ x_1) a '' t) = s -ᵥ t
theorem
Set.unionᵢ_vsub_right_image
{α : Type u_1}
{β : Type u_2}
[inst : VSub α β]
{s : Set β}
{t : Set β}
:
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x -ᵥ a) '' s) = s -ᵥ t
theorem
Set.unionᵢ_vsub
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VSub α β]
(s : ι → Set β)
(t : Set β)
:
(Set.unionᵢ fun i => s i) -ᵥ t = Set.unionᵢ fun i => s i -ᵥ t
theorem
Set.vsub_unionᵢ
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VSub α β]
(s : Set β)
(t : ι → Set β)
:
(s -ᵥ Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s -ᵥ t i
theorem
Set.unionᵢ₂_vsub
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VSub α β]
(s : (i : ι) → κ i → Set β)
(t : Set β)
:
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) -ᵥ t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j -ᵥ t
theorem
Set.vsub_unionᵢ₂
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VSub α β]
(s : Set β)
(t : (i : ι) → κ i → Set β)
:
(s -ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s -ᵥ t i j
theorem
Set.interᵢ_vsub_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VSub α β]
(s : ι → Set β)
(t : Set β)
:
(Set.interᵢ fun i => s i) -ᵥ t ⊆ Set.interᵢ fun i => s i -ᵥ t
theorem
Set.vsub_interᵢ_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
[inst : VSub α β]
(s : Set β)
(t : ι → Set β)
:
(s -ᵥ Set.interᵢ fun i => t i) ⊆ Set.interᵢ fun i => s -ᵥ t i
theorem
Set.interᵢ₂_vsub_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VSub α β]
(s : (i : ι) → κ i → Set β)
(t : Set β)
:
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) -ᵥ t ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s i j -ᵥ t
theorem
Set.vsub_interᵢ₂_subset
{α : Type u_2}
{β : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[inst : VSub α β]
(s : Set β)
(t : (i : ι) → κ i → Set β)
:
(s -ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => s -ᵥ t i j
theorem
Set.image_vadd_distrib
{F : Type u_3}
{α : Type u_1}
{β : Type u_2}
[inst : AddZeroClass α]
[inst : AddZeroClass β]
[inst : AddMonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
theorem
Set.image_smul_distrib
{F : Type u_3}
{α : Type u_1}
{β : Type u_2}
[inst : MulOneClass α]
[inst : MulOneClass β]
[inst : MonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β)
because 0 * ∅ ≠ 0.
theorem
Set.Nonempty.smul_zero
{α : Type u_1}
{β : Type u_2}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
{s : Set α}
(hs : Set.Nonempty s)
:
theorem
Set.Nonempty.zero_smul
{α : Type u_2}
{β : Type u_1}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
{t : Set β}
(ht : Set.Nonempty t)
:
theorem
Set.zero_smul_set
{α : Type u_2}
{β : Type u_1}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
{s : Set β}
(h : Set.Nonempty s)
:
A nonempty set is scaled by zero to the singleton set containing 0.
theorem
Set.subsingleton_zero_smul_set
{α : Type u_2}
{β : Type u_1}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
(s : Set β)
:
Set.Subsingleton (0 • s)
theorem
Set.zero_mem_smul_iff
{α : Type u_2}
{β : Type u_1}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
{s : Set α}
{t : Set β}
[inst : NoZeroSMulDivisors α β]
:
0 ∈ s • t ↔ 0 ∈ s ∧ Set.Nonempty t ∨ 0 ∈ t ∧ Set.Nonempty s
theorem
Set.zero_mem_smul_set_iff
{α : Type u_1}
{β : Type u_2}
[inst : Zero α]
[inst : Zero β]
[inst : SMulWithZero α β]
{t : Set β}
[inst : NoZeroSMulDivisors α β]
{a : α}
(ha : a ≠ 0)
:
theorem
Set.pairwiseDisjoint_vadd_iff
{α : Type u_1}
[inst : AddLeftCancelSemigroup α]
{s : Set α}
{t : Set α}
:
theorem
Set.pairwiseDisjoint_smul_iff
{α : Type u_1}
[inst : 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
Equations
- Set.vadd_univ.match_1 motive hs h_1 = Exists.casesOn hs fun w h => h_1 w h
@[simp]
theorem
Set.unionᵢ_neg_vadd
{α : Type u_2}
{β : Type u_1}
[inst : AddGroup α]
[inst : AddAction α β]
{s : Set β}
:
(Set.unionᵢ fun g => -g +ᵥ s) = Set.unionᵢ fun g => g +ᵥ s
@[simp]
theorem
Set.unionᵢ_inv_smul
{α : Type u_2}
{β : Type u_1}
[inst : Group α]
[inst : MulAction α β]
{s : Set β}
:
(Set.unionᵢ fun g => g⁻¹ • s) = Set.unionᵢ fun g => g • s
theorem
Set.smul_set_univ₀
{α : Type u_1}
{β : Type u_2}
[inst : GroupWithZero α]
[inst : MulAction α β]
{a : α}
(ha : a ≠ 0)
:
theorem
Set.smul_univ₀'
{α : Type u_1}
{β : Type u_2}
[inst : GroupWithZero α]
[inst : MulAction α β]
{s : Set α}
(hs : Set.Nontrivial s)
: