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 all x • y where x ∈ s and y ∈ t.
• s +ᵥ t: Scalar addition, set of all x +ᵥ y where x ∈ s and y ∈ t.
• s -ᵥ t: Scalar subtraction, set of all x -ᵥ y where x ∈ s and y ∈ t.
• a • s: Scaling, set of all a • x where x ∈ s.
• a +ᵥ s: Translation, set of all a +ᵥ x where x ∈ 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 of simp.

Translation/scaling of sets

def Set.vaddSet {α : Type u_2} {β : Type u_3} [VAdd α β] : VAdd α (Set β)

The translation of set x +ᵥ s is defined as {x +ᵥ y | y ∈ s} in locale Pointwise.

Equations

• Set.vaddSet = { vadd := fun (a : α) => Set.image fun (x : β) => a +ᵥ x }

def Set.smulSet {α : Type u_2} {β : Type u_3} [SMul α β] : SMul α (Set β)

The dilation of set x • s is defined as {x • y | y ∈ s} in locale Pointwise.

Equations

• Set.smulSet = { smul := fun (a : α) => Set.image fun (x : β) => a • x }

def Set.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] : VAdd (Set α) (Set β)

The pointwise scalar addition of sets s +ᵥ t is defined as {x +ᵥ y | x ∈ s, y ∈ t} in locale Pointwise.

Equations

• Set.vadd = { vadd := Set.image2 fun (x : α) (x_1 : β) => x +ᵥ x_1 }

def Set.smul {α : Type u_2} {β : Type u_3} [SMul α β] : SMul (Set α) (Set β)

The pointwise scalar multiplication of sets s • t is defined as {x • y | x ∈ s, y ∈ t} in locale Pointwise.

Equations

• Set.smul = { smul := Set.image2 fun (x : α) (x_1 : β) => x • x_1 }

@[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

theorem Set.vadd_image_prod {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (fun (x : α × β) => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t

theorem Set.image_smul_prod {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (fun (x : α × β) => x.1 • x.2) '' s ×ˢ t = s • t

theorem Set.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {b : β} : b ∈ s +ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x +ᵥ y = b

theorem Set.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {b : β} : b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b

theorem Set.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {a : α} {b : β} : a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t

theorem Set.smul_mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {a : α} {b : β} : a ∈ s → b ∈ t → a • b ∈ s • t

@[simp]

theorem Set.empty_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} : ∅ +ᵥ t = ∅

@[simp]

theorem Set.empty_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} : ∅ • t = ∅

@[simp]

theorem Set.vadd_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} : s +ᵥ ∅ = ∅

@[simp]

theorem Set.smul_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} : s • ∅ = ∅

@[simp]

theorem Set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.smul_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : s • t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.vadd_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Set.smul_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty

theorem Set.Nonempty.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s • t).Nonempty

theorem Set.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty → t.Nonempty

theorem Set.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty → t.Nonempty

@[simp]

theorem Set.vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {b : β} : s +ᵥ {b} = (fun (x : α) => x +ᵥ b) '' s

@[simp]

theorem Set.smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {b : β} : s • {b} = (fun (x : α) => x • b) '' s

@[simp]

theorem Set.singleton_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} : {a} +ᵥ t = a +ᵥ t

@[simp]

theorem Set.singleton_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} : {a} • t = a • t

@[simp]

theorem Set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} : {a} +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem Set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} : {a} • {b} = {a • b}

theorem Set.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂

theorem Set.smul_subset_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂

theorem Set.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂

theorem Set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂

theorem Set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t

theorem Set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t

theorem Set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {u : Set β} : s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u

theorem Set.smul_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {u : Set β} : s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u

theorem Set.union_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ∪ s₂ +ᵥ t = s₁ +ᵥ t ∪ (s₂ +ᵥ t)

theorem Set.union_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

theorem Set.vadd_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s +ᵥ (t₁ ∪ t₂) = s +ᵥ t₁ ∪ (s +ᵥ t₂)

theorem Set.smul_union {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂

theorem Set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)

theorem Set.inter_smul_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t

theorem Set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)

theorem Set.smul_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂

theorem Set.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ∩ s₂ +ᵥ (t₁ ∪ t₂) ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)

