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

@[simp]

theorem Set.iInter_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ι → Set α) : (⋂ (i : ι), s i)⁻¹ = ⋂ (i : ι), (s i)⁻¹

@[simp]

theorem Set.iInter_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ι → Set α) : -⋂ (i : ι), s i = ⋂ (i : ι), -s i

@[simp]

theorem Set.sInter_inv {α : Type u_2} [Inv α] (S : Set (Set α)) : (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹

@[simp]

theorem Set.sInter_neg {α : Type u_2} [Neg α] (S : Set (Set α)) : -⋂₀ S = ⋂ s ∈ S, -s

@[simp]

theorem Set.iUnion_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ι → Set α) : (⋃ (i : ι), s i)⁻¹ = ⋃ (i : ι), (s i)⁻¹

@[simp]

theorem Set.iUnion_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ι → Set α) : -⋃ (i : ι), s i = ⋃ (i : ι), -s i

@[simp]

theorem Set.sUnion_inv {α : Type u_2} [Inv α] (S : Set (Set α)) : (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹

@[simp]

theorem Set.sUnion_neg {α : Type u_2} [Neg α] (S : Set (Set α)) : -⋃₀ S = ⋃ s ∈ S, -s

Set addition/multiplication

theorem Set.iUnion_mul_left_image {α : Type u_2} [Mul α] {s t : Set α} : ⋃ a ∈ s, (fun (x : α) => a * x) '' t = s * t

theorem Set.iUnion_add_left_image {α : Type u_2} [Add α] {s t : Set α} : ⋃ a ∈ s, (fun (x : α) => a + x) '' t = s + t

theorem Set.iUnion_mul_right_image {α : Type u_2} [Mul α] {s t : Set α} : ⋃ a ∈ t, (fun (x : α) => x * a) '' s = s * t

theorem Set.iUnion_add_right_image {α : Type u_2} [Add α] {s t : Set α} : ⋃ a ∈ t, (fun (x : α) => x + a) '' s = s + t

theorem Set.iUnion_mul {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) * t = ⋃ (i : ι), s i * t

theorem Set.iUnion_add {α : Type u_2} {ι : Sort u_5} [Add α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) + t = ⋃ (i : ι), s i + t

theorem Set.mul_iUnion {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ι → Set α) : s * ⋃ (i : ι), t i = ⋃ (i : ι), s * t i

theorem Set.add_iUnion {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ι → Set α) : s + ⋃ (i : ι), t i = ⋃ (i : ι), s + t i

theorem Set.sUnion_mul {α : Type u_2} [Mul α] (S : Set (Set α)) (t : Set α) : ⋃₀ S * t = ⋃ s ∈ S, s * t

theorem Set.sUnion_add {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) : ⋃₀ S + t = ⋃ s ∈ S, s + t

theorem Set.mul_sUnion {α : Type u_2} [Mul α] (s : Set α) (T : Set (Set α)) : s * ⋃₀ T = ⋃ t ∈ T, s * t

theorem Set.add_sUnion {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) : s + ⋃₀ T = ⋃ t ∈ T, s + t

theorem Set.iUnion₂_mul {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) * t = ⋃ (i : ι), ⋃ (j : κ i), s i j * t

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

theorem Set.mul_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ i → Set α) : s * ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s * t i j

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

theorem Set.iInter_mul_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) * t ⊆ ⋂ (i : ι), s i * t

theorem Set.iInter_add_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) + t ⊆ ⋂ (i : ι), s i + t

theorem Set.mul_iInter_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ι → Set α) : s * ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s * t i

theorem Set.add_iInter_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ι → Set α) : s + ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s + t i

theorem Set.mul_sInter_subset {α : Type u_2} [Mul α] (s : Set α) (T : Set (Set α)) : s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t

theorem Set.add_sInter_subset {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) : s + ⋂₀ T ⊆ ⋂ t ∈ T, s + t

theorem Set.sInter_mul_subset {α : Type u_2} [Mul α] (S : Set (Set α)) (t : Set α) : ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t

theorem Set.sInter_add_subset {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) : ⋂₀ S + t ⊆ ⋂ s ∈ S, s + t

theorem Set.iInter₂_mul_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) * t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j * t

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

