doc-next-gen

Mathlib.Algebra.Group.Pointwise.Set.Scalar

Module docstring

{"# 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 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 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.

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction ","### Translation/scaling of sets "}

Set.smulSet definition
[SMul α β] : SMul α (Set β)
Full source 
/-- The dilation of set `x • s` is defined as `{x • y | y ∈ s}` in locale `Pointwise`. -/
@[to_additive
"The translation of set `x +ᵥ s` is defined as `{x +ᵥ y | y ∈ s}` in locale `Pointwise`."]
protected def smulSet [SMul α β] : SMul α (Set β) where smul a := image (a • ·)
Scalar dilation of a set
Informal description
Given a scalar multiplication operation `•` between types `α` and `β`, the dilation of a set `s ⊆ β` by a scalar `a ∈ α` is defined as the set `{a • y | y ∈ s}`.
Set.smul definition
[SMul α β] : SMul (Set α) (Set β)
Full source 
/-- The pointwise scalar multiplication of sets `s • t` is defined as `{x • y | x ∈ s, y ∈ t}` in
locale `Pointwise`. -/
@[to_additive
"The pointwise scalar addition of sets `s +ᵥ t` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale
`Pointwise`."]
protected def smul [SMul α β] : SMul (Set α) (Set β) where smul := image2 (· • ·)
Pointwise scalar multiplication of sets
Informal description
Given a scalar multiplication operation `•` between types `α` and `β`, the pointwise scalar multiplication of sets `s ⊆ α` and `t ⊆ β` is defined as the set `{x • y | x ∈ s, y ∈ t}`.
Set.image2_smul theorem
: image2 (· • ·) s t = s • t
Full source 
@[to_additive (attr := simp)] lemma image2_smul : image2 (· • ·) s t = s • t := rfl
Image of Scalar Multiplication Equals Pointwise Product of Sets
Informal description
For any sets $s$ and $t$ and scalar multiplication operation $\cdot$, the image of the scalar multiplication function applied to $s$ and $t$ is equal to the pointwise scalar product $s \cdot t$. That is, \[ \text{image2}(\cdot, s, t) = s \cdot t. \]
Set.image_smul_prod theorem
: (fun x : α × β ↦ x.fst • x.snd) '' s ×ˢ t = s • t
Full source 
@[to_additive vadd_image_prod]
lemma image_smul_prod : (fun x : α × β ↦ x.fst • x.snd) '' s ×ˢ t = s • t := image_prod _
Image of Scalar Multiplication on Cartesian Product Equals Pointwise Product of Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \times \beta \to \gamma$, the image of the Cartesian product $s \times t$ under the scalar multiplication function $(x,y) \mapsto x \cdot y$ is equal to the pointwise scalar product $s \cdot t$. That is, $$ \{(x \cdot y) \mid (x,y) \in s \times t\} = s \cdot t. $$
Set.mem_smul theorem
: b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b
Full source 
@[to_additive] lemma mem_smul : b ∈ s • tb ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b := Iff.rfl
Membership in Pointwise Scalar Product of Sets
Informal description
An element $b$ belongs to the pointwise scalar product $s \cdot t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$ if and only if there exist elements $x \in s$ and $y \in t$ such that $x \cdot y = b$.
Set.smul_mem_smul theorem
: a ∈ s → b ∈ t → a • b ∈ s • t
Full source 
@[to_additive] lemma smul_mem_smul : a ∈ s → b ∈ t → a • b ∈ s • t := mem_image2_of_mem
Membership in Pointwise Scalar Product of Sets
Informal description
For any elements $a \in s$ and $b \in t$, their scalar product $a \bullet b$ belongs to the pointwise scalar product set $s \bullet t$.
Set.empty_smul theorem
: (∅ : Set α) • t = ∅
Full source 
@[to_additive (attr := simp)] lemma empty_smul : (∅ : Set α) • t = ∅ := image2_empty_left
Empty Set Scalar Multiplication Property: $\emptyset \cdot t = \emptyset$
Informal description
For any set $t$ of elements in a type $\beta$, the pointwise scalar multiplication of the empty set (of type $\alpha$) with $t$ is the empty set, i.e., $\emptyset \cdot t = \emptyset$.
Set.smul_empty theorem
: s • (∅ : Set β) = ∅
Full source 
@[to_additive (attr := simp)] lemma smul_empty : s • (∅ : Set β) = ∅ := image2_empty_right
Scalar Multiplication of Set with Empty Set Yields Empty Set
Informal description
For any set $s$ in a type $\alpha$ with a scalar multiplication operation `•` to a type $\beta$, the pointwise scalar multiplication of $s$ with the empty set in $\beta$ is the empty set, i.e., $s \bullet \emptyset = \emptyset$.
Set.smul_eq_empty theorem
: s • t = ∅ ↔ s = ∅ ∨ t = ∅
Full source 
@[to_additive (attr := simp)] lemma smul_eq_empty : s • t = ∅ ↔ s = ∅ ∨ t = ∅ := image2_eq_empty_iff
Empty Scalar Product Criterion for Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\bullet : \alpha \to \beta \to \gamma$, the pointwise scalar product $s \bullet t$ is empty if and only if either $s$ is empty or $t$ is empty. That is, $s \bullet t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.
Set.smul_nonempty theorem
: (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Full source 
@[to_additive (attr := simp)]
lemma smul_nonempty : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := image2_nonempty_iff
Nonempty Criterion for Pointwise Scalar Product of Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\bullet : \alpha \to \beta \to \gamma$, the pointwise scalar product $s \bullet t$ is nonempty if and only if both $s$ and $t$ are nonempty.
Set.Nonempty.smul theorem
: s.Nonempty → t.Nonempty → (s • t).Nonempty
Full source 
@[to_additive] lemma Nonempty.smul : s.Nonempty → t.Nonempty → (s • t).Nonempty := .image2
Nonempty Sets Have Nonempty Scalar Product
Informal description
For any nonempty sets $s \subseteq \alpha$ and $t \subseteq \beta$, the pointwise scalar product $s \bullet t$ is also nonempty.
Set.Nonempty.of_smul_left theorem
: (s • t).Nonempty → s.Nonempty
Full source 
@[to_additive] lemma Nonempty.of_smul_left : (s • t).Nonempty → s.Nonempty := .of_image2_left
Nonemptiness of Left Set in Nonempty Scalar Product
Informal description
If the pointwise scalar product $s \bullet t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty, then the set $s$ is nonempty.
Set.Nonempty.of_smul_right theorem
: (s • t).Nonempty → t.Nonempty
Full source 
@[to_additive] lemma Nonempty.of_smul_right : (s • t).Nonempty → t.Nonempty := .of_image2_right
Nonemptiness of Scalar Product Implies Nonemptiness of Right Set
Informal description
If the pointwise scalar product $s \bullet t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty, then the set $t$ is nonempty.
Set.smul_singleton theorem
: s • ({ b } : Set β) = (· • b) '' s
Full source 
@[to_additive (attr := simp low+1)]
lemma smul_singleton : s • ({b} : Set β) = (· • b) '' s := image2_singleton_right
Pointwise Scalar Multiplication with Singleton Right Argument: $s \bullet \{b\} = \{x \bullet b \mid x \in s\}$
Informal description
For any set $s \subseteq \alpha$ and any singleton set $\{b\} \subseteq \beta$, the pointwise scalar multiplication $s \bullet \{b\}$ is equal to the image of $s$ under the function $\lambda x, x \bullet b$. In other words, $s \bullet \{b\} = \{x \bullet b \mid x \in s\}$.
Set.singleton_smul theorem
: ({ a } : Set α) • t = a • t
Full source 
@[to_additive (attr := simp low+1)]
lemma singleton_smul : ({a} : Set α) • t = a • t := image2_singleton_left
Pointwise scalar multiplication of a singleton set: $\{a\} \cdot t = a \cdot t$
Informal description
For any scalar $a \in \alpha$ and any set $t \subseteq \beta$, the pointwise scalar multiplication of the singleton set $\{a\}$ with $t$ is equal to the dilation of $t$ by $a$, i.e., $\{a\} \cdot t = \{a \cdot y \mid y \in t\}$.
Set.singleton_smul_singleton theorem
: ({ a } : Set α) • ({ b } : Set β) = {a • b}
Full source 
@[to_additive (attr := simp high)]
lemma singleton_smul_singleton : ({a} : Set α) • ({b} : Set β) = {a • b} := image2_singleton
Pointwise Scalar Multiplication of Singleton Sets: $\{a\} \bullet \{b\} = \{a \bullet b\}$
Informal description
For any elements $a \in \alpha$ and $b \in \beta$, the pointwise scalar multiplication of the singleton sets $\{a\}$ and $\{b\}$ is equal to the singleton set $\{a \bullet b\}$, i.e., $\{a\} \bullet \{b\} = \{a \bullet b\}$.
Set.smul_subset_smul theorem
: s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
Full source 
@[to_additive (attr := mono, gcongr)]
lemma smul_subset_smul : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂ := image2_subset
Monotonicity of Pointwise Scalar Multiplication with Respect to Subset Inclusion
Informal description
For any sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then the pointwise scalar product $s_1 \bullet t_1$ is a subset of $s_2 \bullet t_2$.
Set.smul_subset_smul_left theorem
: t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
Full source 
@[to_additive (attr := gcongr)]
lemma smul_subset_smul_left : t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂ := image2_subset_left
Left Monotonicity of Pointwise Scalar Multiplication with Respect to Right Subset Inclusion
Informal description
For any sets $t_1, t_2 \subseteq \beta$ and $s \subseteq \alpha$, if $t_1 \subseteq t_2$, then the pointwise scalar product $s \bullet t_1$ is a subset of $s \bullet t_2$.
Set.smul_subset_smul_right theorem
: s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
Full source 
@[to_additive (attr := gcongr)]
lemma smul_subset_smul_right : s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t := image2_subset_right
Right Monotonicity of Pointwise Scalar Multiplication with Respect to Subset Inclusion
Informal description
For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, if $s_1$ is a subset of $s_2$, then the pointwise product $s_1 \cdot t$ is a subset of $s_2 \cdot t$. In symbols: \[ s_1 \subseteq s_2 \implies s_1 \cdot t \subseteq s_2 \cdot t. \]
Set.smul_subset_iff theorem
: s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u
Full source 
@[to_additive] lemma smul_subset_iff : s • t ⊆ us • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u := image2_subset_iff
Subset condition for pointwise scalar multiplication of sets
Informal description
For any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, the pointwise product set $s \cdot t$ is a subset of $u$ if and only if for every $a \in s$ and $b \in t$, the product $a \cdot b$ belongs to $u$. In symbols: \[ s \cdot t \subseteq u \leftrightarrow \forall a \in s, \forall b \in t, a \cdot b \in u. \]
Set.union_smul theorem
: (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t
Full source 
@[to_additive] lemma union_smul : (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t := image2_union_left
Distributivity of Pointwise Scalar Multiplication over Union in First Argument: $(s_1 \cup s_2) \cdot t = s_1 \cdot t \cup s_2 \cdot t$
Informal description
For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, the pointwise product of the union $s_1 \cup s_2$ with $t$ equals the union of the pointwise products $s_1 \cdot t$ and $s_2 \cdot t$. That is, \[ (s_1 \cup s_2) \cdot t = (s_1 \cdot t) \cup (s_2 \cdot t). \]
Set.smul_union theorem
: s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
Full source 
@[to_additive] lemma smul_union : s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂ := image2_union_right
Distributivity of Pointwise Scalar Multiplication over Union in Second Argument: $s \cdot (t_1 \cup t_2) = s \cdot t_1 \cup s \cdot t_2$
Informal description
For any sets $s \subseteq \alpha$, $t_1, t_2 \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, the pointwise product of $s$ with the union $t_1 \cup t_2$ equals the union of the pointwise products $s \cdot t_1$ and $s \cdot t_2$. That is, \[ s \cdot (t_1 \cup t_2) = (s \cdot t_1) \cup (s \cdot t_2). \]
Set.inter_smul_subset theorem
: (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t
Full source 
@[to_additive]
lemma inter_smul_subset : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t := image2_inter_subset_left
Subset Property of Pointwise Scalar Multiplication over Intersection in First Argument
Informal description
For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, the pointwise product of the intersection $s_1 \cap s_2$ with $t$ is a subset of the intersection of the pointwise products $s_1 \cdot t$ and $s_2 \cdot t$. That is, \[ (s_1 \cap s_2) \cdot t \subseteq (s_1 \cdot t) \cap (s_2 \cdot t). \]
Set.smul_inter_subset theorem
: s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
Full source 
@[to_additive]
lemma smul_inter_subset : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂ := image2_inter_subset_right
Subset Property of Pointwise Scalar Multiplication over Intersection
Informal description
For any sets $s \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$ with a scalar multiplication operation $\cdot : \alpha \to \beta \to \gamma$, the pointwise product of $s$ with the intersection $t_1 \cap t_2$ is a subset of the intersection of the pointwise products $s \cdot t_1$ and $s \cdot t_2$. That is, \[ s \cdot (t_1 \cap t_2) \subseteq (s \cdot t_1) \cap (s \cdot t_2). \]
Set.inter_smul_union_subset_union theorem
: (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
Full source 
@[to_additive]
lemma inter_smul_union_subset_union : (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂ :=
  image2_inter_union_subset_union
Subset Property for Scalar Multiplication on Intersection-Union Pairs
Informal description
For any sets $s_1, s_2$ and $t_1, t_2$ in a type with a scalar multiplication operation, the pointwise scalar product of the intersection $s_1 \cap s_2$ with the union $t_1 \cup t_2$ is a subset of the union of the pointwise scalar products $s_1 \cdot t_1$ and $s_2 \cdot t_2$. In other words: $$(s_1 \cap s_2) \cdot (t_1 \cup t_2) \subseteq (s_1 \cdot t_1) \cup (s_2 \cdot t_2)$$ where $\cdot$ denotes the scalar multiplication operation.
Set.union_smul_inter_subset_union theorem
: (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
Full source 
@[to_additive]
lemma union_smul_inter_subset_union : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂ :=
  image2_union_inter_subset_union
Subset Property of Pointwise Product over Union and Intersection: $(s₁ \cup s₂) \cdot (t₁ \cap t₂) \subseteq s₁ \cdot t₁ \cup s₂ \cdot t₂$
Informal description
For any sets $s₁, s₂$ and $t₁, t₂$ in a type with a scalar multiplication operation, the pointwise product of the union $s₁ \cup s₂$ with the intersection $t₁ \cap t₂$ is a subset of the union of the pointwise products $s₁ \cdot t₁$ and $s₂ \cdot t₂$. That is, $$(s₁ \cup s₂) \cdot (t₁ \cap t₂) \subseteq s₁ \cdot t₁ \cup s₂ \cdot t₂.$$
Set.smul_set_subset_smul theorem
{s : Set α} : a ∈ s → a • t ⊆ s • t
Full source 
@[to_additive]
lemma smul_set_subset_smul {s : Set α} : a ∈ s → a • t ⊆ s • t := image_subset_image2_right
Scaled set is subset of pointwise product: $a \cdot t \subseteq s \cdot t$ when $a \in s$
Informal description
For any scalar $a$ in a set $s$ and any set $t$, the scaled set $a \cdot t$ is a subset of the pointwise product $s \cdot t$, where $\cdot$ denotes the scalar multiplication operation.
Set.image_smul theorem
: (fun x ↦ a • x) '' t = a • t
Full source 
@[to_additive] lemma image_smul : (fun x ↦ a • x) '' t = a • t := rfl
Image of Set under Scalar Multiplication Equals Scalar Multiplication of Set
Informal description
For any scalar $a$ and any set $t$, the image of $t$ under the function $x \mapsto a \cdot x$ is equal to the scalar multiplication of $t$ by $a$, i.e., $\{a \cdot x \mid x \in t\} = a \cdot t$.
Set.mem_smul_set theorem
: x ∈ a • t ↔ ∃ y, y ∈ t ∧ a • y = x
Full source 
@[to_additive] lemma mem_smul_set : x ∈ a • tx ∈ a • t ↔ ∃ y, y ∈ t ∧ a • y = x := Iff.rfl
Characterization of Membership in Scaled Set: $x \in a \cdot t$
Informal description
An element $x$ belongs to the scaled set $a \cdot t$ if and only if there exists an element $y \in t$ such that $a \cdot y = x$, where $\cdot$ denotes the scalar multiplication operation.
Set.smul_mem_smul_set theorem
: b ∈ s → a • b ∈ a • s
Full source 
@[to_additive] lemma smul_mem_smul_set : b ∈ s → a • b ∈ a • s := mem_image_of_mem _
Scalar multiplication preserves membership in scaled sets
Informal description
For any scalar $a$ and element $b$ in a set $s$, the scalar multiplication $a \cdot b$ belongs to the scaled set $a \cdot s$.
Set.smul_set_empty theorem
: a • (∅ : Set β) = ∅
Full source 
@[to_additive (attr := simp)] lemma smul_set_empty : a • (∅ : Set β) = ∅ := image_empty _
Dilation of Empty Set is Empty
Informal description
For any scalar $a$ in a type $\alpha$ with a scalar multiplication operation on a type $\beta$, the dilation of the empty set by $a$ is the empty set, i.e., $a \bullet \emptyset = \emptyset$.
Set.smul_set_eq_empty theorem
: a • s = ∅ ↔ s = ∅
Full source 
@[to_additive (attr := simp)] lemma smul_set_eq_empty : a • s = ∅ ↔ s = ∅ := image_eq_empty
Scalar Multiplication of Set is Empty iff Set is Empty
Informal description
For a scalar $a$ and a set $s$, the scalar multiplication $a \cdot s$ is empty if and only if $s$ is empty. In symbols: $$ a \cdot s = \emptyset \leftrightarrow s = \emptyset $$
Set.smul_set_nonempty theorem
: (a • s).Nonempty ↔ s.Nonempty
Full source 
@[to_additive (attr := simp)]
lemma smul_set_nonempty : (a • s).Nonempty ↔ s.Nonempty := image_nonempty
Nonempty Scalar Multiplication of Set Equivalence
Informal description
For any scalar $a$ and any set $s$, the set $a \bullet s$ is nonempty if and only if $s$ is nonempty. In symbols: $$ a \bullet s \neq \emptyset \iff s \neq \emptyset $$
Set.smul_set_singleton theorem
: a • ({ b } : Set β) = {a • b}
Full source 
@[to_additive (attr := simp)]
lemma smul_set_singleton : a • ({b} : Set β) = {a • b} := image_singleton
Scalar Dilation of Singleton Set: $a \bullet \{b\} = \{a \bullet b\}$
Informal description
For any scalar $a$ in a type $\alpha$ with a scalar multiplication operation $\bullet$ on a type $\beta$, and for any element $b \in \beta$, the dilation of the singleton set $\{b\}$ by $a$ is the singleton set $\{a \bullet b\}$.
Set.smul_set_mono theorem
: s ⊆ t → a • s ⊆ a • t
Full source 
@[to_additive (attr := gcongr)] lemma smul_set_mono : s ⊆ t → a • s ⊆ a • t := image_subset _
Scalar Multiplication Preserves Subset Relation: $a \bullet s \subseteq a \bullet t$ when $s \subseteq t$
Informal description
For any scalar $a$ and any subsets $s, t$ of a set, if $s \subseteq t$, then the scalar multiplication $a \bullet s$ is a subset of $a \bullet t$.
Set.smul_set_subset_iff theorem
: a • s ⊆ t ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ t
Full source 
@[to_additive]
lemma smul_set_subset_iff : a • s ⊆ ta • s ⊆ t ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ t :=
  image_subset_iff
Subset Criterion for Scalar Dilation: $a \cdot s \subseteq t \leftrightarrow \forall b \in s, a \cdot b \in t$
Informal description
For a scalar $a \in \alpha$ and sets $s \subseteq \beta$, $t \subseteq \beta$, the dilation $a \cdot s$ is a subset of $t$ if and only if for every element $b \in s$, the scaled element $a \cdot b$ belongs to $t$. In symbols: \[ a \cdot s \subseteq t \leftrightarrow \forall b \in s, a \cdot b \in t. \]
Set.smul_set_union theorem
: a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂
Full source 
@[to_additive]
lemma smul_set_union : a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂ :=
  image_union ..
Scalar Multiplication Distributes over Set Union: $a \cdot (t_1 \cup t_2) = (a \cdot t_1) \cup (a \cdot t_2)$
Informal description
For any scalar $a \in \alpha$ and any sets $t_1, t_2 \subseteq \beta$, the scalar multiplication of the union $t_1 \cup t_2$ by $a$ is equal to the union of the scalar multiplications of $t_1$ and $t_2$ by $a$, i.e., $$ a \cdot (t_1 \cup t_2) = (a \cdot t_1) \cup (a \cdot t_2). $$
Set.smul_set_insert theorem
(a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s)
Full source 
@[to_additive]
lemma smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s) :=
  image_insert_eq ..
Scalar Multiplication Distributes over Set Insertion: $a \cdot (\{b\} \cup s) = \{a \cdot b\} \cup (a \cdot s)$
Informal description
For any scalar $a \in \alpha$, element $b \in \beta$, and subset $s \subseteq \beta$, the scalar multiplication of the set $\{b\} \cup s$ by $a$ is equal to the union of $\{a \cdot b\}$ and the scalar multiplication of $s$ by $a$, i.e., $$ a \cdot (\{b\} \cup s) = \{a \cdot b\} \cup (a \cdot s). $$
Set.smul_set_inter_subset theorem
: a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂
Full source 
@[to_additive]
lemma smul_set_inter_subset : a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂ :=
  image_inter_subset ..
Scalar Multiplication Preserves Subset Relation on Intersections: $a \cdot (t_1 \cap t_2) \subseteq (a \cdot t_1) \cap (a \cdot t_2)$
Informal description
For any scalar $a$ and any sets $t_1, t_2$, the scalar multiplication of the intersection $t_1 \cap t_2$ by $a$ is a subset of the intersection of the scalar multiplications of $t_1$ and $t_2$ by $a$, i.e., $$ a \cdot (t_1 \cap t_2) \subseteq (a \cdot t_1) \cap (a \cdot t_2). $$
Set.Nonempty.smul_set theorem
: s.Nonempty → (a • s).Nonempty
Full source 
@[to_additive] lemma Nonempty.smul_set : s.Nonempty → (a • s).Nonempty := Nonempty.image _
Nonempty Set Preserved under Scalar Multiplication
Informal description
For any nonempty set $s$ in a type $\beta$ and any scalar $a$ in a type $\alpha$ with a scalar multiplication operation $\cdot : \alpha \times \beta \to \beta$, the dilated set $a \cdot s = \{a \cdot y \mid y \in s\}$ is also nonempty.
Set.smul_set_pi_of_surjective theorem
(c : M) (I : Set ι) (s : ∀ i, Set (π i)) (hsurj : ∀ i ∉ I, Function.Surjective (c • · : π i → π i)) : c • I.pi s = I.pi (c • s)
Full source 
@[to_additive]
theorem smul_set_pi_of_surjective (c : M) (I : Set ι) (s : ∀ i, Set (π i))
    (hsurj : ∀ i ∉ I, Function.Surjective (c • · : π i → π i)) : c • I.pi s = I.pi (c • s) :=
  piMap_image_pi hsurj s
Scalar Multiplication Commutes with Product Set under Surjectivity Condition
Informal description
Let $M$ be a type with a scalar multiplication operation $\cdot : M \times \pi_i \to \pi_i$ for each $i$ in an index set $\iota$. For a scalar $c \in M$, an index subset $I \subseteq \iota$, and a family of sets $s_i \subseteq \pi_i$ for each $i \in \iota$, if for every $i \notin I$ the function $x \mapsto c \cdot x$ is surjective on $\pi_i$, then the scalar multiplication of the product set $\prod_{i \in I} s_i$ by $c$ equals the product set $\prod_{i \in I} (c \cdot s_i)$. In symbols: $$ c \cdot \left( \prod_{i \in I} s_i \right) = \prod_{i \in I} (c \cdot s_i). $$
Set.smul_set_univ_pi theorem
(c : M) (s : ∀ i, Set (π i)) : c • univ.pi s = univ.pi (c • s)
Full source 
@[to_additive]
theorem smul_set_univ_pi (c : M) (s : ∀ i, Set (π i)) : c • univ.pi s = univ.pi (c • s) :=
  piMap_image_univ_pi _ s
Scalar Multiplication Commutes with Universal Product Set
Informal description
Let $M$ be a type with a scalar multiplication operation $\cdot : M \times \pi_i \to \pi_i$ for each $i$ in an index set $\iota$. For a scalar $c \in M$ and a family of sets $s_i \subseteq \pi_i$ for each $i \in \iota$, the scalar multiplication of the product set $\prod_{i \in \iota} s_i$ by $c$ equals the product set $\prod_{i \in \iota} (c \cdot s_i)$. In symbols: $$ c \cdot \left( \prod_{i \in \iota} s_i \right) = \prod_{i \in \iota} (c \cdot s_i). $$
Set.range_smul_range theorem
{ι κ : Type*} [SMul α β] (b : ι → α) (c : κ → β) : range b • range c = range fun p : ι × κ ↦ b p.1 • c p.2
Full source 
@[to_additive]
lemma range_smul_range {ι κ : Type*} [SMul α β] (b : ι → α) (c : κ → β) :
    range b • range c = range fun p : ι × κ ↦ b p.1 • c p.2 :=
  image2_range ..
Pointwise Scalar Multiplication of Ranges Equals Range of Pairwise Scalar Multiplication
Informal description
Let $\alpha$ and $\beta$ be types equipped with a scalar multiplication operation $\cdot : \alpha \to \beta \to \beta$. For any functions $b : \iota \to \alpha$ and $c : \kappa \to \beta$, the pointwise scalar multiplication of their ranges equals the range of the function mapping each pair $(i,j) \in \iota \times \kappa$ to $b(i) \cdot c(j)$. In symbols: $$ \mathrm{range}(b) \cdot \mathrm{range}(c) = \mathrm{range}(\lambda (i,j), b(i) \cdot c(j)) $$
Set.smul_set_range theorem
[SMul α β] {ι : Sort*} (a : α) (f : ι → β) : a • range f = range fun i ↦ a • f i
Full source 
@[to_additive]
lemma smul_set_range [SMul α β] {ι : Sort*} (a : α) (f : ι → β) :
    a • range f = range fun i ↦ a • f i :=
  (range_comp ..).symm
Scalar Multiplication of Range Equals Range of Scalar Multiplication
Informal description
Let $\alpha$ and $\beta$ be types with a scalar multiplication operation $\cdot : \alpha \to \beta \to \beta$, and let $a \in \alpha$ be a scalar. For any function $f : \iota \to \beta$, the scalar multiplication of the range of $f$ by $a$ is equal to the range of the function $\lambda i, a \cdot f(i)$. In symbols: $$ a \cdot \mathrm{range}(f) = \mathrm{range}(\lambda i, a \cdot f(i)) $$
Set.range_smul theorem
[SMul α β] {ι : Sort*} (a : α) (f : ι → β) : range (fun i ↦ a • f i) = a • range f
Full source 
@[to_additive] lemma range_smul [SMul α β] {ι : Sort*} (a : α) (f : ι → β) :
    range (fun i ↦ a • f i) = a • range f := (smul_set_range ..).symm
Range of Scalar Multiplication Equals Scalar Multiplication of Range
Informal description
Let $\alpha$ and $\beta$ be types equipped with a scalar multiplication operation $\cdot : \alpha \to \beta \to \beta$. For any scalar $a \in \alpha$ and any function $f : \iota \to \beta$, the range of the function $\lambda i, a \cdot f(i)$ is equal to the scalar multiplication of the range of $f$ by $a$. In symbols: $$ \mathrm{range}(\lambda i, a \cdot f(i)) = a \cdot \mathrm{range}(f) $$
Set.vsub instance
: VSub (Set α) (Set β)
Full source 
instance vsub : VSub (Set α) (Set β) where vsub := image2 (· -ᵥ ·)
Scalar Subtraction Operation on Sets
Informal description
For any types $\alpha$ and $\beta$ with a scalar subtraction operation $-ᵥ : \alpha \rightarrow \beta \rightarrow \beta$, the set of all elements of $\alpha$ can be equipped with a scalar subtraction operation on sets, where for sets $s, t \subseteq \beta$, the scalar subtraction $s -ᵥ t$ is defined as the set $\{x -ᵥ y \mid x \in s, y \in t\}$.
Set.image2_vsub theorem
: image2 (· -ᵥ ·) s t = s -ᵥ t
Full source 
@[simp] lemma image2_vsub : image2 (· -ᵥ ·) s t = s -ᵥ t := rfl
Image of Scalar Subtraction on Sets Equals Set Subtraction
Informal description
For any sets $s$ and $t$, the image of the scalar subtraction operation $-ᵥ$ applied pairwise to elements of $s$ and $t$ is equal to the scalar subtraction of the sets $s -ᵥ t$. That is, \[ \text{image2} (-ᵥ) s t = s -ᵥ t. \]
Set.image_vsub_prod theorem
: (fun x : β × β ↦ x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t
Full source 
lemma image_vsub_prod : (fun x : β × β ↦ x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t := image_prod _
Image of Cartesian Product under Scalar Subtraction Equals Set Subtraction
Informal description
For any sets $s, t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the scalar subtraction operation $(x,y) \mapsto x -ᵥ y$ is equal to the scalar subtraction set $s -ᵥ t$. That is, $$ \{(x -ᵥ y) \mid (x,y) \in s \times t\} = s -ᵥ t. $$
Set.mem_vsub theorem
: a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a
Full source 
lemma mem_vsub : a ∈ s -ᵥ ta ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a := Iff.rfl
Membership in Scalar Subtraction of Sets: $a \in s -ᵥ t \leftrightarrow \exists x \in s, \exists y \in t, x -ᵥ y = a$
Informal description
An element $a$ belongs to the scalar subtraction set $s -ᵥ t$ if and only if there exist elements $x \in s$ and $y \in t$ such that $x -ᵥ y = a$.
Set.vsub_mem_vsub theorem
(hb : b ∈ s) (hc : c ∈ t) : b -ᵥ c ∈ s -ᵥ t
Full source 
lemma vsub_mem_vsub (hb : b ∈ s) (hc : c ∈ t) : b -ᵥ cb -ᵥ c ∈ s -ᵥ t := mem_image2_of_mem hb hc
Closure of Scalar Subtraction under Set Membership
Informal description
For any elements $b \in s$ and $c \in t$, the scalar subtraction $b -ᵥ c$ belongs to the set $s -ᵥ t$.
Set.empty_vsub theorem
(t : Set β) : ∅ -ᵥ t = ∅
Full source 
@[simp] lemma empty_vsub (t : Set β) : ∅∅ -ᵥ t = ∅ := image2_empty_left
Empty Set Scalar Subtraction Property: $\emptyset -ᵥ t = \emptyset$
Informal description
For any set $t$ of elements of type $\beta$, the scalar subtraction of the empty set with $t$ is the empty set, i.e., $\emptyset -ᵥ t = \emptyset$.
Set.vsub_empty theorem
(s : Set β) : s -ᵥ ∅ = ∅
Full source 
@[simp] lemma vsub_empty (s : Set β) : s -ᵥ ∅ = ∅ := image2_empty_right
Scalar Subtraction with Empty Set Yields Empty Set
Informal description
For any set $s$ of elements of type $\beta$, the scalar subtraction of $s$ with the empty set is the empty set, i.e., $s -ᵥ \emptyset = \emptyset$.
Set.vsub_eq_empty theorem
: s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
Full source 
@[simp] lemma vsub_eq_empty : s -ᵥ ts -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅ := image2_eq_empty_iff
Empty Scalar Subtraction of Sets iff Either Set Empty
Informal description
For any sets $s$ and $t$ in a type $\alpha$ equipped with a scalar subtraction operation $-ᵥ$, the scalar subtraction $s -ᵥ t$ is empty if and only if either $s$ is empty or $t$ is empty. That is, $s -ᵥ t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.
Set.vsub_nonempty theorem
: (s -ᵥ t : Set α).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Full source 
@[simp]
lemma vsub_nonempty : (s -ᵥ t : Set α).Nonempty ↔ s.Nonempty ∧ t.Nonempty := image2_nonempty_iff
Nonempty Condition for Scalar Subtraction of Sets
Informal description
For any sets $s, t \subseteq \alpha$ equipped with a scalar subtraction operation $-ᵥ$, the set $s -ᵥ t$ is nonempty if and only if both $s$ and $t$ are nonempty.
Set.Nonempty.vsub theorem
: s.Nonempty → t.Nonempty → (s -ᵥ t : Set α).Nonempty
Full source 
lemma Nonempty.vsub : s.Nonempty → t.Nonempty → (s -ᵥ t : Set α).Nonempty := .image2
Nonempty Scalar Subtraction of Nonempty Sets
Informal description
For any nonempty sets $s$ and $t$ in a type $\alpha$ equipped with a scalar subtraction operation $-ᵥ$, the set $s -ᵥ t$ is nonempty.
Set.Nonempty.of_vsub_left theorem
: (s -ᵥ t : Set α).Nonempty → s.Nonempty
Full source 
lemma Nonempty.of_vsub_left : (s -ᵥ t : Set α).Nonempty → s.Nonempty := .of_image2_left
Nonemptiness of Left Set in Scalar Subtraction
Informal description
For any sets $s, t \subseteq \alpha$ equipped with a scalar subtraction operation $-ᵥ$, if the set $s -ᵥ t$ is nonempty, then $s$ is nonempty.
Set.Nonempty.of_vsub_right theorem
: (s -ᵥ t : Set α).Nonempty → t.Nonempty
Full source 
lemma Nonempty.of_vsub_right : (s -ᵥ t : Set α).Nonempty → t.Nonempty := .of_image2_right
Nonemptiness of Second Set in Scalar Subtraction Implies Nonemptiness of Second Set
Informal description
For any sets $s$ and $t$ in a type $\alpha$ equipped with a scalar subtraction operation $-ᵥ$, if the set $s -ᵥ t$ is nonempty, then $t$ is nonempty.
Set.vsub_singleton theorem
(s : Set β) (b : β) : s -ᵥ { b } = (· -ᵥ b) '' s
Full source 
@[simp low+1]
lemma vsub_singleton (s : Set β) (b : β) : s -ᵥ {b} = (· -ᵥ b) '' s := image2_singleton_right
Scalar Subtraction of Set by Singleton: $s -ᵥ \{b\} = \{x -ᵥ b \mid x \in s\}$
Informal description
For any set $s \subseteq \beta$ and any element $b \in \beta$, the scalar subtraction of $s$ by the singleton set $\{b\}$ is equal to the image of $s$ under the function $\lambda x, x -ᵥ b$. In other words, $s -ᵥ \{b\} = \{x -ᵥ b \mid x \in s\}$.
Set.singleton_vsub theorem
(t : Set β) (b : β) : { b } -ᵥ t = (b -ᵥ ·) '' t
Full source 
@[simp low+1]
lemma singleton_vsub (t : Set β) (b : β) : {b}{b} -ᵥ t = (b -ᵥ ·) '' t := image2_singleton_left
Scalar subtraction of singleton set: $\{b\} -ᵥ t = \{b -ᵥ x \mid x \in t\}$
Informal description
For any set $t \subseteq \beta$ and any element $b \in \beta$, the scalar subtraction of the singleton set $\{b\}$ from $t$ is equal to the image of $t$ under the function $x \mapsto b -ᵥ x$. That is, $\{b\} -ᵥ t = \{b -ᵥ x \mid x \in t\}$.
Set.singleton_vsub_singleton theorem
: ({ b } : Set β) -ᵥ { c } = {b -ᵥ c}
Full source 
@[simp high] lemma singleton_vsub_singleton : ({b} : Set β) -ᵥ {c} = {b -ᵥ c} := image2_singleton
Scalar subtraction of singletons: $\{b\} -ᵥ \{c\} = \{b -ᵥ c\}$
Informal description
For any elements $b, c \in \beta$, the scalar subtraction of the singleton set $\{b\}$ by the singleton set $\{c\}$ is the singleton set $\{b -ᵥ c\}$. In other words, $\{b\} -ᵥ \{c\} = \{b -ᵥ c\}$.
Set.vsub_subset_vsub theorem
: s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
Full source 
@[mono, gcongr] lemma vsub_subset_vsub : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂ := image2_subset
Monotonicity of Scalar Subtraction on Sets: $s₁ \subseteq s₂ \land t₁ \subseteq t₂ \implies s₁ -ᵥ t₁ \subseteq s₂ -ᵥ t₂$
Informal description
For any sets $s₁, s₂, t₁, t₂$ in a type with a scalar subtraction operation $-ᵥ$, if $s₁ \subseteq s₂$ and $t₁ \subseteq t₂$, then the scalar subtraction of sets satisfies $s₁ -ᵥ t₁ \subseteq s₂ -ᵥ t₂$.
Set.vsub_subset_vsub_left theorem
: t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
Full source 
@[gcongr] lemma vsub_subset_vsub_left : t₁ ⊆ t₂ → s -ᵥ t₁s -ᵥ t₁ ⊆ s -ᵥ t₂ := image2_subset_left
Left Monotonicity of Scalar Subtraction on Sets: $t₁ \subseteq t₂ \implies s -ᵥ t₁ \subseteq s -ᵥ t₂$
Informal description
For any sets $s, t₁, t₂$ in a type with a scalar subtraction operation $-ᵥ$, if $t₁ \subseteq t₂$, then the scalar subtraction set $s -ᵥ t₁$ is a subset of $s -ᵥ t₂$.
Set.vsub_subset_vsub_right theorem
: s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
Full source 
@[gcongr] lemma vsub_subset_vsub_right : s₁ ⊆ s₂ → s₁ -ᵥ ts₁ -ᵥ t ⊆ s₂ -ᵥ t := image2_subset_right
Right Monotonicity of Scalar Subtraction on Sets: $s₁ \subseteq s₂ \implies s₁ -ᵥ t \subseteq s₂ -ᵥ t$
Informal description
For any sets $s₁, s₂, t$ in a type with a scalar subtraction operation $-ᵥ$, if $s₁ \subseteq s₂$, then the scalar subtraction set $s₁ -ᵥ t$ is a subset of $s₂ -ᵥ t$.
Set.vsub_subset_iff theorem
: s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u
Full source 
lemma vsub_subset_iff : s -ᵥ ts -ᵥ t ⊆ us -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u := image2_subset_iff
Subset Condition for Scalar Subtraction of Sets
Informal description
For any sets $s, t \subseteq \beta$ and $u \subseteq \gamma$, the scalar subtraction set $s -ᵥ t$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the scalar subtraction $x -ᵥ y$ belongs to $u$. In other words: \[ s -ᵥ t \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, x -ᵥ y \in u. \]
Set.vsub_self_mono theorem
(h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t
Full source 
lemma vsub_self_mono (h : s ⊆ t) : s -ᵥ ss -ᵥ s ⊆ t -ᵥ t := vsub_subset_vsub h h
Monotonicity of Self Scalar Subtraction: $s \subseteq t \implies s -ᵥ s \subseteq t -ᵥ t$
Informal description
For any sets $s$ and $t$ in a type with a scalar subtraction operation $-ᵥ$, if $s \subseteq t$, then the scalar subtraction set $s -ᵥ s$ is a subset of $t -ᵥ t$.
Set.union_vsub theorem
: s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
Full source 
lemma union_vsub : s₁ ∪ s₂s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ ts₁ -ᵥ t ∪ (s₂ -ᵥ t) := image2_union_left
Distributivity of Scalar Subtraction over Union in First Argument: $(s_1 \cup s_2) -ᵥ t = (s_1 -ᵥ t) \cup (s_2 -ᵥ t)$
Informal description
For any sets $s_1, s_2, t \subseteq \beta$, the scalar subtraction of the union $s_1 \cup s_2$ with $t$ is equal to the union of the scalar subtractions $s_1 -ᵥ t$ and $s_2 -ᵥ t$. That is, \[ (s_1 \cup s_2) -ᵥ t = (s_1 -ᵥ t) \cup (s_2 -ᵥ t). \]
Set.vsub_union theorem
: s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
Full source 
lemma vsub_union : s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁s -ᵥ t₁ ∪ (s -ᵥ t₂) := image2_union_right
Distributivity of Scalar Subtraction over Union in Second Argument
Informal description
For any sets $s, t_1, t_2$ in a type with a scalar subtraction operation $-ᵥ$, the scalar subtraction of $s$ with the union $t_1 \cup t_2$ is equal to the union of the scalar subtractions $s -ᵥ t_1$ and $s -ᵥ t_2$. That is, \[ s -ᵥ (t_1 \cup t_2) = (s -ᵥ t_1) \cup (s -ᵥ t_2). \]
Set.inter_vsub_subset theorem
: s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
Full source 
lemma inter_vsub_subset : s₁ ∩ s₂s₁ ∩ s₂ -ᵥ ts₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t) := image2_inter_subset_left
Intersection Subset Property for Scalar Subtraction of Sets
Informal description
For any sets $s_1, s_2, t$ in a type with a scalar subtraction operation $-ᵥ$, the scalar subtraction of the intersection $s_1 \cap s_2$ with $t$ is a subset of the intersection of the scalar subtractions $s_1 -ᵥ t$ and $s_2 -ᵥ t$. That is, \[ (s_1 \cap s_2) -ᵥ t \subseteq (s_1 -ᵥ t) \cap (s_2 -ᵥ t). \]
Set.vsub_inter_subset theorem
: s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
Full source 
lemma vsub_inter_subset : s -ᵥ t₁ ∩ t₂s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂) := image2_inter_subset_right
Subset Property of Scalar Subtraction over Intersection in Second Argument
Informal description
For any sets $s, t_1, t_2$ in a type with a scalar subtraction operation $-ᵥ$, the scalar subtraction of $s$ with the intersection $t_1 \cap t_2$ is a subset of the intersection of the scalar subtractions $s -ᵥ t_1$ and $s -ᵥ t_2$. That is, \[ s -ᵥ (t_1 \cap t_2) \subseteq (s -ᵥ t_1) \cap (s -ᵥ t_2). \]
Set.inter_vsub_union_subset_union theorem
: s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
Full source 
lemma inter_vsub_union_subset_union : s₁ ∩ s₂s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂)s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂) :=
  image2_inter_union_subset_union
Subset Property for Scalar Subtraction on Intersection-Union Pairs
Informal description
For any sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$ with a scalar subtraction operation $-ᵥ : \alpha \rightarrow \beta \rightarrow \beta$, the following subset relation holds: \[ (s_1 \cap s_2) -ᵥ (t_1 \cup t_2) \subseteq (s_1 -ᵥ t_1) \cup (s_2 -ᵥ t_2). \] Here, $A -ᵥ B$ denotes the set $\{a -ᵥ b \mid a \in A, b \in B\}$.
Set.union_vsub_inter_subset_union theorem
: s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
Full source 
lemma union_vsub_inter_subset_union : s₁ ∪ s₂s₁ ∪ s₂ -ᵥ t₁ ∩ t₂s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂) :=
  image2_union_inter_subset_union
Union-Intersection Subset Property for Scalar Subtraction: $(s₁ \cup s₂) -ᵥ (t₁ \cap t₂) \subseteq (s₁ -ᵥ t₁) \cup (s₂ -ᵥ t₂)$
Informal description
For any sets $s₁, s₂ \subseteq \alpha$ and $t₁, t₂ \subseteq \beta$ with a scalar subtraction operation $-ᵥ : \alpha \rightarrow \beta \rightarrow \gamma$, the following subset relation holds: $$ (s₁ \cup s₂) -ᵥ (t₁ \cap t₂) \subseteq (s₁ -ᵥ t₁) \cup (s₂ -ᵥ t₂). $$ Here, $s -ᵥ t$ denotes the set $\{x -ᵥ y \mid x \in s, y \in t\}$.
Set.image_smul_comm theorem
[SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Set β) : (∀ b, f (a • b) = a • f b) → f '' (a • s) = a • f '' s
Full source 
@[to_additive]
lemma image_smul_comm [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Set β) :
    (∀ b, f (a • b) = a • f b) → f '' (a • s) = a • f '' s := image_comm
Commutativity of Image and Scalar Multiplication: $f(a \cdot s) = a \cdot f(s)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types equipped with scalar multiplication operations. For any function $f \colon \beta \to \gamma$, scalar $a \in \alpha$, and set $s \subseteq \beta$, if $f$ satisfies the commutation relation $f(a \cdot b) = a \cdot f(b)$ for all $b \in \beta$, then the image of the scaled set $a \cdot s$ under $f$ equals the scaled image of $s$ under $f$, i.e., $$ f(a \cdot s) = a \cdot f(s). $$
Set.op_smul_set_smul_eq_smul_smul_set theorem
(a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) : (op a • s) • t = s • a • t
Full source 
@[to_additive]
lemma op_smul_set_smul_eq_smul_smul_set (a : α) (s : Set β) (t : Set γ)
    (h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) : (op a • s) • t = s • a • t := by
  ext; simp [mem_smul, mem_smul_set, h]
Compatibility of Opposite Scalar Multiplication with Set Operations: $(a^\text{op} \cdot s) \cdot t = s \cdot (a \cdot t)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types equipped with scalar multiplication operations. For any element $a \in \alpha$, sets $s \subseteq \beta$ and $t \subseteq \gamma$, and a compatibility condition $h$ stating that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, we have $(a^\text{op} \cdot b) \cdot c = b \cdot (a \cdot c)$, the following equality holds: $$(a^\text{op} \cdot s) \cdot t = s \cdot (a \cdot t)$$ where $a^\text{op}$ denotes the multiplicative opposite of $a$, and $\cdot$ denotes the respective scalar multiplications.