theorem Set.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Set.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ∪ s₂ +ᵥ t₁ ∩ t₂ ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)

theorem Set.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Set.iUnion_vadd_left_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : ⋃ a ∈ s, a +ᵥ t = s +ᵥ t

theorem Set.iUnion_smul_left_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : ⋃ a ∈ s, a • t = s • t

theorem Set.iUnion_vadd_right_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : ⋃ a ∈ t, (fun (x : α) => x +ᵥ a) '' s = s +ᵥ t

theorem Set.iUnion_smul_right_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : ⋃ a ∈ t, (fun (x : α) => x • a) '' s = s • t

theorem Set.iUnion_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ι → Set α) (t : Set β) : (⋃ (i : ι), s i) +ᵥ t = ⋃ (i : ι), s i +ᵥ t

theorem Set.iUnion_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ι → Set α) (t : Set β) : (⋃ (i : ι), s i) • t = ⋃ (i : ι), s i • t

theorem Set.vadd_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ι → Set β) : s +ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s +ᵥ t i

theorem Set.smul_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ι → Set β) : s • ⋃ (i : ι), t i = ⋃ (i : ι), s • t i

theorem Set.iUnion₂_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) +ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j +ᵥ t

theorem Set.iUnion₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) • t = ⋃ (i : ι), ⋃ (j : κ i), s i j • t

theorem Set.vadd_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s +ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s +ᵥ t i j

theorem Set.smul_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s • ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s • t i j

theorem Set.iInter_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ι → Set α) (t : Set β) : (⋂ (i : ι), s i) +ᵥ t ⊆ ⋂ (i : ι), s i +ᵥ t

theorem Set.iInter_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ι → Set α) (t : Set β) : (⋂ (i : ι), s i) • t ⊆ ⋂ (i : ι), s i • t

theorem Set.vadd_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ι → Set β) : s +ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s +ᵥ t i

theorem Set.smul_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ι → Set β) : s • ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s • t i

theorem Set.iInter₂_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) +ᵥ t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j +ᵥ t

theorem Set.iInter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) • t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j • t

theorem Set.vadd_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s +ᵥ t i j

theorem Set.smul_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s • ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s • t i j

theorem Set.vadd_set_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {s : Set α} : a ∈ s → a +ᵥ t ⊆ s +ᵥ t

theorem Set.smul_set_subset_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {s : Set α} : a ∈ s → a • t ⊆ s • t

@[simp]

theorem Set.iUnion_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (t : Set β) : ⋃ a ∈ s, a +ᵥ t = s +ᵥ t

@[simp]

theorem Set.iUnion_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (t : Set β) : ⋃ a ∈ s, a • t = s • t

theorem Set.image_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} : (fun (x : β) => a +ᵥ x) '' t = a +ᵥ t

theorem Set.image_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} : (fun (x : β) => a • x) '' t = a • t

theorem Set.mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {x : β} : x ∈ a +ᵥ t ↔ ∃ y ∈ t, a +ᵥ y = x

theorem Set.mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {x : β} : x ∈ a • t ↔ ∃ y ∈ t, a • y = x

theorem Set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} {b : β} : b ∈ s → a +ᵥ b ∈ a +ᵥ s

theorem Set.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} {b : β} : b ∈ s → a • b ∈ a • s

@[simp]

theorem Set.vadd_set_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} : a +ᵥ ∅ = ∅

@[simp]

theorem Set.smul_set_empty {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} : a • ∅ = ∅

@[simp]

theorem Set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : a +ᵥ s = ∅ ↔ s = ∅

@[simp]

theorem Set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : a • s = ∅ ↔ s = ∅

@[simp]

theorem Set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : (a +ᵥ s).Nonempty ↔ s.Nonempty

@[simp]

theorem Set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : (a • s).Nonempty ↔ s.Nonempty

@[simp]

theorem Set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} : a +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem Set.smul_set_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} : a • {b} = {a • b}

theorem Set.vadd_set_mono {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} : s ⊆ t → a +ᵥ s ⊆ a +ᵥ t

theorem Set.smul_set_mono {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} : s ⊆ t → a • s ⊆ a • t

