The set lattice and (pre)images of functions

This file contains lemmas on the interaction between the indexed union/intersection of sets and the image and preimage operations: Set.image, Set.preimage, Set.image2, Set.kernImage. It also covers Set.MapsTo, Set.InjOn, Set.SurjOn, Set.BijOn.

In order to accommodate Set.image2, the file includes results on union/intersection in products.

Naming convention

In lemma names,

• ⋃ i, s i is called iUnion
• ⋂ i, s i is called iInter
• ⋃ i j, s i j is called iUnion₂. This is an iUnion inside an iUnion.
• ⋂ i j, s i j is called iInter₂. This is an iInter inside an iInter.
• ⋃ i ∈ s, t i is called biUnion for "bounded iUnion". This is the special case of iUnion₂ where j : i ∈ s.
• ⋂ i ∈ s, t i is called biInter for "bounded iInter". This is the special case of iInter₂ where j : i ∈ s.

Notation

• ⋃: Set.iUnion
• ⋂: Set.iInter
• ⋃₀: Set.sUnion
• ⋂₀: Set.sInter

theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (image f) (preimage f)

theorem Set.preimage_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (preimage f) (kernImage f)

theorem Set.kernImage_mono {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (kernImage f)

theorem Set.kernImage_eq_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : kernImage f s = (f '' sᶜ)ᶜ

theorem Set.kernImage_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : kernImage f sᶜ = (f '' s)ᶜ

theorem Set.kernImage_empty {α : Type u_1} {β : Type u_2} {f : α → β} : kernImage f ∅ = (range f)ᶜ

theorem Set.kernImage_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

theorem Set.compl_range_subset_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : (range f)ᶜ ⊆ kernImage f s

theorem Set.kernImage_union_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

theorem Set.kernImage_preimage_union {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

theorem Set.image_projection_prod {ι : Type u_9} {α : ι → Type u_10} {v : (i : ι) → Set (α i)} (hv : (univ.pi v).Nonempty) (i : ι) : (fun (x : (i : ι) → α i) => x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) => x k) ⁻¹' v k = v i

Bounded unions and intersections

Lemmas about Set.MapsTo

@[simp]

theorem Set.mapsTo_sUnion {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : α → β} : MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, MapsTo f s t

@[simp]

theorem Set.mapsTo_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β} {f : α → β} : MapsTo f (⋃ (i : ι), s i) t ↔ ∀ (i : ι), MapsTo f (s i) t

theorem Set.mapsTo_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β} : MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), MapsTo f (s i j) t

theorem Set.mapsTo_iUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), MapsTo f (s i) (t i)) : MapsTo f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem Set.mapsTo_iUnion₂_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), MapsTo f (s i j) (t i j)) : MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)

@[simp]

theorem Set.mapsTo_sInter {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β} : MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, MapsTo f s t

@[simp]

theorem Set.mapsTo_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β} : MapsTo f s (⋂ (i : ι), t i) ↔ ∀ (i : ι), MapsTo f s (t i)

theorem Set.mapsTo_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β} : MapsTo f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

theorem Set.mapsTo_iInter_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), MapsTo f (s i) (t i)) : MapsTo f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

theorem Set.mapsTo_iInter₂_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), MapsTo f (s i j) (t i j)) : MapsTo f (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)

theorem Set.image_iInter_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (f : α → β) : f '' ⋂ (i : ι), s i ⊆ ⋂ (i : ι), f '' s i

theorem Set.image_iInter₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (f : α → β) : f '' ⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), f '' s i j

theorem Set.image_sInter_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (f : α → β) : f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

theorem Set.image2_sInter_right_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Set α) (S : Set (Set β)) (f : α → β → γ) : image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

theorem Set.image2_sInter_left_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Set (Set α)) (t : Set β) (f : α → β → γ) : image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

restrictPreimage

theorem Set.injective_iff_injective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β} (hU : iUnion U = univ) : Function.Injective f ↔ ∀ (i : ι), Function.Injective ((U i).restrictPreimage f)

theorem Set.surjective_iff_surjective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β} (hU : iUnion U = univ) : Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f)

theorem Set.bijective_iff_bijective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β} (hU : iUnion U = univ) : Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)

InjOn

