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.image_smul_prod {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (fun x => x.fst • x.snd) '' s ×ˢ t = s • t

theorem Set.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {b : β} : b ∈ s +ᵥ t ↔ ∃ x y, 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 y, 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 β} : 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_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 : α), a ∈ s → ∀ (b : β), 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 : α), a ∈ s → ∀ (b : β), 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 : α) (_ : a ∈ s), a +ᵥ t = s +ᵥ t

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

theorem Set.iUnion_vadd_right_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : ⋃ (a : β) (_ : 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 : β) (_ : 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 : α) (_ : a ∈ s), a +ᵥ t = s +ᵥ t

@[simp]

theorem Set.iUnion_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (t : Set β) : ⋃ (a : α) (_ : 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, 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, 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 : α} : 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

@[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_Union {α : 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_Union {α : 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 : α} : 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.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 : α) (_ : a ∈ t), AddOpposite.op a +ᵥ s = s + t

@[simp]

theorem Set.iUnion_op_smul_set {α : Type u_2} [Mul α] (s : Set α) (t : Set α) : ⋃ (a : α) (_ : 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 : α), 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 : α), 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 : α), 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 : α), b ∈ t → MulOpposite.op b • s ⊆ u

abbrev Set.range_vadd_range.match_1 {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4} [VAdd α β] (b : ι → α) (c : κ → β) (_x : β) (motive : (∃ x y, x ∈ Set.range b ∧ y ∈ Set.range c ∧ x +ᵥ y = _x) → Prop) : (x : ∃ x y, x ∈ Set.range b ∧ y ∈ Set.range c ∧ x +ᵥ y = _x) → ((_p : α) → (_q : β) → (i : ι) → (hi : b i = _p) → (j : κ) → (hj : c j = _q) → (hpq : _p +ᵥ _q = _x) → motive (_ : ∃ x y, x ∈ Set.range b ∧ y ∈ Set.range c ∧ x +ᵥ y = _x)) → motive x

Equations

• One or more equations did not get rendered due to their size.

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.fst +ᵥ c p.snd

abbrev Set.range_vadd_range.match_2 {α : Type u_4} {β : Type u_1} {ι : Type u_2} {κ : Type u_3} [VAdd α β] (b : ι → α) (c : κ → β) (_x : β) (motive : (_x ∈ Set.range fun p => b p.fst +ᵥ c p.snd) → Prop) : (x : _x ∈ Set.range fun p => b p.fst +ᵥ c p.snd) → ((i : ι) → (j : κ) → (h : (fun p => b p.fst +ᵥ c p.snd) (i, j) = _x) → motive (_ : ∃ y, (fun p => b p.fst +ᵥ c p.snd) y = _x)) → motive x

Equations

• One or more equations did not get rendered due to their size.

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.fst • c p.snd

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

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 γ)

Equations

• @Set.vaddCommClass_set = @Set.vaddCommClass_set.proof_1

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

Equations

• @Set.smulCommClass_set = @Set.smulCommClass_set.proof_1

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

Equations

• @Set.vaddCommClass_set' = @Set.vaddCommClass_set'.proof_1

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 γ)

Equations

• @Set.smulCommClass_set' = @Set.smulCommClass_set'.proof_1

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 γ)

Equations

• @Set.vaddCommClass_set'' = @Set.vaddCommClass_set''.proof_1

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

Equations

• @Set.smulCommClass_set'' = @Set.smulCommClass_set''.proof_1

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

Equations

• @Set.vaddCommClass = @Set.vaddCommClass.proof_1

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 γ)

Equations

• @Set.smulCommClass = @Set.smulCommClass.proof_1

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

Equations

• @Set.vAddAssocClass = @Set.vAddAssocClass.proof_1

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 γ)

Equations

• @Set.isScalarTower = @Set.isScalarTower.proof_1

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 γ)

Equations

• @Set.vAddAssocClass' = @Set.vAddAssocClass'.proof_1

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

Equations

• @Set.isScalarTower' = @Set.isScalarTower'.proof_1

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

Equations

• @Set.vAddAssocClass'' = @Set.vAddAssocClass''.proof_1

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 γ)

Equations

• @Set.isScalarTower'' = @Set.isScalarTower''.proof_1

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

Equations

• @Set.isCentralVAdd = @Set.isCentralVAdd.proof_1

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

Equations

• @Set.isCentralScalar = @Set.isCentralScalar.proof_1

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

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

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

Equations

• @Set.instNoZeroSMulDivisorsSetSetZeroZeroSmul = @Set.instNoZeroSMulDivisorsSetSetZeroZeroSmul.proof_1

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

Equations

• @Set.noZeroSMulDivisors_set = @Set.noZeroSMulDivisors_set.proof_1

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

Equations

• @Set.instNoZeroDivisorsSetMulZero = @Set.instNoZeroDivisorsSetMulZero.proof_1

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.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t

theorem Set.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {a : α} : a ∈ s -ᵥ t ↔ ∃ x y, 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 β} : 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

@[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 x_1 => x -ᵥ x_1) b '' 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 : β), x ∈ s → ∀ (y : β), 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 : β) (_ : a ∈ s), (fun x x_1 => x -ᵥ x_1) a '' t = s -ᵥ t

theorem Set.iUnion_vsub_right_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : ⋃ (a : β) (_ : 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 β] [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 β] [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

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

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

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

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

theorem Set.zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMulWithZero α β] {s : Set β} (h : Set.Nonempty s) : 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 β) : Set.Subsingleton (0 • s)

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

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) : 0 ∈ a • t ↔ 0 ∈ t

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} [AddLeftCancelSemigroup α] {s : Set α} {t : Set α} : (Set.PairwiseDisjoint s fun x => x +ᵥ t) ↔ Set.InjOn (fun p => p.fst + p.snd) (s ×ˢ t)

theorem Set.pairwiseDisjoint_smul_iff {α : Type u_2} [LeftCancelSemigroup α] {s : Set α} {t : Set α} : (Set.PairwiseDisjoint s fun x => x • t) ↔ Set.InjOn (fun p => p.fst * p.snd) (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_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 +ᵥ s ∆ t = (a +ᵥ s) ∆ (a +ᵥ t)

theorem Set.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} : a • s ∆ t = (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

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.vadd_univ {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set α} (hs : Set.Nonempty s) : s +ᵥ Set.univ = Set.univ

@[simp]

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

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.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 • s ∆ t = (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 : Set.Nontrivial s) : s • Set.univ = Set.univ

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