theorem Set.mul_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ i → Set α) : s * ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s * t i j

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

Set subtraction/division

theorem Set.iUnion_div_left_image {α : Type u_2} [Div α] {s t : Set α} : ⋃ a ∈ s, (fun (x : α) => a / x) '' t = s / t

theorem Set.iUnion_sub_left_image {α : Type u_2} [Sub α] {s t : Set α} : ⋃ a ∈ s, (fun (x : α) => a - x) '' t = s - t

theorem Set.iUnion_div_right_image {α : Type u_2} [Div α] {s t : Set α} : ⋃ a ∈ t, (fun (x : α) => x / a) '' s = s / t

theorem Set.iUnion_sub_right_image {α : Type u_2} [Sub α] {s t : Set α} : ⋃ a ∈ t, (fun (x : α) => x - a) '' s = s - t

theorem Set.iUnion_div {α : Type u_2} {ι : Sort u_5} [Div α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) / t = ⋃ (i : ι), s i / t

theorem Set.iUnion_sub {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) - t = ⋃ (i : ι), s i - t

theorem Set.div_iUnion {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ι → Set α) : s / ⋃ (i : ι), t i = ⋃ (i : ι), s / t i

theorem Set.sub_iUnion {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ι → Set α) : s - ⋃ (i : ι), t i = ⋃ (i : ι), s - t i

theorem Set.sUnion_div {α : Type u_2} [Div α] (S : Set (Set α)) (t : Set α) : ⋃₀ S / t = ⋃ s ∈ S, s / t

theorem Set.sUnion_sub {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) : ⋃₀ S - t = ⋃ s ∈ S, s - t

theorem Set.div_sUnion {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) : s / ⋃₀ T = ⋃ t ∈ T, s / t

theorem Set.sub_sUnion {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) : s - ⋃₀ T = ⋃ t ∈ T, s - t

theorem Set.iUnion₂_div {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) / t = ⋃ (i : ι), ⋃ (j : κ i), s i j / t

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

theorem Set.div_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : Set α) (t : (i : ι) → κ i → Set α) : s / ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s / t i j

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

theorem Set.iInter_div_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) / t ⊆ ⋂ (i : ι), s i / t

theorem Set.iInter_sub_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) - t ⊆ ⋂ (i : ι), s i - t

theorem Set.div_iInter_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ι → Set α) : s / ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s / t i

theorem Set.sub_iInter_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ι → Set α) : s - ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s - t i

theorem Set.sInter_div_subset {α : Type u_2} [Div α] (S : Set (Set α)) (t : Set α) : ⋂₀ S / t ⊆ ⋂ s ∈ S, s / t

theorem Set.sInter_sub_subset {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) : ⋂₀ S - t ⊆ ⋂ s ∈ S, s - t

theorem Set.div_sInter_subset {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) : s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t

theorem Set.sub_sInter_subset {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) : s - ⋂₀ T ⊆ ⋂ t ∈ T, s - t

theorem Set.iInter₂_div_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) / t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j / t

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

theorem Set.div_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : Set α) (t : (i : ι) → κ i → Set α) : s / ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s / t i j

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

Translation/scaling of sets

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Set.sInter_smul_subset {α : Type u_2} {β : Type u_3} [SMul α β] (S : Set (Set α)) (t : Set β) : ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t

theorem Set.sInter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (S : Set (Set α)) (t : Set β) : ⋂₀ S +ᵥ t ⊆ ⋂ s ∈ S, s +ᵥ t

theorem Set.smul_sInter_subset {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (T : Set (Set β)) : s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t

theorem Set.vadd_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (T : Set (Set β)) : s +ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s +ᵥ t

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

theorem Set.smul_set_sInter_subset {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (S : Set (Set β)) : a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s

theorem Set.vadd_set_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (S : Set (Set β)) : a +ᵥ ⋂₀ S ⊆ ⋂ s ∈ S, a +ᵥ s

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

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

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

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

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

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

theorem Set.sUnion_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (S : Set (Set β)) (t : Set β) : ⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t

theorem Set.vsub_sUnion {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) : s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t

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

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

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

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

theorem Set.sInter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] (S : Set (Set β)) (t : Set β) : ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t

theorem Set.vsub_sInter_subset {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) : s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t

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

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