theorem Set.InjOn.image_iInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {f : α → β} (h : InjOn f (⋃ (i : ι), s i)) : f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

theorem Set.InjOn.image_biInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {p : ι → Prop} {s : (i : ι) → p i → Set α} (hp : ∃ (i : ι), p i) {f : α → β} (h : InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)) : f '' ⋂ (i : ι), ⋂ (hi : p i), s i hi = ⋂ (i : ι), ⋂ (hi : p i), f '' s i hi

theorem Set.image_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} (hf : Function.Bijective f) (s : ι → Set α) : f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i

theorem Set.image_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β} (hf : Function.Bijective f) (s : (i : ι) → κ i → Set α) : f '' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f '' s i j

theorem Set.inj_on_iUnion_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) {f : α → β} (hf : ∀ (i : ι), InjOn f (s i)) : InjOn f (⋃ (i : ι), s i)

SurjOn

theorem Set.surjOn_sUnion {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β} (H : ∀ t ∈ T, SurjOn f s t) : SurjOn f s (⋃₀ T)

theorem Set.surjOn_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), SurjOn f s (t i)) : SurjOn f s (⋃ (i : ι), t i)

theorem Set.surjOn_iUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), SurjOn f (s i) (t i)) : SurjOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem Set.surjOn_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), SurjOn f s (t i j)) : SurjOn f s (⋃ (i : ι), ⋃ (j : κ i), t i j)

theorem Set.surjOn_iUnion₂_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), SurjOn f (s i j) (t i j)) : SurjOn f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)

theorem Set.surjOn_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {t : Set β} {f : α → β} (H : ∀ (i : ι), SurjOn f (s i) t) (Hinj : InjOn f (⋃ (i : ι), s i)) : SurjOn f (⋂ (i : ι), s i) t

theorem Set.surjOn_iInter_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), SurjOn f (s i) (t i)) (Hinj : InjOn f (⋃ (i : ι), s i)) : SurjOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

BijOn

theorem Set.bijOn_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), BijOn f (s i) (t i)) (Hinj : InjOn f (⋃ (i : ι), s i)) : BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem Set.bijOn_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [hi : Nonempty ι] {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), BijOn f (s i) (t i)) (Hinj : InjOn f (⋃ (i : ι), s i)) : BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

theorem Set.bijOn_iUnion_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), BijOn f (s i) (t i)) : BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem Set.bijOn_iInter_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} (hs : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), BijOn f (s i) (t i)) : BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

image, preimage

theorem Set.image_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set α} : f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i

theorem Set.image_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β) (s : (i : ι) → κ i → Set α) : f '' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f '' s i j

theorem Set.univ_subtype {α : Type u_1} {p : α → Prop} : univ = ⋃ (x : α), ⋃ (h : p x), {⟨x, h⟩}

theorem Set.range_eq_iUnion {α : Type u_1} {ι : Sort u_9} (f : ι → α) : range f = ⋃ (i : ι), {f i}

theorem Set.image_eq_iUnion {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s = ⋃ i ∈ s, {f i}

theorem Set.biUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β} : ⋃ x ∈ range f, g x = ⋃ (y : ι), g (f y)

@[simp]

theorem Set.iUnion_iUnion_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β} : ⋃ (x : α), ⋃ (y : ι), ⋃ (_ : f y = x), g x = ⋃ (y : ι), g (f y)

theorem Set.biInter_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β} : ⋂ x ∈ range f, g x = ⋂ (y : ι), g (f y)

@[simp]

theorem Set.iInter_iInter_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β} : ⋂ (x : α), ⋂ (y : ι), ⋂ (_ : f y = x), g x = ⋂ (y : ι), g (f y)

theorem Set.biUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β} : ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y)

theorem Set.biInter_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β} : ⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y)

theorem Set.biUnion_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) : ⋃ c ∈ image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g (f a b)

theorem Set.biInter_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) : ⋂ c ∈ image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g (f a b)

theorem Set.iUnion_inter_iUnion {α : Type u_1} {ι : Sort u_9} {κ : Sort u_10} (f : ι → Set α) (g : κ → Set α) : (⋃ (i : ι), f i) ∩ ⋃ (j : κ), g j = ⋃ (i : ι), ⋃ (j : κ), f i ∩ g j

