Documentation

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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)⁻¹ = sS, s⁻¹
@[simp]
theorem Set.sInter_neg {α : Type u_2} [Neg α] (S : Set (Set α)) :
-⋂₀ S = sS, -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)⁻¹ = sS, s⁻¹
@[simp]
theorem Set.sUnion_neg {α : Type u_2} [Neg α] (S : Set (Set α)) :
-⋃₀ S = sS, -s

Set addition/multiplication #

theorem Set.iUnion_mul_left_image {α : Type u_2} [Mul α] {s t : Set α} :
as, (fun (x : α) => a * x) '' t = s * t
theorem Set.iUnion_add_left_image {α : Type u_2} [Add α] {s t : Set α} :
as, (fun (x : α) => a + x) '' t = s + t
theorem Set.iUnion_mul_right_image {α : Type u_2} [Mul α] {s t : Set α} :
at, (fun (x : α) => x * a) '' s = s * t
theorem Set.iUnion_add_right_image {α : Type u_2} [Add α] {s t : Set α} :
at, (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 = sS, s * t
theorem Set.sUnion_add {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) :
⋃₀ S + t = sS, s + t
theorem Set.mul_sUnion {α : Type u_2} [Mul α] (s : Set α) (T : Set (Set α)) :
s * ⋃₀ T = tT, s * t
theorem Set.add_sUnion {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) :
s + ⋃₀ T = tT, s + t
theorem Set.iUnion₂_mul {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet α) :
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 : ι) → κ iSet α) :
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 tT, s * t
theorem Set.add_sInter_subset {α : Type u_2} [Add α] (s : Set α) (T : Set (Set α)) :
s + ⋂₀ T tT, s + t
theorem Set.sInter_mul_subset {α : Type u_2} [Mul α] (S : Set (Set α)) (t : Set α) :
⋂₀ S * t sS, s * t
theorem Set.sInter_add_subset {α : Type u_2} [Add α] (S : Set (Set α)) (t : Set α) :
⋂₀ S + t sS, s + t
theorem Set.iInter₂_mul_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Mul α] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet α) :
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 : ι) → κ iSet α) :
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 α} :
as, (fun (x : α) => a / x) '' t = s / t
theorem Set.iUnion_sub_left_image {α : Type u_2} [Sub α] {s t : Set α} :
as, (fun (x : α) => a - x) '' t = s - t
theorem Set.iUnion_div_right_image {α : Type u_2} [Div α] {s t : Set α} :
at, (fun (x : α) => x / a) '' s = s / t
theorem Set.iUnion_sub_right_image {α : Type u_2} [Sub α] {s t : Set α} :
at, (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 = sS, s / t
theorem Set.sUnion_sub {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) :
⋃₀ S - t = sS, s - t
theorem Set.div_sUnion {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) :
s / ⋃₀ T = tT, s / t
theorem Set.sub_sUnion {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) :
s - ⋃₀ T = tT, s - t
theorem Set.iUnion₂_div {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet α) :
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 : ι) → κ iSet α) :
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 sS, s / t
theorem Set.sInter_sub_subset {α : Type u_2} [Sub α] (S : Set (Set α)) (t : Set α) :
⋂₀ S - t sS, s - t
theorem Set.div_sInter_subset {α : Type u_2} [Div α] (s : Set α) (T : Set (Set α)) :
s / ⋂₀ T tT, s / t
theorem Set.sub_sInter_subset {α : Type u_2} [Sub α] (s : Set α) (T : Set (Set α)) :
s - ⋂₀ T tT, s - t
theorem Set.iInter₂_div_subset {α : Type u_2} {ι : Sort u_5} {κ : ιSort u_6} [Div α] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet α) :
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 : ι) → κ iSet α) :
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 β} :
as, a t = s t
theorem Set.iUnion_vadd_left_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
as, a +ᵥ t = s +ᵥ t
theorem Set.iUnion_smul_right_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} :
at, (fun (x : α) => x a) '' s = s t
theorem Set.iUnion_vadd_right_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} :
at, (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 = sS, s t
theorem Set.sUnion_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] (S : Set (Set α)) (t : Set β) :
⋃₀ S +ᵥ t = sS, s +ᵥ t
theorem Set.smul_sUnion {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (T : Set (Set β)) :
s ⋃₀ T = tT, s t
theorem Set.vadd_sUnion {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (T : Set (Set β)) :
s +ᵥ ⋃₀ T = tT, s +ᵥ t
theorem Set.iUnion₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet β) :
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 : ι) → κ iSet β) :
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 sS, s t
theorem Set.sInter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (S : Set (Set α)) (t : Set β) :
⋂₀ S +ᵥ t sS, s +ᵥ t
theorem Set.smul_sInter_subset {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (T : Set (Set β)) :
s ⋂₀ T tT, s t
theorem Set.vadd_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (T : Set (Set β)) :
s +ᵥ ⋂₀ T tT, s +ᵥ t
theorem Set.iInter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (s : (i : ι) → κ iSet α) (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 : ι) → κ iSet α) (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 : ι) → κ iSet β) :
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 : ι) → κ iSet β) :
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 β) :
as, a t = s t
@[simp]
theorem Set.iUnion_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (t : Set β) :
as, 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 : ι) → κ iSet β) :
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 : ι) → κ iSet β) :
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 = sS, a s
theorem Set.vadd_set_sUnion {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (S : Set (Set β)) :
a +ᵥ ⋃₀ S = sS, 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 sS, a s
theorem Set.vadd_set_sInter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (S : Set (Set β)) :
a +ᵥ ⋂₀ S sS, a +ᵥ s
theorem Set.smul_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [SMul α β] (a : α) (t : (i : ι) → κ iSet β) :
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 : ι) → κ iSet β) :
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 β} :
as, (fun (x : β) => a -ᵥ x) '' t = s -ᵥ t
theorem Set.iUnion_vsub_right_image {α : Type u_2} {β : Type u_3} [VSub α β] {s t : Set β} :
at, (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 = sS, s -ᵥ t
theorem Set.vsub_sUnion {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) :
s -ᵥ ⋃₀ T = tT, s -ᵥ t
theorem Set.iUnion₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : (i : ι) → κ iSet β) (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 : ι) → κ iSet β) :
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 sS, s -ᵥ t
theorem Set.vsub_sInter_subset {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (T : Set (Set β)) :
s -ᵥ ⋂₀ T tT, s -ᵥ t
theorem Set.iInter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ιSort u_6} [VSub α β] (s : (i : ι) → κ iSet β) (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 : ι) → κ iSet β) :
s -ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⋂ (i : ι), ⋂ (j : κ i), s -ᵥ t i j