Pointwise scalar operations of sets

This file defines pointwise scalar-flavored 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 division, set of all x /ₛ y where x ∈ s and y ∈ t. Available in multiplicative torsors.
• 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. As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].

Appropriate definitions and results are also transported to the additive theory via to_additive.

Implementation notes

• The following expressions are considered in simp-normal form in a group: (fun h ↦ h * g) ⁻¹' s, (fun h ↦ g * h) ⁻¹' s, (fun h ↦ h * g⁻¹) ⁻¹' s, (fun h ↦ g⁻¹ * h) ⁻¹' s, s * t, s⁻¹, (1 : Set _) (and similarly for additive variants). Expressions equal to one of these will be simplified.
• We put all instances in the scope 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 scope to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp).

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

Translation/scaling of sets

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Set.smul = { smul := Set.image2 fun (x1 : α) (x2 : β) => x1 • x2 }

@[instance_reducible]

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 (x1 : α) (x2 : β) => x1 +ᵥ x2 }

@[simp]

theorem Set.image2_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : image2 (fun (x1 : α) (x2 : β) => x1 • x2) s t = s • t

@[simp]

theorem Set.image2_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : image2 (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) 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.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.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {b : β} : b ∈ s • t ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : β), y ∈ t ∧ x • y = b

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

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

@[simp]

theorem Set.vadd_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ 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.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s +ᵥ t).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_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty → s.Nonempty

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

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

@[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.vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {b : β} : s +ᵥ {b} = (fun (x : α) => x +ᵥ b) '' s

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Set.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ s₂ : Set α} {t₁ 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₁ s₂ : Set α} {t₁ 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₁ s₂ : Set α} {t₁ t₂ : Set β} : (s₁ ∪ s₂) +ᵥ t₁ ∩ t₂ ⊆ (s₁ +ᵥ 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

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.image_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} : (fun (x : β) => a • x) '' t = a • t

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

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.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.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} {b : β} : b ∈ s → a • b ∈ a • s

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

@[simp]

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

@[simp]

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

@[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_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : a +ᵥ s = ∅ ↔ s = ∅

@[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_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : (a +ᵥ s).Nonempty ↔ s.Nonempty

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem Set.smul_set_insert {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s)

theorem Set.vadd_set_insert {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (b : β) (s : Set β) : a +ᵥ insert b s = insert (a +ᵥ b) (a +ᵥ s)

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

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

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

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

theorem Set.smul_set_pi_of_surjective {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → SMul M (π i)] (c : M) (I : Set ι) (s : (i : ι) → Set (π i)) (hsurj : ∀ (i : ι), ¬i ∈ I → Function.Surjective fun (x : π i) => c • x) : c • I.pi s = I.pi (c • s)

theorem Set.vadd_set_pi_of_surjective {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → VAdd M (π i)] (c : M) (I : Set ι) (s : (i : ι) → Set (π i)) (hsurj : ∀ (i : ι), ¬i ∈ I → Function.Surjective fun (x : π i) => c +ᵥ x) : c +ᵥ I.pi s = I.pi (c +ᵥ s)

theorem Set.smul_set_univ_pi {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → SMul M (π i)] (c : M) (s : (i : ι) → Set (π i)) : c • univ.pi s = univ.pi (c • s)

theorem Set.vadd_set_univ_pi {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → VAdd M (π i)] (c : M) (s : (i : ι) → Set (π i)) : c +ᵥ univ.pi s = univ.pi (c +ᵥ s)

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

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

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

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

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

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

@[instance_reducible]

instance Set.sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] : SDiv (Set α) (Set β)

Equations

• Set.sdiv = { sdiv := Set.image2 fun (x1 x2 : β) => x1 /ₛ x2 }

@[instance_reducible]

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

Equations

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

@[simp]

theorem Set.image2_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : image2 (fun (x1 x2 : β) => x1 /ₛ x2) s t = s /ₛ t

@[simp]

theorem Set.image2_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s t : Set β} : image2 (fun (x1 x2 : β) => x1 -ᵥ x2) s t = s -ᵥ t

theorem Set.image_sdiv_prod {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : (fun (x : β × β) => x.1 /ₛ x.2) '' s ×ˢ t = s /ₛ t

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

theorem Set.mem_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} {a : α} : a ∈ s /ₛ t ↔ ∃ (x : β), x ∈ s ∧ ∃ (y : β), y ∈ t ∧ x /ₛ y = a

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

theorem Set.sdiv_mem_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} {b c : β} (hb : b ∈ s) (hc : c ∈ t) : b /ₛ c ∈ s /ₛ t

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