theorem Set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} : a +ᵥ s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a +ᵥ b ∈ t

theorem Set.smul_set_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} : a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t

theorem Set.vadd_set_union {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a +ᵥ (t₁ ∪ t₂) = a +ᵥ t₁ ∪ (a +ᵥ t₂)

theorem Set.smul_set_union {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂

theorem Set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a +ᵥ t₁ ∩ t₂ ⊆ (a +ᵥ t₁) ∩ (a +ᵥ t₂)

theorem Set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂

theorem Set.vadd_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (s : ι → Set β) : a +ᵥ ⋃ (i : ι), s i = ⋃ (i : ι), a +ᵥ s i

theorem Set.smul_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (s : ι → Set β) : a • ⋃ (i : ι), s i = ⋃ (i : ι), a • s i

theorem Set.vadd_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (a : α) (s : (i : ι) → κ i → Set β) : a +ᵥ ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a +ᵥ s i j

theorem Set.smul_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (a : α) (s : (i : ι) → κ i → Set β) : a • ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a • s i j

theorem Set.vadd_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (t : ι → Set β) : a +ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), a +ᵥ t i

theorem Set.smul_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (t : ι → Set β) : a • ⋂ (i : ι), t i ⊆ ⋂ (i : ι), a • t i

theorem Set.vadd_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (a : α) (t : (i : ι) → κ i → Set β) : a +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), a +ᵥ t i j

theorem Set.smul_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (a : α) (t : (i : ι) → κ i → Set β) : a • ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), a • t i j

theorem Set.Nonempty.vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : s.Nonempty → (a +ᵥ s).Nonempty

theorem Set.Nonempty.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : s.Nonempty → (a • s).Nonempty

theorem Set.op_vadd_set_subset_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} : a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t

theorem Set.op_smul_set_subset_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} : a ∈ t → MulOpposite.op a • s ⊆ s * t

theorem Set.image_op_vadd {α : Type u_2} [Add α] {s : Set α} {t : Set α} : AddOpposite.op '' s +ᵥ t = t + s

theorem Set.image_op_smul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : MulOpposite.op '' s • t = t * s

@[simp]

theorem Set.iUnion_op_vadd_set {α : Type u_2} [Add α] (s : Set α) (t : Set α) : ⋃ a ∈ t, AddOpposite.op a +ᵥ s = s + t

@[simp]

theorem Set.iUnion_op_smul_set {α : Type u_2} [Mul α] (s : Set α) (t : Set α) : ⋃ a ∈ t, MulOpposite.op a • s = s * t

theorem Set.add_subset_iff_left {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} : s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u

theorem Set.mul_subset_iff_left {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} : s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u

theorem Set.add_subset_iff_right {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} : s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u

theorem Set.mul_subset_iff_right {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} : s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u

theorem Set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [VAdd α β] (b : ι → α) (c : κ → β) : Set.range b +ᵥ Set.range c = Set.range fun (p : ι × κ) => b p.1 +ᵥ c p.2

theorem Set.range_smul_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [SMul α β] (b : ι → α) (c : κ → β) : Set.range b • Set.range c = Set.range fun (p : ι × κ) => b p.1 • c p.2

theorem Set.vadd_set_range {α : Type u_2} {β : Type u_3} {a : α} [VAdd α β] {ι : Sort u_5} {f : ι → β} : a +ᵥ Set.range f = Set.range fun (i : ι) => a +ᵥ f i

theorem Set.smul_set_range {α : Type u_2} {β : Type u_3} {a : α} [SMul α β] {ι : Sort u_5} {f : ι → β} : a • Set.range f = Set.range fun (i : ι) => a • f i

instance Set.vaddCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α β (Set γ)

Equations

• ⋯ = ⋯