theorem Set.iInter_union_iInter {α : Type u_1} {ι : Sort u_9} {κ : Sort u_10} (f : ι → Set α) (g : κ → Set α) : (⋂ (i : ι), f i) ∪ ⋂ (j : κ), g j = ⋂ (i : ι), ⋂ (j : κ), f i ∪ g j

theorem Set.iUnion₂_inter_iUnion₂ {α : Type u_1} {ι₁ : Sort u_9} {κ₁ : Sort u_10} {ι₂ : ι₁ → Sort u_11} {k₂ : κ₁ → Sort u_12} (f : (i₁ : ι₁) → ι₂ i₁ → Set α) (g : (j₁ : κ₁) → k₂ j₁ → Set α) : (⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), f i₁ i₂) ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂ = ⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂

theorem Set.iInter₂_union_iInter₂ {α : Type u_1} {ι₁ : Sort u_9} {κ₁ : Sort u_10} {ι₂ : ι₁ → Sort u_11} {k₂ : κ₁ → Sort u_12} (f : (i₁ : ι₁) → ι₂ i₁ → Set α) (g : (j₁ : κ₁) → k₂ j₁ → Set α) : (⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), f i₁ i₂) ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂ = ⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂

theorem Set.biUnion_inter_of_pairwise_disjoint {α : Type u_1} {ι : Type u_9} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) (s t : Set ι) : ⋃ i ∈ s ∩ t, f i = (⋃ i ∈ s, f i) ∩ ⋃ i ∈ t, f i

theorem Set.biUnion_iInter_of_pairwise_disjoint {α : Type u_1} {ι : Type u_9} {κ : Type u_10} [hκ : Nonempty κ] {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) (s : κ → Set ι) : ⋃ i ∈ ⋂ (j : κ), s j, f i = ⋂ (j : κ), ⋃ i ∈ s j, f i

theorem Set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (preimage f)

@[simp]

theorem Set.preimage_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β} : f ⁻¹' ⋃ (i : ι), s i = ⋃ (i : ι), f ⁻¹' s i

theorem Set.preimage_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β} {s : (i : ι) → κ i → Set β} : f ⁻¹' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f ⁻¹' s i j

theorem Set.image_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set α)} : f '' ⋃₀ s = ⋃₀ (image f '' s)

@[simp]

theorem Set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

theorem Set.preimage_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β} : f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i

theorem Set.preimage_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β} {s : (i : ι) → κ i → Set β} : f ⁻¹' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f ⁻¹' s i j

@[simp]

theorem Set.preimage_sInter {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t

@[simp]

theorem Set.biUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

theorem Set.biUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) : ⋃ y ∈ range f, f ⁻¹' {y} = univ

theorem Set.prod_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} : s ×ˢ ⋃ (i : ι), t i = ⋃ (i : ι), s ×ˢ t i

theorem Set.prod_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} : s ×ˢ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s ×ˢ t i j

theorem Set.prod_sUnion {α : Type u_1} {β : Type u_2} {s : Set α} {C : Set (Set β)} : s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) => s ×ˢ t) '' C)

theorem Set.iUnion_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β} : (⋃ (i : ι), s i) ×ˢ t = ⋃ (i : ι), s i ×ˢ t

theorem Set.iUnion₂_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set β} : (⋃ (i : ι), ⋃ (j : κ i), s i j) ×ˢ t = ⋃ (i : ι), ⋃ (j : κ i), s i j ×ˢ t

theorem Set.sUnion_prod_const {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {t : Set β} : ⋃₀ C ×ˢ t = ⋃₀ ((fun (s : Set α) => s ×ˢ t) '' C)

theorem Set.iUnion_prod {ι : Type u_9} {ι' : Type u_10} {α : Type u_11} {β : Type u_12} (s : ι → Set α) (t : ι' → Set β) : ⋃ (x : ι × ι'), s x.1 ×ˢ t x.2 = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i

theorem Set.iUnion_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α) : ⋃ (x : β × γ), f x = ⋃ (i : β), ⋃ (j : γ), f (i, j)

Analogue of iSup_prod for sets.

theorem Set.iUnion_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) : ⋃ (x : α), s x ×ˢ t x = (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x

theorem Set.biUnion_prod {δ : Type u_4} {α : Type u_9} {β : Type u_10} {γ : Type u_11} (s : Set α) (t : Set β) (f : α → Set γ) (g : β → Set δ) : ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x

theorem Set.biUnion_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set β) (t : Set γ) (f : β × γ → Set α) : ⋃ x ∈ s ×ˢ t, f x = ⋃ i ∈ s, ⋃ j ∈ t, f (i, j)