@[simp]

theorem Set.empty_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] (t : Set β) : ∅ /ₛ t = ∅

@[simp]

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

@[simp]

theorem Set.sdiv_empty {α : Type u_2} {β : Type u_3} [SDiv α β] (s : Set β) : s /ₛ ∅ = ∅

@[simp]

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

@[simp]

theorem Set.sdiv_eq_empty {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : s /ₛ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

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

@[simp]

theorem Set.sdiv_nonempty {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : (s /ₛ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

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

theorem Set.Nonempty.sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : s.Nonempty → t.Nonempty → (s /ₛ t).Nonempty

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

theorem Set.Nonempty.of_sdiv_left {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : (s /ₛ t).Nonempty → s.Nonempty

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

theorem Set.Nonempty.of_sdiv_right {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : (s /ₛ t).Nonempty → t.Nonempty

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

@[simp]

theorem Set.sdiv_singleton {α : Type u_2} {β : Type u_3} [SDiv α β] (s : Set β) (b : β) : s /ₛ {b} = (fun (x : β) => x /ₛ b) '' s

@[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_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] (t : Set β) (b : β) : {b} /ₛ t = (fun (x : β) => b /ₛ x) '' t

@[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_sdiv_singleton {α : Type u_2} {β : Type u_3} [SDiv α β] {b c : β} : {b} /ₛ {c} = {b /ₛ c}

@[simp]

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

theorem Set.sdiv_subset_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t₁ t₂ : Set β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ /ₛ t₁ ⊆ s₂ /ₛ t₂

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

theorem Set.sdiv_subset_sdiv_left {α : Type u_2} {β : Type u_3} [SDiv α β] {s t₁ t₂ : Set β} : t₁ ⊆ t₂ → s /ₛ t₁ ⊆ s /ₛ t₂

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

theorem Set.sdiv_subset_sdiv_right {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t : Set β} : s₁ ⊆ s₂ → s₁ /ₛ t ⊆ s₂ /ₛ t

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

theorem Set.sdiv_subset_iff {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} {u : Set α} : s /ₛ t ⊆ u ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ t → x /ₛ y ∈ u

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

theorem Set.sdiv_self_mono {α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} (h : s ⊆ t) : s /ₛ s ⊆ t /ₛ t

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

theorem Set.union_sdiv {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t : Set β} : s₁ ∪ s₂ /ₛ t = s₁ /ₛ t ∪ (s₂ /ₛ t)

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

theorem Set.sdiv_union {α : Type u_2} {β : Type u_3} [SDiv α β] {s t₁ t₂ : Set β} : s /ₛ (t₁ ∪ t₂) = s /ₛ t₁ ∪ (s /ₛ t₂)

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

theorem Set.inter_sdiv_subset {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t : Set β} : s₁ ∩ s₂ /ₛ t ⊆ (s₁ /ₛ t) ∩ (s₂ /ₛ t)

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

theorem Set.sdiv_inter_subset {α : Type u_2} {β : Type u_3} [SDiv α β] {s t₁ t₂ : Set β} : s /ₛ t₁ ∩ t₂ ⊆ (s /ₛ t₁) ∩ (s /ₛ t₂)

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

theorem Set.inter_sdiv_union_subset_union {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t₁ t₂ : Set β} : s₁ ∩ s₂ /ₛ (t₁ ∪ t₂) ⊆ s₁ /ₛ t₁ ∪ (s₂ /ₛ t₂)

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

theorem Set.union_sdiv_inter_subset_union {α : Type u_2} {β : Type u_3} [SDiv α β] {s₁ s₂ t₁ 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₁ s₂ t₁ t₂ : Set β} : s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)

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