instance Set.smulCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α β (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass α (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.smulCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass α (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Set α) β (Set γ)

Equations

• ⋯ = ⋯

instance Set.smulCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) β (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : VAddCommClass (Set α) (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : SMulCommClass (Set α) (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α β (Set γ)

Equations

• ⋯ = ⋯

instance Set.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass α (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [VAddAssocClass α β γ] : VAddAssocClass (Set α) (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Set α) (Set β) (Set γ)

Equations

• ⋯ = ⋯

instance Set.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [IsCentralVAdd α β] : IsCentralVAdd α (Set β)

Equations

• ⋯ = ⋯

instance Set.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Set β)

Equations

• ⋯ = ⋯

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)

def Set.addAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] : AddAction (Set α) (Set β)

An additive action of an additive monoid α on a type β gives an additive action of Set α on Set β

Equations

• Set.addAction = AddAction.mk ⋯ ⋯

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.mulAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] : MulAction (Set α) (Set β)

A multiplicative action of a monoid α on a type β gives a multiplicative action of Set α on Set β.

Equations

• Set.mulAction = MulAction.mk ⋯ ⋯

theorem Set.addActionSet.proof_1 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] : ∀ (x : Set β), (fun (x : β) => 0 +ᵥ x) '' x = x

theorem Set.addActionSet.proof_2 {α : Type u_2} {β : Type u_1} [AddMonoid α] [AddAction α β] : ∀ (x x_1 : α) (x_2 : Set β), (fun (x_3 : β) => x + x_1 +ᵥ x_3) '' x_2 = (fun (x_3 : β) => x +ᵥ x_3) '' ((fun (x : β) => x_1 +ᵥ x) '' x_2)

def Set.addActionSet {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] : AddAction α (Set β)

An additive action of an additive monoid on a type β gives an additive action on Set β.

Equations

• Set.addActionSet = AddAction.mk ⋯ ⋯

def Set.mulActionSet {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] : MulAction α (Set β)

A multiplicative action of a monoid on a type β gives a multiplicative action on Set β.

Equations

• Set.mulActionSet = MulAction.mk ⋯ ⋯

def Set.smulZeroClassSet {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] : SMulZeroClass α (Set β)

If scalar multiplication by elements of α sends (0 : β) to zero, then the same is true for (0 : Set β).

Equations

• Set.smulZeroClassSet = SMulZeroClass.mk ⋯

def Set.distribSMulSet {α : Type u_2} {β : Type u_3} [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Set β)

If the scalar multiplication (· • ·) : α → β → β is distributive, then so is (· • ·) : α → Set β → Set β.

Equations

• Set.distribSMulSet = DistribSMul.mk ⋯

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 β.

Equations

• Set.distribMulActionSet = DistribMulAction.mk ⋯ ⋯

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 β.

Equations

• Set.mulDistribMulActionSet = MulDistribMulAction.mk ⋯ ⋯

instance Set.instNoZeroSMulDivisors {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Set α) (Set β)

Equations

• ⋯ = ⋯

instance Set.noZeroSMulDivisors_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Set β)

Equations

• ⋯ = ⋯

instance Set.instNoZeroDivisors {α : Type u_2} [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors (Set α)

Equations

• ⋯ = ⋯

instance Set.vsub {α : Type u_2} {β : Type u_3} [VSub α β] : VSub (Set α) (Set β)

Equations

• Set.vsub = { vsub := Set.image2 fun (x x_1 : β) => x -ᵥ x_1 }

@[simp]

theorem Set.image2_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : Set.image2 VSub.vsub s t = s -ᵥ t

theorem Set.image_vsub_prod {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (fun (x : β × β) => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t

theorem Set.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {a : α} : a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a

theorem Set.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {b : β} {c : β} (hb : b ∈ s) (hc : c ∈ t) : b -ᵥ c ∈ s -ᵥ t

@[simp]

theorem Set.empty_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (t : Set β) : ∅ -ᵥ t = ∅

@[simp]

theorem Set.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) : s -ᵥ ∅ = ∅

@[simp]

theorem Set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty

theorem Set.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty → t.Nonempty

@[simp]

theorem Set.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (b : β) : s -ᵥ {b} = (fun (x : β) => x -ᵥ b) '' s

@[simp]

theorem Set.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (t : Set β) (b : β) : {b} -ᵥ t = (fun (x : β) => b -ᵥ x) '' t

@[simp]

theorem Set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] {b : β} {c : β} : {b} -ᵥ {c} = {b -ᵥ c}

theorem Set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂

theorem Set.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂

theorem Set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t

theorem Set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {u : Set α} : s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u

theorem Set.vsub_self_mono {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t

theorem Set.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)

theorem Set.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)