Analogue of biSup_prod for sets.

theorem Set.iInter_prod_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (t : ι → Set β) : (⋂ (i : ι), s i) ×ˢ ⋂ (i : ι), t i = ⋂ (i : ι), s i ×ˢ t i

theorem Set.sInter_prod_sInter_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (T : Set (Set β)) : ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

theorem Set.sInter_prod_sInter {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) : ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

theorem Set.sInter_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) : ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

theorem Set.prod_sInter {α : Type u_1} {β : Type u_2} {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) : s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

theorem Set.prod_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} [hι : Nonempty ι] : s ×ˢ ⋂ (i : ι), t i = ⋂ (i : ι), s ×ˢ t i

theorem Set.image2_eq_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

The Set.image2 version of Set.image_eq_iUnion

theorem Set.iUnion_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β} : ⋃ a ∈ s, f a '' t = image2 f s t

theorem Set.iUnion_image_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β} : ⋃ b ∈ t, (fun (x : α) => f x b) '' s = image2 f s t

theorem Set.image2_iUnion_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : ι → Set α) (t : Set β) : image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), image2 f (s i) t

theorem Set.image2_iUnion_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : Set α) (t : ι → Set β) : image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), image2 f s (t i)

theorem Set.image2_sUnion_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (S : Set (Set α)) (t : Set β) : image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

theorem Set.image2_sUnion_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (T : Set (Set β)) : image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

theorem Set.image2_iUnion₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : (i : ι) → κ i → Set α) (t : Set β) : image2 f (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), image2 f (s i j) t

theorem Set.image2_iUnion₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : Set α) (t : (i : ι) → κ i → Set β) : image2 f s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), image2 f s (t i j)

theorem Set.image2_iInter_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : ι → Set α) (t : Set β) : image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), image2 f (s i) t

theorem Set.image2_iInter_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : Set α) (t : ι → Set β) : image2 f s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), image2 f s (t i)

theorem Set.image2_iInter₂_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : (i : ι) → κ i → Set α) (t : Set β) : image2 f (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⊆ ⋂ (i : ι), ⋂ (j : κ i), image2 f (s i j) t

theorem Set.image2_iInter₂_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : Set α) (t : (i : ι) → κ i → Set β) : image2 f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ⊆ ⋂ (i : ι), ⋂ (j : κ i), image2 f s (t i j)

theorem Set.image2_sInter_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (S : Set (Set α)) (t : Set β) : image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

theorem Set.image2_sInter_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (T : Set (Set β)) : image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

theorem Set.prod_eq_biUnion_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ⋃ a ∈ s, (fun (b : β) => (a, b)) '' t

theorem Set.prod_eq_biUnion_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ⋃ b ∈ t, (fun (a : α) => (a, b)) '' s

theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} : s.seq t = ⋃ f ∈ s, f '' t

theorem Set.seq_subset {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} {u : Set β} : s.seq t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, f a ∈ u

theorem Set.seq_mono {α : Type u_1} {β : Type u_2} {s₀ s₁ : Set (α → β)} {t₀ t₁ : Set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) : s₀.seq t₀ ⊆ s₁.seq t₁

theorem Set.singleton_seq {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set α} : {f}.seq t = f '' t

theorem Set.seq_singleton {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {a : α} : s.seq {a} = (fun (f : α → β) => f a) '' s

theorem Set.seq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} : s.seq (t.seq u) = (((fun (x1 : β → γ) (x2 : α → β) => x1 ∘ x2) '' s).seq t).seq u

theorem Set.image_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {s : Set (α → β)} {t : Set α} : f '' s.seq t = ((fun (x : α → β) => f ∘ x) '' s).seq t

theorem Set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t

theorem Set.prod_image_seq_comm {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : (Prod.mk '' s).seq t = ((fun (b : β) (a : α) => (a, b)) '' t).seq s

theorem Set.image2_eq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = (f '' s).seq t