# 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`

source
theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} :
GaloisConnection (image f) (preimage f)
source
theorem Set.preimage_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} :
GaloisConnection (preimage f) (kernImage f)
source
theorem Set.kernImage_mono {α : Type u_1} {β : Type u_2} {f : α → β} :
Monotone (kernImage f)
source
theorem Set.kernImage_eq_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} :
kernImage f s = (f '' s ᶜ)ᶜ
source
theorem Set.kernImage_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} :
kernImage f s ᶜ = (f '' s)ᶜ
source
theorem Set.kernImage_empty {α : Type u_1} {β : Type u_2} {f : α → β} :
kernImage f ∅ = (range f)ᶜ
source
theorem Set.kernImage_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} :
kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
source
theorem Set.compl_range_subset_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} :
(range f)ᶜ ⊆ kernImage f s
source
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
source
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
source
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` #

source
@[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
source
@[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
source
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
source
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)
source
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)
source
@[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
source
@[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)
source
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)
source
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)
source
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)
source
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
source
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
source
theorem Set.image_sInter_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (f : α → β) :
f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s
source
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
source
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` #

source
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)
source
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)
source
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` #

source
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
source
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
source
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
source
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
source
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` #

source
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)
source
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)
source
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)
source
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)
source
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)
source
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
source
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` #

source
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)
source
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)
source
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)
source
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` #

source
theorem Set.image_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set α} :
f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i
source
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
source
theorem Set.univ_subtype {α : Type u_1} {p : α → Prop} :
univ = ⋃ (x : α), ⋃ (h : p x), {⟨x, h⟩}
source
theorem Set.range_eq_iUnion {α : Type u_1} {ι : Sort u_9} (f : ι → α) :
range f = ⋃ (i : ι), {f i}
source
theorem Set.image_eq_iUnion {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) :
f '' s = ⋃ i ∈ s, {f i}
source
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)
source
@[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)
source
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)
source
@[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)
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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₂
source
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₂
source
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
source
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
source
theorem Set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : α → β} :
Monotone (preimage f)
source
@[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
source
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
source
theorem Set.image_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set α)} :
f '' ⋃₀ s = ⋃₀ (image f '' s)
source
@[simp]
theorem Set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} :
f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
source
theorem Set.preimage_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β} :
f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i
source
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
source
@[simp]
theorem Set.preimage_sInter {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} :
f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t
source
@[simp]
theorem Set.biUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) :
⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
source
theorem Set.biUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) :
⋃ y ∈ range f, f ⁻¹' {y} = univ
source
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
source
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
source
theorem Set.prod_sUnion {α : Type u_1} {β : Type u_2} {s : Set α} {C : Set (Set β)} :
s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) => s ×ˢ t) '' C)
source
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
source
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
source
theorem Set.sUnion_prod_const {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {t : Set β} :
⋃₀ C ×ˢ t = ⋃₀ ((fun (s : Set α) => s ×ˢ t) '' C)
source
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
source
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.

source
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
source
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
source
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.

source
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
source
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
source
theorem Set.sInter_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) :
⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t
source
theorem Set.prod_sInter {α : Type u_1} {β : Type u_2} {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) :
s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t
source
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
source
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`

source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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)
source
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
source
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)
source
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
source
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)
source
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
source
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
source
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
source
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
source
theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} :
s.seq t = ⋃ f ∈ s, f '' t
source
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
source
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₁
source
theorem Set.singleton_seq {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set α} :
{f}.seq t = f '' t
source
theorem Set.seq_singleton {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {a : α} :
s.seq {a} = (fun (f : α → β) => f a) '' s
source
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
source
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
source
theorem Set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = (Prod.mk '' s).seq t
source
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
source
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