doc-next-gen

Mathlib.Algebra.Group.Pointwise.Set.Lattice

Module docstring

{"# Indexed unions and intersections of pointwise operations of sets

This file contains lemmas on taking the union and intersection over pointwise algebraic operations on sets.

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction ","### Set negation/inversion ","### Set addition/multiplication ","### Set subtraction/division ","### Translation/scaling of sets "}

Set.iInter_inv theorem
(s : ι → Set α) : (⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem iInter_inv (s : ι → Set α) : (⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹ :=
  preimage_iInter
Inverse of Indexed Intersection Equals Intersection of Inverses
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the inverse of their intersection equals the intersection of their inverses. That is: \[ \left( \bigcap_{i} s_i \right)^{-1} = \bigcap_{i} s_i^{-1}. \]
Set.sInter_inv theorem
(S : Set (Set α)) : (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹
Full source 
@[to_additive (attr := simp)]
theorem sInter_inv (S : Set (Set α)) : (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹ :=
  preimage_sInter
Inverse of Set Intersection Equals Intersection of Inverses
Informal description
For any collection of sets \( S \subseteq \mathcal{P}(\alpha) \), the inverse of their intersection equals the intersection of their inverses. That is: \[ \left( \bigcap_{s \in S} s \right)^{-1} = \bigcap_{s \in S} s^{-1}. \]
Set.iUnion_inv theorem
(s : ι → Set α) : (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹
Full source 
@[to_additive (attr := simp)]
theorem iUnion_inv (s : ι → Set α) : (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹ :=
  preimage_iUnion
Inverse of Union Equals Union of Inverses
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the inverse of their union equals the union of their inverses. That is: $$ \left(\bigcup_{i} s_i\right)^{-1} = \bigcup_{i} s_i^{-1} $$
Set.sUnion_inv theorem
(S : Set (Set α)) : (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹
Full source 
@[to_additive (attr := simp)]
theorem sUnion_inv (S : Set (Set α)) : (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹ :=
  preimage_sUnion
Inverse of Union of Sets Equals Union of Inverses
Informal description
For any collection of sets $S$ consisting of subsets of a type $\alpha$, the inverse of the union of all sets in $S$ equals the union of the inverses of each set in $S$. That is: \[ \left( \bigcup_{s \in S} s \right)^{-1} = \bigcup_{s \in S} s^{-1}. \]
Set.iUnion_mul_left_image theorem
: ⋃ a ∈ s, (a * ·) '' t = s * t
Full source 
@[to_additive]
theorem iUnion_mul_left_image : ⋃ a ∈ s, (a * ·) '' t = s * t :=
  iUnion_image_left _
Union of Left Multiplications Equals Pointwise Product
Informal description
For any sets $s$ and $t$ in a type $\alpha$ with a multiplication operation, the union over all $a \in s$ of the images of $t$ under left multiplication by $a$ equals the pointwise product of $s$ and $t$. In symbols: \[ \bigcup_{a \in s} \{a \cdot x \mid x \in t\} = s \cdot t \]
Set.iUnion_mul_right_image theorem
: ⋃ a ∈ t, (· * a) '' s = s * t
Full source 
@[to_additive]
theorem iUnion_mul_right_image : ⋃ a ∈ t, (· * a) '' s = s * t :=
  iUnion_image_right _
Union of Right Multiplications Equals Pointwise Product
Informal description
For any set $s$ and $t$ in a type $\alpha$ with a multiplication operation, the union over all $a \in t$ of the images of $s$ under right multiplication by $a$ equals the pointwise product of $s$ and $t$. In symbols: \[ \bigcup_{a \in t} \{x \cdot a \mid x \in s\} = s \cdot t \]
Set.iUnion_mul theorem
(s : ι → Set α) (t : Set α) : (⋃ i, s i) * t = ⋃ i, s i * t
Full source 
@[to_additive]
theorem iUnion_mul (s : ι → Set α) (t : Set α) : (⋃ i, s i) * t = ⋃ i, s i * t :=
  image2_iUnion_left ..
Distributivity of Pointwise Multiplication over Indexed Union
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ with a multiplication operation, and any set $t \subseteq \alpha$, the pointwise product of the union $\bigcup_i s_i$ with $t$ equals the union of the pointwise products $s_i * t$ for all $i \in \iota$. In symbols: $$ \left(\bigcup_{i} s_i\right) * t = \bigcup_{i} (s_i * t). $$
Set.mul_iUnion theorem
(s : Set α) (t : ι → Set α) : (s * ⋃ i, t i) = ⋃ i, s * t i
Full source 
@[to_additive]
theorem mul_iUnion (s : Set α) (t : ι → Set α) : (s * ⋃ i, t i) = ⋃ i, s * t i :=
  image2_iUnion_right ..
Distributivity of Pointwise Multiplication over Indexed Union (Left)
Informal description
For any set $s$ in a type $\alpha$ with a multiplication operation, and any indexed family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, the pointwise product of $s$ with the union $\bigcup_i t_i$ equals the union of the pointwise products $s \cdot t_i$ for all $i \in \iota$. In symbols: $$ s \cdot \left( \bigcup_{i} t_i \right) = \bigcup_{i} (s \cdot t_i). $$
Set.sUnion_mul theorem
(S : Set (Set α)) (t : Set α) : ⋃₀ S * t = ⋃ s ∈ S, s * t
Full source 
@[to_additive]
theorem sUnion_mul (S : Set (Set α)) (t : Set α) : ⋃₀ S * t = ⋃ s ∈ S, s * t :=
  image2_sUnion_left ..
Distributivity of Pointwise Multiplication over Union of Sets
Informal description
For any family of sets $S \subseteq \mathcal{P}(\alpha)$ and any set $t \subseteq \alpha$, the pointwise multiplication of the union $\bigcup S$ with $t$ equals the union over all $s \in S$ of the pointwise multiplications $s \cdot t$. In symbols: $$ \left( \bigcup S \right) \cdot t = \bigcup_{s \in S} (s \cdot t). $$
Set.mul_sUnion theorem
(s : Set α) (T : Set (Set α)) : s * ⋃₀ T = ⋃ t ∈ T, s * t
Full source 
@[to_additive]
theorem mul_sUnion (s : Set α) (T : Set (Set α)) : s * ⋃₀ T = ⋃ t ∈ T, s * t :=
  image2_sUnion_right ..
Distributivity of Pointwise Multiplication over Union of Families of Sets
Informal description
For any set $s \subseteq \alpha$ and any family of sets $T \subseteq \mathcal{P}(\alpha)$, the pointwise multiplication of $s$ with the union of all sets in $T$ equals the union over all $t \in T$ of the pointwise multiplications of $s$ with $t$. In symbols: $$ s \cdot \left( \bigcup_{t \in T} t \right) = \bigcup_{t \in T} (s \cdot t) $$
Set.iUnion₂_mul theorem
(s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) * t = ⋃ (i) (j), s i j * t
Full source 
@[to_additive]
theorem iUnion₂_mul (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋃ (i) (j), s i j) * t = ⋃ (i) (j), s i j * t :=
  image2_iUnion₂_left ..
Distributivity of Pointwise Multiplication over Indexed Union of Sets
Informal description
For any indexed family of sets \( s_{i,j} \subseteq \alpha \) (where \( i \) and \( j \) are indices) and any set \( t \subseteq \alpha \), the pointwise multiplication of the union \( \bigcup_{i,j} s_{i,j} \) with \( t \) is equal to the union of the pointwise multiplications \( \bigcup_{i,j} (s_{i,j} \cdot t) \). In symbols: $$ \left( \bigcup_{i,j} s_{i,j} \right) \cdot t = \bigcup_{i,j} (s_{i,j} \cdot t) $$
Set.mul_iUnion₂ theorem
(s : Set α) (t : ∀ i, κ i → Set α) : (s * ⋃ (i) (j), t i j) = ⋃ (i) (j), s * t i j
Full source 
@[to_additive]
theorem mul_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s * ⋃ (i) (j), t i j) = ⋃ (i) (j), s * t i j :=
  image2_iUnion₂_right ..
Distributivity of Pointwise Multiplication over Doubly-Indexed Union of Sets
Informal description
For any set $s \subseteq \alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the pointwise multiplication of $s$ with the union $\bigcup_{i,j} t_{i,j}$ equals the union of the pointwise multiplications $s \cdot t_{i,j}$ for all $i \in \iota$ and $j \in \kappa_i$. In symbols: $$ s \cdot \left( \bigcup_{i,j} t_{i,j} \right) = \bigcup_{i,j} (s \cdot t_{i,j}). $$
Set.iInter_mul_subset theorem
(s : ι → Set α) (t : Set α) : (⋂ i, s i) * t ⊆ ⋂ i, s i * t
Full source 
@[to_additive]
theorem iInter_mul_subset (s : ι → Set α) (t : Set α) : (⋂ i, s i) * t ⊆ ⋂ i, s i * t :=
  Set.image2_iInter_subset_left ..
Intersection-Pointwise Multiplication Subset Property
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t \subseteq \alpha$, the pointwise multiplication of the intersection $\bigcap_i s_i$ with $t$ is contained in the intersection of the pointwise multiplications $s_i \cdot t$ for all $i$. That is, $$ \left(\bigcap_{i} s_i\right) \cdot t \subseteq \bigcap_{i} (s_i \cdot t). $$
Set.mul_iInter_subset theorem
(s : Set α) (t : ι → Set α) : (s * ⋂ i, t i) ⊆ ⋂ i, s * t i
Full source 
@[to_additive]
theorem mul_iInter_subset (s : Set α) (t : ι → Set α) : (s * ⋂ i, t i) ⊆ ⋂ i, s * t i :=
  image2_iInter_subset_right ..
Pointwise Multiplication Preserves Subset Relation with Intersection
Informal description
For any set $s \subseteq \alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, the pointwise multiplication of $s$ with the intersection $\bigcap_i t_i$ is contained in the intersection of the pointwise multiplications $s \cdot t_i$ for all $i \in \iota$. In symbols: $$ s \cdot \left( \bigcap_i t_i \right) \subseteq \bigcap_i (s \cdot t_i). $$
Set.mul_sInter_subset theorem
(s : Set α) (T : Set (Set α)) : s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t
Full source 
@[to_additive]
lemma mul_sInter_subset (s : Set α) (T : Set (Set α)) :
    s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t := image2_sInter_right_subset s T (fun a b => a * b)
Pointwise product with intersection is contained in intersection of pointwise products
Informal description
For any subset $s$ of a type $\alpha$ and any family $T$ of subsets of $\alpha$, the pointwise product of $s$ with the intersection of $T$ is contained in the intersection over $t \in T$ of the pointwise products $s * t$. In symbols: \[ s \cdot \bigcap T \subseteq \bigcap_{t \in T} (s \cdot t). \]
Set.sInter_mul_subset theorem
(S : Set (Set α)) (t : Set α) : ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t
Full source 
@[to_additive]
lemma sInter_mul_subset (S : Set (Set α)) (t : Set α) :
    ⋂₀ S⋂₀ S * t ⊆ ⋂ s ∈ S, s * t := image2_sInter_left_subset S t (fun a b => a * b)
Intersection-Multiplication Subset Property
Informal description
For any family of sets $S$ in a type $\alpha$ and any set $t \subseteq \alpha$, the product of the intersection of $S$ with $t$ is contained in the intersection of the products of each set $s \in S$ with $t$. In symbols: $$ \left(\bigcap S\right) \cdot t \subseteq \bigcap_{s \in S} (s \cdot t) $$
Set.iInter₂_mul_subset theorem
(s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) * t ⊆ ⋂ (i) (j), s i j * t
Full source 
@[to_additive]
theorem iInter₂_mul_subset (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) * t ⊆ ⋂ (i) (j), s i j * t :=
  image2_iInter₂_subset_left ..
Intersection-Multiplication Subset Property: $(\bigcap s_{i,j}) * t \subseteq \bigcap (s_{i,j} * t)$
Informal description
For a family of sets $(s_{i,j})_{i,j}$ indexed by $i$ and $j$ in a type $\alpha$ with a multiplication operation, and a set $t \subseteq \alpha$, the product of the intersection $\bigcap_{i,j} s_{i,j}$ with $t$ is contained in the intersection of the products $s_{i,j} * t$ for all $i,j$. In symbols: $$ \left(\bigcap_{i,j} s_{i,j}\right) * t \subseteq \bigcap_{i,j} (s_{i,j} * t). $$
Set.mul_iInter₂_subset theorem
(s : Set α) (t : ∀ i, κ i → Set α) : (s * ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s * t i j
Full source 
@[to_additive]
theorem mul_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) :
    (s * ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s * t i j :=
  image2_iInter₂_subset_right ..
Multiplication of Set with Intersection is Contained in Intersection of Multiplications
Informal description
For any set $s$ in a type $\alpha$ with a multiplication operation, and for any indexed family of sets $t_{i,j}$ in $\alpha$, the product of $s$ with the intersection of all $t_{i,j}$ is contained in the intersection of all products $s \cdot t_{i,j}$. In symbols: $$ s \cdot \left( \bigcap_{i,j} t_{i,j} \right) \subseteq \bigcap_{i,j} (s \cdot t_{i,j}). $$
Set.iUnion_div_left_image theorem
: ⋃ a ∈ s, (a / ·) '' t = s / t
Full source 
@[to_additive]
theorem iUnion_div_left_image : ⋃ a ∈ s, (a / ·) '' t = s / t :=
  iUnion_image_left _
Union of Left Division Images Equals Set Division: $\bigcup_{a \in s} a / t = s / t$
Informal description
For any sets $s$ and $t$ in a type $\alpha$ with a division operation, the union over all $a \in s$ of the images of $t$ under the left division operation $(y \mapsto a / y)$ equals the division of $s$ by $t$. In symbols: \[ \bigcup_{a \in s} \{a / y \mid y \in t\} = s / t. \]
Set.iUnion_div_right_image theorem
: ⋃ a ∈ t, (· / a) '' s = s / t
Full source 
@[to_additive]
theorem iUnion_div_right_image : ⋃ a ∈ t, (· / a) '' s = s / t :=
  iUnion_image_right _
Union of Right Division Images Equals Set Division: $\bigcup_{a \in t} s / a = s / t$
Informal description
For any set $s$ and $t$ in a type $\alpha$ with a division operation, the union over all $a \in t$ of the images of $s$ under the right division operation $(x \mapsto x / a)$ equals the division of $s$ by $t$. In symbols: \[ \bigcup_{a \in t} \{x / a \mid x \in s\} = s / t. \]
Set.iUnion_div theorem
(s : ι → Set α) (t : Set α) : (⋃ i, s i) / t = ⋃ i, s i / t
Full source 
@[to_additive]
theorem iUnion_div (s : ι → Set α) (t : Set α) : (⋃ i, s i) / t = ⋃ i, s i / t :=
  image2_iUnion_left ..
Union of Set Divisions: $(\bigcup_i s_i) / t = \bigcup_i (s_i / t)$
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the division of the union $\bigcup_i s_i$ by $t$ equals the union of the divisions $s_i / t$ for all $i \in \iota$. In symbols: $$\left(\bigcup_{i} s_i\right) / t = \bigcup_{i} (s_i / t).$$
Set.div_iUnion theorem
(s : Set α) (t : ι → Set α) : (s / ⋃ i, t i) = ⋃ i, s / t i
Full source 
@[to_additive]
theorem div_iUnion (s : Set α) (t : ι → Set α) : (s / ⋃ i, t i) = ⋃ i, s / t i :=
  image2_iUnion_right ..
Division of Set by Union Equals Union of Divisions: $s / \bigcup_i t_i = \bigcup_i (s / t_i)$
Informal description
For any set $s$ in a type $\alpha$ and any indexed family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, the division of $s$ by the union $\bigcup_i t_i$ equals the union of the divisions $s / t_i$ for all $i \in \iota$. In symbols: $$ s / \left(\bigcup_{i} t_i\right) = \bigcup_{i} (s / t_i). $$
Set.sUnion_div theorem
(S : Set (Set α)) (t : Set α) : ⋃₀ S / t = ⋃ s ∈ S, s / t
Full source 
@[to_additive]
theorem sUnion_div (S : Set (Set α)) (t : Set α) : ⋃₀ S / t = ⋃ s ∈ S, s / t :=
  image2_sUnion_left ..
Division Distributes Over Union of Sets: $(\bigcup S) / t = \bigcup_{s \in S} (s / t)$
Informal description
For any family of sets $S \subseteq \mathcal{P}(\alpha)$ and any set $t \subseteq \alpha$, the division of the union $\bigcup S$ by $t$ equals the union over all $s \in S$ of the divisions $s / t$. In symbols: $$ \left(\bigcup S\right) / t = \bigcup_{s \in S} (s / t). $$
Set.div_sUnion theorem
(s : Set α) (T : Set (Set α)) : s / ⋃₀ T = ⋃ t ∈ T, s / t
Full source 
@[to_additive]
theorem div_sUnion (s : Set α) (T : Set (Set α)) : s / ⋃₀ T = ⋃ t ∈ T, s / t :=
  image2_sUnion_right ..
Division of Set by Union Equals Union of Divisions: $s / \bigcup T = \bigcup_{t \in T} (s / t)$
Informal description
For any set $s$ in a type $\alpha$ and any family of sets $T \subseteq \mathcal{P}(\alpha)$, the division of $s$ by the union $\bigcup T$ equals the union over all $t \in T$ of the divisions $s / t$. In symbols: $$ s / \left(\bigcup T\right) = \bigcup_{t \in T} (s / t). $$
Set.iUnion₂_div theorem
(s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) / t = ⋃ (i) (j), s i j / t
Full source 
@[to_additive]
theorem iUnion₂_div (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋃ (i) (j), s i j) / t = ⋃ (i) (j), s i j / t :=
  image2_iUnion₂_left ..
Union of Divisions Equals Division of Union for Indexed Family of Sets
Informal description
For an indexed family of sets \( s_i \) (where \( i \) ranges over some index set and \( j \) ranges over another index set \( \kappa_i \)) and a set \( t \), the division of their union by \( t \) equals the union of the divisions of each \( s_i \) by \( t \). That is, \[ \left( \bigcup_{i,j} s_i(j) \right) / t = \bigcup_{i,j} (s_i(j) / t). \]
Set.div_iUnion₂ theorem
(s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋃ (i) (j), t i j) = ⋃ (i) (j), s / t i j
Full source 
@[to_additive]
theorem div_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s / ⋃ (i) (j), t i j) = ⋃ (i) (j), s / t i j :=
  image2_iUnion₂_right ..
Division of Set by Doubly-Indexed Union Equals Union of Divisions
Informal description
For any set $s$ in a type $\alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the division of $s$ by the union $\bigcup_{i,j} t_{i,j}$ equals the union of the divisions $s / t_{i,j}$ for all $i \in \iota$ and $j \in \kappa_i$. In symbols: $$ s / \left(\bigcup_{i,j} t_{i,j}\right) = \bigcup_{i,j} (s / t_{i,j}). $$
Set.iInter_div_subset theorem
(s : ι → Set α) (t : Set α) : (⋂ i, s i) / t ⊆ ⋂ i, s i / t
Full source 
@[to_additive]
theorem iInter_div_subset (s : ι → Set α) (t : Set α) : (⋂ i, s i) / t ⊆ ⋂ i, s i / t :=
  image2_iInter_subset_left ..
Intersection of Divisions is Contained in Division of Intersections
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t \subseteq \alpha$, the division of the intersection $\bigcap_i s_i$ by $t$ is contained in the intersection of the divisions of each $s_i$ by $t$. That is, $$ \left(\bigcap_{i} s_i\right) / t \subseteq \bigcap_{i} (s_i / t). $$
Set.div_iInter_subset theorem
(s : Set α) (t : ι → Set α) : (s / ⋂ i, t i) ⊆ ⋂ i, s / t i
Full source 
@[to_additive]
theorem div_iInter_subset (s : Set α) (t : ι → Set α) : (s / ⋂ i, t i) ⊆ ⋂ i, s / t i :=
  image2_iInter_subset_right ..
Division of Set by Intersection is Subset of Intersection of Divisions
Informal description
For any set $s$ in a type $\alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\alpha$, the division of $s$ by the intersection $\bigcap_i t_i$ is contained in the intersection of the divisions $s / t_i$ for all $i \in \iota$. In symbols: $$ s / \left(\bigcap_i t_i\right) \subseteq \bigcap_i (s / t_i). $$
Set.sInter_div_subset theorem
(S : Set (Set α)) (t : Set α) : ⋂₀ S / t ⊆ ⋂ s ∈ S, s / t
Full source 
@[to_additive]
theorem sInter_div_subset (S : Set (Set α)) (t : Set α) : ⋂₀ S⋂₀ S / t ⊆ ⋂ s ∈ S, s / t :=
  image2_sInter_subset_left ..
Intersection of Set Division: $\left(\bigcap S\right) / t \subseteq \bigcap_{s \in S} (s / t)$
Informal description
For any family of sets $S$ of subsets of a type $\alpha$ and any subset $t \subseteq \alpha$, the set division of the intersection $\bigcap_{s \in S} s$ by $t$ is contained in the intersection of the set divisions of each $s \in S$ by $t$, i.e., $$ \left(\bigcap_{s \in S} s\right) / t \subseteq \bigcap_{s \in S} (s / t). $$
Set.div_sInter_subset theorem
(s : Set α) (T : Set (Set α)) : s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t
Full source 
@[to_additive]
theorem div_sInter_subset (s : Set α) (T : Set (Set α)) : s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t :=
  image2_sInter_subset_right ..
Set Division Preserves Intersection Containment
Informal description
For any set $s$ and any collection of sets $T$ in a type $\alpha$, the set division $s / \bigcap T$ is contained in the intersection of all set divisions $s / t$ for $t \in T$. In symbols: $$ s / \bigcap T \subseteq \bigcap_{t \in T} (s / t) $$
Set.iInter₂_div_subset theorem
(s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) / t ⊆ ⋂ (i) (j), s i j / t
Full source 
@[to_additive]
theorem iInter₂_div_subset (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) / t ⊆ ⋂ (i) (j), s i j / t :=
  image2_iInter₂_subset_left ..
Intersection of Sets Divided by a Set is Contained in Intersection of Divisions
Informal description
For any indexed family of sets $(s_{i,j})_{i,j}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the division of the intersection $\bigcap_{i,j} s_{i,j}$ by $t$ is contained in the intersection of the divisions of each $s_{i,j}$ by $t$. That is, $$ \left(\bigcap_{i,j} s_{i,j}\right) / t \subseteq \bigcap_{i,j} (s_{i,j} / t). $$
Set.div_iInter₂_subset theorem
(s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s / t i j
Full source 
@[to_additive]
theorem div_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) :
    (s / ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s / t i j :=
  image2_iInter₂_subset_right ..
Division of Set by Indexed Intersection is Contained in Intersection of Divisions
Informal description
For any set $s$ in a type $\alpha$ and any indexed family of sets $(t_{i,j})_{i,j}$ in $\alpha$, the division of $s$ by the intersection $\bigcap_{i,j} t_{i,j}$ is contained in the intersection of the divisions of $s$ by each $t_{i,j}$. In symbols: $$ s / \left(\bigcap_{i,j} t_{i,j}\right) \subseteq \bigcap_{i,j} (s / t_{i,j}). $$
Set.iUnion_smul_left_image theorem
: ⋃ a ∈ s, a • t = s • t
Full source 
@[to_additive] lemma iUnion_smul_left_image : ⋃ a ∈ s, a • t = s • t := iUnion_image_left _
Union of Scalar Multiples Equals Pointwise Scalar Product
Informal description
For any set $s$ of scalars and any set $t$ of vectors, the union over all $a \in s$ of the scalar multiples $a \bullet t$ equals the pointwise scalar product $s \bullet t$. In other words: \[ \bigcup_{a \in s} a \bullet t = s \bullet t \]
Set.iUnion_smul_right_image theorem
: ⋃ a ∈ t, (· • a) '' s = s • t
Full source 
@[to_additive]
lemma iUnion_smul_right_image : ⋃ a ∈ t, (· • a) '' s = s • t := iUnion_image_right _
Union of Left Scalar Multiplication Images Equals Pointwise Scalar Multiplication
Informal description
For any set $s \subseteq \alpha$ and any set $t \subseteq \beta$, the union over all $a \in t$ of the left scalar multiplication images $\{x \bullet a \mid x \in s\}$ equals the pointwise scalar multiplication $s \bullet t$. In other words: \[ \bigcup_{a \in t} \{x \bullet a \mid x \in s\} = s \bullet t \]
Set.iUnion_smul theorem
(s : ι → Set α) (t : Set β) : (⋃ i, s i) • t = ⋃ i, s i • t
Full source 
@[to_additive]
lemma iUnion_smul (s : ι → Set α) (t : Set β) : (⋃ i, s i) • t = ⋃ i, s i • t :=
  image2_iUnion_left ..
Union of Pointwise Scalar Multiplications: $(\bigcup_i s_i) \bullet t = \bigcup_i (s_i \bullet t)$
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t \subseteq \beta$, the pointwise scalar multiplication of the union $\bigcup_i s_i$ with $t$ equals the union of the pointwise scalar multiplications $s_i \bullet t$ for all $i \in \iota$. In symbols: $$ \left(\bigcup_{i} s_i\right) \bullet t = \bigcup_{i} (s_i \bullet t). $$
Set.smul_iUnion theorem
(s : Set α) (t : ι → Set β) : (s • ⋃ i, t i) = ⋃ i, s • t i
Full source 
@[to_additive]
lemma smul_iUnion (s : Set α) (t : ι → Set β) : (s • ⋃ i, t i) = ⋃ i, s • t i :=
  image2_iUnion_right ..
Distributivity of Pointwise Scalar Multiplication over Indexed Union
Informal description
For any set $s \subseteq \alpha$ and any indexed family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the pointwise scalar multiplication of $s$ with the union $\bigcup_i t_i$ equals the union of the pointwise scalar multiplications $s \bullet t_i$ for all $i \in \iota$. In symbols: $$ s \bullet \left( \bigcup_{i} t_i \right) = \bigcup_{i} (s \bullet t_i). $$
Set.sUnion_smul theorem
(S : Set (Set α)) (t : Set β) : ⋃₀ S • t = ⋃ s ∈ S, s • t
Full source 
@[to_additive]
lemma sUnion_smul (S : Set (Set α)) (t : Set β) : ⋃₀ S • t = ⋃ s ∈ S, s • t :=
  image2_sUnion_left ..
Union of Pointwise Scalar Multiplications
Informal description
For any family of sets $S$ in $\alpha$ and any set $t \subseteq \beta$, the pointwise scalar multiplication of the union $\bigcup S$ with $t$ equals the union over all $s \in S$ of the pointwise scalar multiplications $s \bullet t$. In symbols: $$ \left(\bigcup S\right) \bullet t = \bigcup_{s \in S} (s \bullet t) $$
Set.smul_sUnion theorem
(s : Set α) (T : Set (Set β)) : s • ⋃₀ T = ⋃ t ∈ T, s • t
Full source 
@[to_additive]
lemma smul_sUnion (s : Set α) (T : Set (Set β)) : s • ⋃₀ T = ⋃ t ∈ T, s • t :=
  image2_sUnion_right ..
Distributivity of Pointwise Scalar Multiplication over Union of Sets
Informal description
For any set $s \subseteq \alpha$ and any family of sets $T \subseteq \mathcal{P}(\beta)$, the pointwise scalar multiplication of $s$ with the union $\bigcup T$ equals the union over all $t \in T$ of the pointwise scalar multiplications $s \bullet t$. In symbols: $$ s \bullet \left( \bigcup T \right) = \bigcup_{t \in T} (s \bullet t). $$
Set.iUnion₂_smul theorem
(s : ∀ i, κ i → Set α) (t : Set β) : (⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t
Full source 
@[to_additive]
lemma iUnion₂_smul (s : ∀ i, κ i → Set α) (t : Set β) :
    (⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t := image2_iUnion₂_left ..
Double Union Commutes with Pointwise Scalar Multiplication
Informal description
For an indexed family of sets $s_{i,j} \subseteq \alpha$ (where $i$ and $j$ are indices) and a set $t \subseteq \beta$, the pointwise scalar multiplication of the double union $\bigcup_i \bigcup_j s_{i,j}$ with $t$ equals the double union of the pointwise scalar multiplications $s_{i,j} \bullet t$. In symbols: $$ \left(\bigcup_i \bigcup_j s_{i,j}\right) \bullet t = \bigcup_i \bigcup_j (s_{i,j} \bullet t) $$
Set.smul_iUnion₂ theorem
(s : Set α) (t : ∀ i, κ i → Set β) : (s • ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s • t i j
Full source 
@[to_additive]
lemma smul_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set β) :
    (s • ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s • t i j := image2_iUnion₂_right ..
Distributivity of Pointwise Scalar Multiplication over Doubly-Indexed Union: $s \bullet \bigcup_{i,j} t_{i,j} = \bigcup_{i,j} (s \bullet t_{i,j})$
Informal description
For any set $s \subseteq \alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\beta$, the pointwise scalar multiplication of $s$ with the union $\bigcup_{i,j} t_{i,j}$ equals the union of the pointwise scalar multiplications $s \bullet t_{i,j}$ for all $i \in \iota$ and $j \in \kappa_i$. In symbols: $$ s \bullet \left( \bigcup_{i,j} t_{i,j} \right) = \bigcup_{i,j} (s \bullet t_{i,j}). $$
Set.iInter_smul_subset theorem
(s : ι → Set α) (t : Set β) : (⋂ i, s i) • t ⊆ ⋂ i, s i • t
Full source 
@[to_additive]
lemma iInter_smul_subset (s : ι → Set α) (t : Set β) : (⋂ i, s i) • t ⊆ ⋂ i, s i • t :=
  image2_iInter_subset_left ..
Intersection Subset under Pointwise Scalar Multiplication: $\left(\bigcap_i s_i\right) \bullet t \subseteq \bigcap_i (s_i \bullet t)$
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t \subseteq \beta$, the pointwise scalar multiplication of the intersection $\bigcap_i s_i$ with $t$ is contained in the intersection of the pointwise scalar multiplications $s_i \bullet t$ for all $i \in \iota$. In symbols: $$ \left(\bigcap_{i} s_i\right) \bullet t \subseteq \bigcap_{i} (s_i \bullet t). $$
Set.smul_iInter_subset theorem
(s : Set α) (t : ι → Set β) : (s • ⋂ i, t i) ⊆ ⋂ i, s • t i
Full source 
@[to_additive]
lemma smul_iInter_subset (s : Set α) (t : ι → Set β) : (s • ⋂ i, t i) ⊆ ⋂ i, s • t i :=
  image2_iInter_subset_right ..
Pointwise scalar multiplication preserves intersection containment: $s \bullet \bigcap_i t_i \subseteq \bigcap_i (s \bullet t_i)$
Informal description
For any set $s \subseteq \alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the pointwise scalar multiplication of $s$ with the intersection $\bigcap_{i} t_i$ is contained in the intersection of the pointwise scalar multiplications $s \bullet t_i$ for all $i \in \iota$. In symbols: $$ s \bullet \left( \bigcap_{i} t_i \right) \subseteq \bigcap_{i} (s \bullet t_i). $$
Set.sInter_smul_subset theorem
(S : Set (Set α)) (t : Set β) : ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t
Full source 
@[to_additive]
lemma sInter_smul_subset (S : Set (Set α)) (t : Set β) : ⋂₀ S⋂₀ S • t ⊆ ⋂ s ∈ S, s • t :=
  image2_sInter_left_subset S t (fun a x => a • x)
Intersection of Sets Under Pointwise Scalar Multiplication is Subset of Pointwise Scalar Multiplications of Intersections
Informal description
For any collection of sets $S$ in $\alpha$ and any set $t$ in $\beta$, the pointwise scalar multiplication of the intersection of $S$ with $t$ is contained in the intersection of the pointwise scalar multiplications of each set $s \in S$ with $t$. In symbols: $$ \left(\bigcap S\right) \bullet t \subseteq \bigcap_{s \in S} (s \bullet t) $$
Set.smul_sInter_subset theorem
(s : Set α) (T : Set (Set β)) : s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t
Full source 
@[to_additive]
lemma smul_sInter_subset (s : Set α) (T : Set (Set β)) : s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t :=
  image2_sInter_right_subset s T (fun a x => a • x)
Pointwise Scalar Multiplication Distributes Over Intersection
Informal description
For any subset $s$ of a type $\alpha$ and any collection $T$ of subsets of a type $\beta$, the pointwise scalar multiplication of $s$ with the intersection of $T$ is contained in the intersection over $t \in T$ of the pointwise scalar multiplications of $s$ with $t$. In symbols: \[ s \cdot \bigcap T \subseteq \bigcap_{t \in T} (s \cdot t). \]
Set.iInter₂_smul_subset theorem
(s : ∀ i, κ i → Set α) (t : Set β) : (⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t
Full source 
@[to_additive]
lemma iInter₂_smul_subset (s : ∀ i, κ i → Set α) (t : Set β) :
    (⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t := image2_iInter₂_subset_left ..
Intersection of Sets under Pointwise Scalar Multiplication is Contained in Intersection of Scalar Multiplications
Informal description
Let $(s_{i,j})_{i,j}$ be a family of subsets of $\alpha$ indexed by $i$ and $j$, and let $t$ be a subset of $\beta$. Then the pointwise scalar multiplication of the intersection $\bigcap_{i,j} s_{i,j}$ with $t$ is contained in the intersection of all pointwise scalar multiplications $s_{i,j} \bullet t$. That is, \[ \left(\bigcap_{i,j} s_{i,j}\right) \bullet t \subseteq \bigcap_{i,j} (s_{i,j} \bullet t). \]
Set.smul_iInter₂_subset theorem
(s : Set α) (t : ∀ i, κ i → Set β) : (s • ⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, s • t i j
Full source 
@[to_additive]
lemma smul_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set β) :
    (s • ⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, s • t i j := image2_iInter₂_subset_right ..
Pointwise Scalar Multiplication Distributes Over Indexed Intersection
Informal description
Let $s$ be a subset of $\alpha$ and $\{t_{i,j}\}_{i,j}$ be a family of subsets of $\beta$ indexed by $i$ and $j$. Then the pointwise scalar multiplication of $s$ with the intersection $\bigcap_{i,j} t_{i,j}$ is contained in the intersection of all pointwise scalar multiplications $s \bullet t_{i,j}$. In symbols: $$ s \bullet \left( \bigcap_{i,j} t_{i,j} \right) \subseteq \bigcap_{i,j} (s \bullet t_{i,j}). $$
Set.iUnion_smul_set theorem
(s : Set α) (t : Set β) : ⋃ a ∈ s, a • t = s • t
Full source 
@[to_additive (attr := simp)]
lemma iUnion_smul_set (s : Set α) (t : Set β) : ⋃ a ∈ s, a • t = s • t := iUnion_image_left _
Union of Scalar Multiples Equals Pointwise Scalar Multiplication of Sets
Informal description
For any set $s$ of elements of type $\alpha$ and any set $t$ of elements of type $\beta$, the union over all $a \in s$ of the scalar multiples $a \bullet t$ is equal to the pointwise scalar multiplication $s \bullet t$. That is, \[ \bigcup_{a \in s} a \bullet t = s \bullet t. \]
Set.smul_set_iUnion theorem
(a : α) (s : ι → Set β) : a • ⋃ i, s i = ⋃ i, a • s i
Full source 
@[to_additive]
lemma smul_set_iUnion (a : α) (s : ι → Set β) : a • ⋃ i, s i = ⋃ i, a • s i :=
  image_iUnion
Scalar Multiplication Distributes Over Union of Sets
Informal description
For any scalar $a \in \alpha$ and any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\beta$, the scalar multiplication of $a$ with the union $\bigcup_{i} s_i$ equals the union of the scalar multiplications $\bigcup_{i} (a \bullet s_i)$. In symbols: $$ a \bullet \left( \bigcup_{i} s_i \right) = \bigcup_{i} (a \bullet s_i). $$
Set.smul_set_iUnion₂ theorem
(a : α) (s : ∀ i, κ i → Set β) : a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j
Full source 
@[to_additive]
lemma smul_set_iUnion₂ (a : α) (s : ∀ i, κ i → Set β) :
    a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j := image_iUnion₂ ..
Scalar Multiplication Distributes over Double Union of Sets
Informal description
For any scalar $a \in \alpha$ and any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\beta$, the scalar multiplication of $a$ with the double union $\bigcup_{i,j} s_{i,j}$ equals the double union of the scalar multiplications $\bigcup_{i,j} (a \bullet s_{i,j})$. In symbols: $$ a \bullet \left(\bigcup_{i,j} s_{i,j}\right) = \bigcup_{i,j} (a \bullet s_{i,j}). $$
Set.smul_set_sUnion theorem
(a : α) (S : Set (Set β)) : a • ⋃₀ S = ⋃ s ∈ S, a • s
Full source 
@[to_additive]
lemma smul_set_sUnion (a : α) (S : Set (Set β)) : a • ⋃₀ S = ⋃ s ∈ S, a • s := by
  rw [sUnion_eq_biUnion, smul_set_iUnion₂]
Scalar Multiplication Distributes Over Union of a Set of Sets
Informal description
For any scalar $a \in \alpha$ and any collection of sets $S \subseteq \mathcal{P}(\beta)$, the scalar multiplication of $a$ with the union $\bigcup_{s \in S} s$ equals the union of the scalar multiplications $\bigcup_{s \in S} (a \bullet s)$. In symbols: $$ a \bullet \left( \bigcup_{s \in S} s \right) = \bigcup_{s \in S} (a \bullet s). $$
Set.smul_set_iInter_subset theorem
(a : α) (t : ι → Set β) : a • ⋂ i, t i ⊆ ⋂ i, a • t i
Full source 
@[to_additive]
lemma smul_set_iInter_subset (a : α) (t : ι → Set β) : a • ⋂ i, t i ⊆ ⋂ i, a • t i :=
  image_iInter_subset ..
Scalar Multiplication Preserves Subset Relation with Intersection
Informal description
For any scalar $a \in \alpha$ and any indexed family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the scalar multiplication of $a$ with the intersection $\bigcap_{i \in \iota} t_i$ is contained in the intersection of the scalar multiplications $\bigcap_{i \in \iota} (a \bullet t_i)$. In symbols: $$ a \bullet \left(\bigcap_{i \in \iota} t_i\right) \subseteq \bigcap_{i \in \iota} (a \bullet t_i). $$
Set.smul_set_sInter_subset theorem
(a : α) (S : Set (Set β)) : a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s
Full source 
@[to_additive]
lemma smul_set_sInter_subset (a : α) (S : Set (Set β)) :
    a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s := image_sInter_subset ..
Scalar Multiplication Distributes Over Set Intersection (Subset Version)
Informal description
For any scalar $a \in \alpha$ and any collection of sets $S \subseteq \mathcal{P}(\beta)$, the scalar multiplication of the intersection $\bigcap S$ by $a$ is contained in the intersection of the scalar multiplications $\bigcap_{s \in S} (a \cdot s)$. In other words: \[ a \cdot \left( \bigcap S \right) \subseteq \bigcap_{s \in S} (a \cdot s) \]
Set.smul_set_iInter₂_subset theorem
(a : α) (t : ∀ i, κ i → Set β) : a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j
Full source 
@[to_additive]
lemma smul_set_iInter₂_subset (a : α) (t : ∀ i, κ i → Set β) :
    a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j := image_iInter₂_subset ..
Scalar Multiplication Preserves Double Intersection Inclusion
Informal description
For any scalar $a \in \alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i,j}$ in $\beta$, the scalar multiplication of the double intersection $\bigcap_{i,j} t_{i,j}$ by $a$ is contained in the double intersection of the scalar multiplications $\bigcap_{i,j} (a \cdot t_{i,j})$. In other words, \[ a \cdot \left( \bigcap_{i,j} t_{i,j} \right) \subseteq \bigcap_{i,j} (a \cdot t_{i,j}). \]
Set.iUnion_vsub_left_image theorem
: ⋃ a ∈ s, (a -ᵥ ·) '' t = s -ᵥ t
Full source 
lemma iUnion_vsub_left_image : ⋃ a ∈ s, (a -ᵥ ·) '' t = s -ᵥ t := iUnion_image_left _
Union of Left Scalar Subtraction Images Equals Scalar Subtraction of Sets
Informal description
For any set $s$ in a type with a scalar subtraction operation $-ᵥ$ and any set $t$, the union over all $a \in s$ of the images of $t$ under the function $(a -ᵥ \cdot)$ equals the scalar subtraction $s -ᵥ t$. In other words: \[ \bigcup_{a \in s} \{a -ᵥ b \mid b \in t\} = s -ᵥ t \]
Set.iUnion_vsub_right_image theorem
: ⋃ a ∈ t, (· -ᵥ a) '' s = s -ᵥ t
Full source 
lemma iUnion_vsub_right_image : ⋃ a ∈ t, (· -ᵥ a) '' s = s -ᵥ t := iUnion_image_right _
Union of Right Scalar Subtraction Images Equals Scalar Subtraction of Sets
Informal description
For any sets $s, t \subseteq \beta$ with a scalar subtraction operation $-ᵥ : \beta \rightarrow \beta \rightarrow \alpha$, the union over all $a \in t$ of the images $\{x -ᵥ a \mid x \in s\}$ equals the scalar subtraction of $s$ and $t$. In other words: \[ \bigcup_{a \in t} \{x -ᵥ a \mid x \in s\} = s -ᵥ t \]
Set.iUnion_vsub theorem
(s : ι → Set β) (t : Set β) : (⋃ i, s i) -ᵥ t = ⋃ i, s i -ᵥ t
Full source 
lemma iUnion_vsub (s : ι → Set β) (t : Set β) : (⋃ i, s i) -ᵥ t = ⋃ i, s i -ᵥ t :=
  image2_iUnion_left ..
Union Distributes over Scalar Subtraction: $(\bigcup_i s_i) -ᵥ t = \bigcup_i (s_i -ᵥ t)$
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$ and any set $t \subseteq \beta$, the scalar subtraction of the union $\bigcup_i s_i$ and $t$ equals the union of the scalar subtractions $s_i -ᵥ t$ for all $i \in \iota$. In symbols: $$ \left(\bigcup_{i} s_i\right) -ᵥ t = \bigcup_{i} (s_i -ᵥ t). $$
Set.vsub_iUnion theorem
(s : Set β) (t : ι → Set β) : (s -ᵥ ⋃ i, t i) = ⋃ i, s -ᵥ t i
Full source 
lemma vsub_iUnion (s : Set β) (t : ι → Set β) : (s -ᵥ ⋃ i, t i) = ⋃ i, s -ᵥ t i :=
  image2_iUnion_right ..
Scalar Subtraction Distributes over Union: $s -ᵥ \bigcup_i t_i = \bigcup_i (s -ᵥ t_i)$
Informal description
For any set $s \subseteq \beta$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the scalar subtraction of $s$ and the union $\bigcup_i t_i$ equals the union of the scalar subtractions $s -ᵥ t_i$ for all $i \in \iota$. In symbols: $$ s -ᵥ \left( \bigcup_{i} t_i \right) = \bigcup_{i} (s -ᵥ t_i). $$
Set.sUnion_vsub theorem
(S : Set (Set β)) (t : Set β) : ⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t
Full source 
lemma sUnion_vsub (S : Set (Set β)) (t : Set β) : ⋃₀ S⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t :=
  image2_sUnion_left ..
Scalar Subtraction Distributes Over Union of Sets
Informal description
For any family of sets $S$ in $\beta$ and any set $t \subseteq \beta$, the scalar subtraction of the union $\bigcup S$ by $t$ equals the union over all $s \in S$ of the scalar subtractions $s -ᵥ t$. In symbols: $$ \left(\bigcup S\right) -ᵥ t = \bigcup_{s \in S} (s -ᵥ t) $$
Set.vsub_sUnion theorem
(s : Set β) (T : Set (Set β)) : s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t
Full source 
lemma vsub_sUnion (s : Set β) (T : Set (Set β)) : s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t :=
  image2_sUnion_right ..
Scalar Subtraction Distributes Over Union of Sets
Informal description
For any set $s \subseteq \beta$ and any family of sets $T \subseteq \mathcal{P}(\beta)$, the scalar subtraction of $s$ by the union of all sets in $T$ is equal to the union over all $t \in T$ of the scalar subtractions of $s$ by $t$. In symbols: $$ s -ᵥ \left( \bigcup T \right) = \bigcup_{t \in T} (s -ᵥ t) $$
Set.iUnion₂_vsub theorem
(s : ∀ i, κ i → Set β) (t : Set β) : (⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t
Full source 
lemma iUnion₂_vsub (s : ∀ i, κ i → Set β) (t : Set β) :
    (⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t := image2_iUnion₂_left ..
Double Union Scalar Subtraction Identity: $(\bigcup_i \bigcup_j s_{i,j}) -ᵥ t = \bigcup_i \bigcup_j (s_{i,j} -ᵥ t)$
Informal description
For any indexed family of sets $s_{i,j} \subseteq \beta$ (where $i$ and $j$ are indices) and any set $t \subseteq \beta$, the scalar subtraction of the double union $\bigcup_i \bigcup_j s_{i,j}$ by $t$ equals the double union of the scalar subtractions $s_{i,j} -ᵥ t$. In symbols: $$ \left(\bigcup_i \bigcup_j s_{i,j}\right) -ᵥ t = \bigcup_i \bigcup_j (s_{i,j} -ᵥ t) $$
Set.vsub_iUnion₂ theorem
(s : Set β) (t : ∀ i, κ i → Set β) : (s -ᵥ ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s -ᵥ t i j
Full source 
lemma vsub_iUnion₂ (s : Set β) (t : ∀ i, κ i → Set β) :
    (s -ᵥ ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s -ᵥ t i j := image2_iUnion₂_right ..
Scalar Subtraction Distributes Over Doubly-Indexed Union of Sets
Informal description
For any set $s \subseteq \beta$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\beta$, the scalar subtraction of $s$ by the union $\bigcup_{i,j} t_{i,j}$ is equal to the union over all $i \in \iota$ and $j \in \kappa_i$ of the scalar subtractions $s -ᵥ t_{i,j}$. In symbols: $$ s -ᵥ \left( \bigcup_{i,j} t_{i,j} \right) = \bigcup_{i,j} (s -ᵥ t_{i,j}). $$
Set.iInter_vsub_subset theorem
(s : ι → Set β) (t : Set β) : (⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t
Full source 
lemma iInter_vsub_subset (s : ι → Set β) (t : Set β) : (⋂ i, s i) -ᵥ t(⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t :=
  image2_iInter_subset_left ..
Intersection Scalar Subtraction Subset Property: $(\bigcap_i s_i) -ᵥ t \subseteq \bigcap_i (s_i -ᵥ t)$
Informal description
For any indexed family of sets $\{s_i\}_{i \in \iota}$ in $\beta$ and any set $t \subseteq \beta$, the scalar subtraction of the intersection $\bigcap_i s_i$ by $t$ is contained in the intersection of the scalar subtractions $s_i -ᵥ t$ for each $i$. In symbols: $$ \left(\bigcap_{i} s_i\right) -ᵥ t \subseteq \bigcap_{i} (s_i -ᵥ t). $$
Set.vsub_iInter_subset theorem
(s : Set β) (t : ι → Set β) : (s -ᵥ ⋂ i, t i) ⊆ ⋂ i, s -ᵥ t i
Full source 
lemma vsub_iInter_subset (s : Set β) (t : ι → Set β) : (s -ᵥ ⋂ i, t i) ⊆ ⋂ i, s -ᵥ t i :=
  image2_iInter_subset_right ..
Scalar Subtraction of Set by Intersection is Subset of Intersection of Scalar Subtractions
Informal description
For any set $s \subseteq \beta$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the scalar subtraction of $s$ by the intersection $\bigcap_i t_i$ is contained in the intersection over $i$ of the scalar subtractions $s -ᵥ t_i$. In symbols: $$ s -ᵥ \left( \bigcap_i t_i \right) \subseteq \bigcap_i (s -ᵥ t_i). $$
Set.sInter_vsub_subset theorem
(S : Set (Set β)) (t : Set β) : ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t
Full source 
lemma sInter_vsub_subset (S : Set (Set β)) (t : Set β) : ⋂₀ S⋂₀ S -ᵥ t⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t :=
  image2_sInter_subset_left ..
Intersection Preserved Under Scalar Subtraction with Fixed Set
Informal description
For a collection $S$ of subsets of a type $\beta$ and a subset $t \subseteq \beta$, the scalar subtraction of the intersection $\bigcap S$ and $t$ is contained in the intersection of the scalar subtractions of each $s \in S$ and $t$, i.e., $$ \left(\bigcap S\right) -ᵥ t \subseteq \bigcap_{s \in S} (s -ᵥ t). $$
Set.vsub_sInter_subset theorem
(s : Set β) (T : Set (Set β)) : s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t
Full source 
lemma vsub_sInter_subset (s : Set β) (T : Set (Set β)) : s -ᵥ ⋂₀ Ts -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t :=
  image2_sInter_subset_right ..
Scalar Subtraction Preserves Intersection Containment
Informal description
For any set $s$ of elements of type $\beta$ and any collection $T$ of subsets of $\beta$, the scalar subtraction of $s$ by the intersection of all sets in $T$ is contained in the intersection of the scalar subtractions of $s$ by each individual set $t \in T$. In symbols: $$ s -ᵥ \bigcap T \subseteq \bigcap_{t \in T} (s -ᵥ t) $$
Set.iInter₂_vsub_subset theorem
(s : ∀ i, κ i → Set β) (t : Set β) : (⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t
Full source 
lemma iInter₂_vsub_subset (s : ∀ i, κ i → Set β) (t : Set β) :
    (⋂ i, ⋂ j, s i j) -ᵥ t(⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t := image2_iInter₂_subset_left ..
Double Intersection Scalar Subtraction Subset Property
Informal description
For a family of sets $(s_{i,j})_{i,j}$ indexed by $i$ and $j$ in $\beta$, and a set $t \subseteq \beta$, the scalar subtraction of the double intersection $\bigcap_i \bigcap_j s_{i,j}$ by $t$ is contained in the double intersection of the scalar subtractions $s_{i,j} -ᵥ t$, i.e., $$ \left(\bigcap_i \bigcap_j s_{i,j}\right) -ᵥ t \subseteq \bigcap_i \bigcap_j (s_{i,j} -ᵥ t). $$
Set.vsub_iInter₂_subset theorem
(s : Set β) (t : ∀ i, κ i → Set β) : s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j
Full source 
lemma vsub_iInter₂_subset (s : Set β) (t : ∀ i, κ i → Set β) :
    s -ᵥ ⋂ i, ⋂ j, t i js -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j := image2_iInter₂_subset_right ..
Inclusion of Scalar Subtraction with Indexed Intersection
Informal description
For any set $s$ of elements in type $\beta$ and any indexed family of sets $t_{i,j}$ in $\beta$, the scalar subtraction of $s$ by the intersection of all $t_{i,j}$ is contained in the intersection of all scalar subtractions of $s$ by each $t_{i,j}$. In symbols: $$ s -ᵥ \bigcap_{i,j} t_{i,j} \subseteq \bigcap_{i,j} (s -ᵥ t_{i,j}) $$