theorem Set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)

theorem Set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)

theorem Set.inter_vsub_union_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} : s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)

theorem Set.union_vsub_inter_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} : s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)

theorem Set.iUnion_vsub_left_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : ⋃ a ∈ s, (fun (x : β) => a -ᵥ x) '' t = s -ᵥ t

theorem Set.iUnion_vsub_right_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : ⋃ a ∈ t, (fun (x : β) => x -ᵥ a) '' s = s -ᵥ t

theorem Set.iUnion_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ι → Set β) (t : Set β) : (⋃ (i : ι), s i) -ᵥ t = ⋃ (i : ι), s i -ᵥ t

theorem Set.vsub_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ι → Set β) : s -ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s -ᵥ t i

theorem Set.iUnion₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : (i : ι) → κ i → Set β) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) -ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j -ᵥ t

theorem Set.vsub_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ i → Set β) : s -ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s -ᵥ t i j

theorem Set.iInter_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ι → Set β) (t : Set β) : (⋂ (i : ι), s i) -ᵥ t ⊆ ⋂ (i : ι), s i -ᵥ t

theorem Set.vsub_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ι → Set β) : s -ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s -ᵥ t i

theorem Set.iInter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : (i : ι) → κ i → Set β) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) -ᵥ t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j -ᵥ t

theorem Set.vsub_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ i → Set β) : s -ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s -ᵥ t i j

theorem Set.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] (f : β → γ) (a : α) (s : Set β) : (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → f '' (a +ᵥ s) = a +ᵥ f '' s

theorem Set.image_smul_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Set β) : (∀ (b : β), f (a • b) = a • f b) → f '' (a • s) = a • f '' s

theorem Set.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (a +ᵥ s) = f a +ᵥ ⇑f '' s

theorem Set.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (a : α) (s : Set α) : ⇑f '' (a • s) = f a • ⇑f '' s

theorem Set.op_vadd_set_vadd_eq_vadd_vadd_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd αᵃᵒᵖ β] [VAdd β γ] [VAdd α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), AddOpposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)) : AddOpposite.op a +ᵥ s +ᵥ t = s +ᵥ (a +ᵥ t)

theorem Set.op_smul_set_smul_eq_smul_smul_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c) : (MulOpposite.op a • s) • t = s • a • t

theorem Set.smul_zero_subset {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] (s : Set α) : s • 0 ⊆ 0

theorem Set.Nonempty.smul_zero {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {s : Set α} (hs : s.Nonempty) : s • 0 = 0

theorem Set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} (h : 0 ∈ t) : 0 ∈ a • t

theorem Set.zero_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [Zero β] [SMulZeroClass α β] {t : Set β} {a : α} [Zero α] [NoZeroSMulDivisors α β] (ha : a ≠ 0) : 0 ∈ a • t ↔ 0 ∈ t

Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β) because 0 * ∅ ≠ 0.

theorem Set.zero_smul_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] (t : Set β) : 0 • t ⊆ 0

theorem Set.Nonempty.zero_smul {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {t : Set β} (ht : t.Nonempty) : 0 • t = 0

@[simp]

theorem Set.zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {s : Set β} (h : s.Nonempty) : 0 • s = 0

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 β) : 0 • s ⊆ 0

theorem Set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] (s : Set β) : (0 • s).Subsingleton

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 ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

theorem Set.op_vadd_set_add_eq_add_vadd_set {α : Type u_2} [AddSemigroup α] (a : α) (s : Set α) (t : Set α) : AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)

theorem Set.op_smul_set_mul_eq_mul_smul_set {α : Type u_2} [Semigroup α] (a : α) (s : Set α) (t : Set α) : MulOpposite.op a • s * t = s * a • t

theorem Set.pairwiseDisjoint_vadd_iff {α : Type u_2} [Add α] [IsLeftCancelAdd α] {s : Set α} {t : Set α} : (s.PairwiseDisjoint fun (x : α) => x +ᵥ t) ↔ Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)

theorem Set.pairwiseDisjoint_smul_iff {α : Type u_2} [Mul α] [IsLeftCancelMul α] {s : Set α} {t : Set α} : (s.PairwiseDisjoint fun (x : α) => x • t) ↔ Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)

@[simp]

theorem Set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} {x : β} : a +ᵥ x ∈ a +ᵥ s ↔ x ∈ s

@[simp]

theorem Set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} {x : β} : a • x ∈ a • s ↔ x ∈ s

theorem Set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} : x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A

theorem Set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} : x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem Set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {a : α} {x : β} : x ∈ -a +ᵥ A ↔ a +ᵥ x ∈ A

theorem Set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {a : α} {x : β} : x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem Set.preimage_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) : (fun (x : β) => a +ᵥ x) ⁻¹' t = -a +ᵥ t

theorem Set.preimage_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) : (fun (x : β) => a • x) ⁻¹' t = a⁻¹ • t

theorem Set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] (a : α) (t : Set β) : (fun (x : β) => -a +ᵥ x) ⁻¹' t = a +ᵥ t

theorem Set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] (a : α) (t : Set β) : (fun (x : β) => a⁻¹ • x) ⁻¹' t = a • t

@[simp]

theorem Set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} : a +ᵥ A ⊆ a +ᵥ B ↔ A ⊆ B

@[simp]

theorem Set.set_smul_subset_set_smul_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} : a • A ⊆ a • B ↔ A ⊆ B

theorem Set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} : a +ᵥ A ⊆ B ↔ A ⊆ -a +ᵥ B

theorem Set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem Set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {A : Set β} {B : Set β} {a : α} : A ⊆ a +ᵥ B ↔ -a +ᵥ A ⊆ B

theorem Set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {A : Set β} {B : Set β} {a : α} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem Set.vadd_set_inter {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} : a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)

theorem Set.smul_set_inter {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} : a • (s ∩ t) = a • s ∩ a • t

theorem Set.vadd_set_iInter {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {ι : Type u_5} (a : α) (t : ι → Set β) : a +ᵥ ⋂ (i : ι), t i = ⋂ (i : ι), a +ᵥ t i

theorem Set.smul_set_iInter {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {ι : Type u_5} (a : α) (t : ι → Set β) : a • ⋂ (i : ι), t i = ⋂ (i : ι), a • t i

theorem Set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} : a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)

theorem Set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} : a • (s \ t) = a • s \ a • t

theorem Set.vadd_set_symmDiff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} : a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)

theorem Set.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} : a • symmDiff s t = symmDiff (a • s) (a • t)

@[simp]

theorem Set.vadd_set_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {a : α} : a +ᵥ Set.univ = Set.univ

@[simp]

theorem Set.smul_set_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {a : α} : a • Set.univ = Set.univ

@[simp]

theorem Set.vadd_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set α} (hs : s.Nonempty) : s +ᵥ Set.univ = Set.univ

abbrev Set.vadd_univ.match_1 {α : Type u_1} {s : Set α} (motive : s.Nonempty → Prop) : ∀ (hs : s.Nonempty), (∀ (a : α) (ha : a ∈ s), motive ⋯) → motive hs

Equations

• ⋯ = ⋯

@[simp]

theorem Set.smul_univ {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set α} (hs : s.Nonempty) : s • Set.univ = Set.univ

theorem Set.vadd_set_compl {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {a : α} : a +ᵥ sᶜ = (a +ᵥ s)ᶜ

theorem Set.smul_set_compl {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {a : α} : a • sᶜ = (a • s)ᶜ

theorem Set.vadd_inter_ne_empty_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : α} : (x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a + -b = x

theorem Set.smul_inter_ne_empty_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

theorem Set.vadd_inter_ne_empty_iff' {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : α} : (x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a - b = x

theorem Set.smul_inter_ne_empty_iff' {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ t ∧ b ∈ s) ∧ a / b = x

theorem Set.op_vadd_inter_ne_empty_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} {x : αᵃᵒᵖ} : (x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ -a + b = AddOpposite.unop x

theorem Set.op_smul_inter_ne_empty_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} {x : αᵐᵒᵖ} : x • s ∩ t ≠ ∅ ↔ ∃ (a : α) (b : α), (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x

@[simp]

theorem Set.iUnion_neg_vadd {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : ⋃ (g : α), -g +ᵥ s = ⋃ (g : α), g +ᵥ s

@[simp]

theorem Set.iUnion_inv_smul {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : ⋃ (g : α), g⁻¹ • s = ⋃ (g : α), g • s

theorem Set.iUnion_vadd_eq_setOf_exists {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : ⋃ (g : α), g +ᵥ s = {a : β | ∃ (g : α), g +ᵥ a ∈ s}

theorem Set.iUnion_smul_eq_setOf_exists {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : ⋃ (g : α), g • s = {a : β | ∃ (g : α), g • a ∈ s}

@[simp]

theorem Set.neg_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) : -(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s

@[simp]

theorem Set.inv_smul_set_distrib {α : Type u_2} [Group α] (a : α) (s : Set α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

theorem Set.neg_op_vadd_set_distrib {α : Type u_2} [AddGroup α] (a : α) (s : Set α) : -(AddOpposite.op a +ᵥ s) = -a +ᵥ -s

@[simp]

theorem Set.inv_op_smul_set_distrib {α : Type u_2} [Group α] (a : α) (s : Set α) : (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹

@[simp]

theorem Set.vadd_set_disjoint_iff {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} {t : Set β} {a : α} : Disjoint (a +ᵥ s) (a +ᵥ t) ↔ Disjoint s t

@[simp]

theorem Set.smul_set_disjoint_iff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} : Disjoint (a • s) (a • t) ↔ Disjoint s t

@[simp]

theorem Set.smul_mem_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : a • x ∈ a • A ↔ x ∈ A

theorem Set.mem_smul_set_iff_inv_smul_mem₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A

theorem Set.mem_inv_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (A : Set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A

theorem Set.preimage_smul₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (t : Set β) : (fun (x : β) => a • x) ⁻¹' t = a⁻¹ • t

theorem Set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (t : Set β) : (fun (x : β) => a⁻¹ • x) ⁻¹' t = a • t

@[simp]

theorem Set.set_smul_subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A : Set β} {B : Set β} : a • A ⊆ a • B ↔ A ⊆ B

theorem Set.set_smul_subset_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A : Set β} {B : Set β} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B

theorem Set.subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {A : Set β} {B : Set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B

theorem Set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t

theorem Set.smul_set_sdiff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t

theorem Set.smul_set_symmDiff₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a ≠ 0) : a • symmDiff s t = symmDiff (a • s) (a • t)

theorem Set.smul_set_univ₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : a • Set.univ = Set.univ

theorem Set.smul_univ₀ {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : ¬s ⊆ 0) : s • Set.univ = Set.univ

theorem Set.smul_univ₀' {α : Type u_2} {β : Type u_3} [GroupWithZero α] [MulAction α β] {s : Set α} (hs : s.Nontrivial) : s • Set.univ = Set.univ

@[simp]

theorem Set.inv_zero {α : Type u_2} [GroupWithZero α] : 0⁻¹ = 0

@[simp]

theorem Set.inv_smul_set_distrib₀ {α : Type u_2} [GroupWithZero α] (a : α) (s : Set α) : (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹

@[simp]

theorem Set.inv_op_smul_set_distrib₀ {α : Type u_2} [GroupWithZero α] (a : α) (s : Set α) : (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹

@[simp]

theorem Set.smul_set_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] (a : α) (t : Set β) : a • -t = -(a • t)

@[simp]

theorem Set.smul_neg {α : Type u_2} {β : Type u_3} [Monoid α] [AddGroup β] [DistribMulAction α β] (s : Set α) (t : Set β) : s • -t = -(s • t)

theorem Set.add_smul_subset {α : Type u_2} {β : Type u_3} [Semiring α] [AddCommMonoid β] [Module α β] (a : α) (b : α) (s : Set β) : (a + b) • s ⊆ a • s + b • s

@[simp]

theorem Set.neg_smul_set {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] (a : α) (t : Set β) : -a • t = -(a • t)

@[simp]

theorem Set.neg_smul {α : Type u_2} {β : Type u_3} [Ring α] [AddCommGroup β] [Module α β] (s : Set α) (t : Set β) : -s • t = -(s • t)