Mathlib.Data.Set.Lattice.Image

Set.image_preimage theorem

: GaloisConnection (image f) (preimage f)

Full source

protected theorem image_preimage : GaloisConnection (image f) (preimage f) := fun _ _ =>
  image_subset_iff

Galois Connection Between Image and Preimage Operations

Informal description

For any function $f : \alpha \to \beta$, the image and preimage operations form a Galois connection. That is, for any subset $s \subseteq \alpha$ and $t \subseteq \beta$, we have: \[ f(s) \subseteq t \quad \text{if and only if} \quad s \subseteq f^{-1}(t) \] where $f(s)$ denotes the image of $s$ under $f$ and $f^{-1}(t)$ denotes the preimage of $t$ under $f$.

Set.preimage_kernImage theorem

: GaloisConnection (preimage f) (kernImage f)

Full source

protected theorem preimage_kernImage : GaloisConnection (preimage f) (kernImage f) := fun _ _ =>
  subset_kernImage_iff.symm

Galois Connection Between Preimage and Kernel Image

Informal description

The functions `preimage f` and `kernImage f` form a Galois connection. That is, for any function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, we have: \[ f^{-1}(t) \subseteq s \iff t \subseteq \text{kernImage}(f)(s) \] where $f^{-1}(t)$ denotes the preimage of $t$ under $f$, and $\text{kernImage}(f)(s)$ denotes the kernel image of $s$ under $f$.

Set.kernImage_mono theorem

: Monotone (kernImage f)

Full source

lemma kernImage_mono : Monotone (kernImage f) :=
  Set.preimage_kernImage.monotone_u

Monotonicity of Kernel Image Operation

Informal description

The kernel image operation `kernImage f` is monotone. That is, for any function $f : \alpha \to \beta$ and sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subseteq s_2$, then $\text{kernImage}(f)(s_1) \subseteq \text{kernImage}(f)(s_2)$.

Set.kernImage_eq_compl theorem

{s : Set α} : kernImage f s = (f '' sᶜ)ᶜ

Full source

lemma kernImage_eq_compl {s : Set α} : kernImage f s = (f '' sᶜ)ᶜ :=
  Set.preimage_kernImage.u_unique (Set.image_preimage.compl)
    (fun t ↦ compl_compl (f ⁻¹' t) ▸ Set.preimage_compl)

Kernel Image as Complement of Image of Complement

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the kernel image of $s$ under $f$ is equal to the complement of the image of the complement of $s$ under $f$. That is, \[ \text{kernImage}(f)(s) = (f(s^c))^c \] where $s^c$ denotes the complement of $s$ in $\alpha$.

Set.kernImage_compl theorem

{s : Set α} : kernImage f (sᶜ) = (f '' s)ᶜ

Full source

lemma kernImage_compl {s : Set α} : kernImage f (sᶜ) = (f '' s)ᶜ := by
  rw [kernImage_eq_compl, compl_compl]

Kernel Image of Complement Equals Complement of Image

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the kernel image of the complement of $s$ under $f$ is equal to the complement of the image of $s$ under $f$. That is, \[ \text{kernImage}(f)(s^c) = (f(s))^c \] where $s^c$ denotes the complement of $s$ in $\alpha$.

Set.kernImage_empty theorem

: kernImage f ∅ = (range f)ᶜ

Full source

lemma kernImage_empty : kernImage f ∅ = (range f)ᶜ := by
  rw [kernImage_eq_compl, compl_empty, image_univ]

Kernel Image of Empty Set Equals Complement of Range

Informal description

For any function $f : \alpha \to \beta$, the kernel image of the empty set under $f$ equals the complement of the range of $f$. That is, \[ \text{kernImage}(f)(\emptyset) = (\text{range } f)^c \]

Set.kernImage_preimage_eq_iff theorem

{s : Set β} : kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Full source

lemma kernImage_preimage_eq_iff {s : Set β} : kernImagekernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s := by
  rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]

Kernel Image of Preimage Equals Set iff Complement of Range is Subset

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \beta$, the kernel image of the preimage of $s$ under $f$ equals $s$ if and only if the complement of the range of $f$ is a subset of $s$. That is, \[ \text{kernImage}(f)(f^{-1}(s)) = s \iff (\text{range } f)^c \subseteq s. \]

Set.compl_range_subset_kernImage theorem

{s : Set α} : (range f)ᶜ ⊆ kernImage f s

Full source

lemma compl_range_subset_kernImage {s : Set α} : (range f)ᶜ(range f)ᶜ ⊆ kernImage f s := by
  rw [← kernImage_empty]
  exact kernImage_mono (empty_subset _)

Complement of Range is Subset of Kernel Image

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \alpha$, the complement of the range of $f$ is a subset of the kernel image of $s$ under $f$. That is, \[ (\text{range } f)^c \subseteq \text{kernImage}(f)(s). \]

Set.kernImage_union_preimage theorem

{s : Set α} {t : Set β} : kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Full source

lemma kernImage_union_preimage {s : Set α} {t : Set β} :
    kernImage f (s ∪ f ⁻¹' t) = kernImagekernImage f s ∪ t := by
  rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]

Kernel Image of Union with Preimage Equals Union of Kernel Image and Set

Informal description

For any function $f : \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the kernel image of the union $s \cup f^{-1}(t)$ under $f$ equals the union of the kernel image of $s$ and $t$. That is, \[ \text{kernImage}(f)(s \cup f^{-1}(t)) = \text{kernImage}(f)(s) \cup t. \]

Set.kernImage_preimage_union theorem

{s : Set α} {t : Set β} : kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

Full source

lemma kernImage_preimage_union {s : Set α} {t : Set β} :
    kernImage f (f ⁻¹' tf ⁻¹' t ∪ s) = t ∪ kernImage f s := by
  rw [union_comm, kernImage_union_preimage, union_comm]

Kernel Image of Preimage Union Equals Union of Target and Kernel Image

Informal description

For any function $f : \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the kernel image of the union $f^{-1}(t) \cup s$ under $f$ equals the union of $t$ and the kernel image of $s$. That is, \[ \text{kernImage}(f)(f^{-1}(t) \cup s) = t \cup \text{kernImage}(f)(s). \]

Set.image_projection_prod theorem

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

Full source

theorem image_projection_prod {ι : Type*} {α : ι → Type*} {v : ∀ i : ι, Set (α i)}
    (hv : (pi univ v).Nonempty) (i : ι) :
    ((fun x : ∀ i : ι, α i => x i) '' ⋂ k, (fun x : ∀ j : ι, α j => x k) ⁻¹' v k) = v i := by
  classical
    apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

Projection Image of Intersection Equals Component Set in Nonempty Product

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of types, and for each $i \in \iota$, let $v_i \subseteq α_i$ be a subset. Assume that the product $\prod_{i \in \iota} v_i$ is nonempty. Then for any fixed index $i \in \iota$, the image of the intersection $\bigcap_{k \in \iota} \{x \in \prod_{j \in \iota} α_j \mid x_k \in v_k\}$ under the projection map $x \mapsto x_i$ is equal to $v_i$. In other words: \[ \left\{x_i \mid x \in \bigcap_{k \in \iota} \{x \mid x_k \in v_k\}\right\} = v_i. \]

Set.mapsTo_sUnion theorem

{S : Set (Set α)} {t : Set β} {f : α → β} : MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, MapsTo f s t

Full source

@[simp]
theorem mapsTo_sUnion {S : Set (Set α)} {t : Set β} {f : α → β} :
    MapsToMapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, MapsTo f s t :=
  sUnion_subset_iff

Mapping Property of Union of Sets: $f(\bigcup S) \subseteq t \leftrightarrow \forall s \in S, f(s) \subseteq t$

Informal description

For any family of sets $S$ in $\alpha$, a set $t$ in $\beta$, and a function $f : \alpha \to \beta$, the function $f$ maps the union of all sets in $S$ into $t$ if and only if for every set $s \in S$, $f$ maps $s$ into $t$.

Set.mapsTo_iUnion theorem

{s : ι → Set α} {t : Set β} {f : α → β} : MapsTo f (⋃ i, s i) t ↔ ∀ i, MapsTo f (s i) t

Full source

@[simp]
theorem mapsTo_iUnion {s : ι → Set α} {t : Set β} {f : α → β} :
    MapsToMapsTo f (⋃ i, s i) t ↔ ∀ i, MapsTo f (s i) t :=
  iUnion_subset_iff

Maps to Union iff Maps to Each Set in the Family

Informal description

For any family of sets $(s_i)_{i \in \iota}$ in $\alpha$, a set $t$ in $\beta$, and a function $f : \alpha \to \beta$, the function $f$ maps the union $\bigcup_{i \in \iota} s_i$ into $t$ if and only if for every index $i$, $f$ maps $s_i$ into $t$.

Set.mapsTo_iUnion₂ theorem

 {s : ∀ i, κ i → Set α} {t : Set β} {f : α → β} : MapsTo f (⋃ (i) (j), s i j) t ↔ ∀ i j, MapsTo f (s i j) t

Full source

theorem mapsTo_iUnion₂ {s : ∀ i, κ i → Set α} {t : Set β} {f : α → β} :
    MapsToMapsTo f (⋃ (i) (j), s i j) t ↔ ∀ i j, MapsTo f (s i j) t :=
  iUnion₂_subset_iff

MapsTo Condition for Double Union of Sets

Informal description

For a function $f : \alpha \to \beta$, a family of sets $\{s_{i,j}\}_{i,j}$ in $\alpha$, and a set $t \subseteq \beta$, the following are equivalent: 1. $f$ maps the union $\bigcup_{i,j} s_{i,j}$ into $t$. 2. For every $i$ and $j$, $f$ maps $s_{i,j}$ into $t$. In symbols: $$ f\left(\bigcup_{i,j} s_{i,j}\right) \subseteq t \leftrightarrow \forall i\, j,\ f(s_{i,j}) \subseteq t. $$

Set.mapsTo_iUnion_iUnion theorem

 {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, MapsTo f (s i) (t i)) : MapsTo f (⋃ i, s i) (⋃ i, t i)

Full source

theorem mapsTo_iUnion_iUnion {s : ι → Set α} {t : ι → Set β} {f : α → β}
    (H : ∀ i, MapsTo f (s i) (t i)) : MapsTo f (⋃ i, s i) (⋃ i, t i) :=
  mapsTo_iUnion.2 fun i ↦ (H i).mono_right (subset_iUnion t i)

Union Preservation under MapsTo Condition

Informal description

Let $(s_i)_{i \in \iota}$ be a family of subsets of $\alpha$, $(t_i)_{i \in \iota}$ a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every index $i$, $f$ maps $s_i$ into $t_i$, then $f$ maps the union $\bigcup_{i} s_i$ into the union $\bigcup_{i} t_i$.

Set.mapsTo_iUnion₂_iUnion₂ theorem

 {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β} (H : ∀ i j, MapsTo f (s i j) (t i j)) :
  MapsTo f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j)

Full source

theorem mapsTo_iUnion₂_iUnion₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, MapsTo f (s i j) (t i j)) : MapsTo f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j) :=
  mapsTo_iUnion_iUnion fun i => mapsTo_iUnion_iUnion (H i)

Double Union Preservation under Componentwise MapsTo Condition

Informal description

Let $\{s_{i,j}\}_{i,j}$ be a family of subsets of $\alpha$, $\{t_{i,j}\}_{i,j}$ a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every index $i$ and $j$, $f$ maps $s_{i,j}$ into $t_{i,j}$, then $f$ maps the double union $\bigcup_{i,j} s_{i,j}$ into the double union $\bigcup_{i,j} t_{i,j}$.

Set.mapsTo_sInter theorem

{s : Set α} {T : Set (Set β)} {f : α → β} : MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, MapsTo f s t

Full source

@[simp]
theorem mapsTo_sInter {s : Set α} {T : Set (Set β)} {f : α → β} :
    MapsToMapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, MapsTo f s t :=
  forall₂_swap

Characterization of Mapping into Set Intersection via Component Mappings

Informal description

For a function $f : \alpha \to \beta$, a set $s \subseteq \alpha$, and a family of sets $T \subseteq \mathcal{P}(\beta)$, the following are equivalent: 1. $f$ maps $s$ into the intersection $\bigcap T$ of all sets in $T$ 2. For every set $t \in T$, $f$ maps $s$ into $t$ In other words, $f(s) \subseteq \bigcap T$ if and only if for all $t \in T$, $f(s) \subseteq t$.

Set.mapsTo_iInter theorem

{s : Set α} {t : ι → Set β} {f : α → β} : MapsTo f s (⋂ i, t i) ↔ ∀ i, MapsTo f s (t i)

Full source

@[simp]
theorem mapsTo_iInter {s : Set α} {t : ι → Set β} {f : α → β} :
    MapsToMapsTo f s (⋂ i, t i) ↔ ∀ i, MapsTo f s (t i) :=
  mapsTo_sInter.trans forall_mem_range

Characterization of Mapping into Indexed Intersection via Componentwise Maps

Informal description

For a function $f \colon \alpha \to \beta$, a subset $s \subseteq \alpha$, and a family of subsets $\{t_i\}_{i \in \iota}$ of $\beta$, the following are equivalent: 1. $f$ maps $s$ into the intersection $\bigcap_{i \in \iota} t_i$ 2. For every index $i \in \iota$, $f$ maps $s$ into $t_i$ In other words, $f(s) \subseteq \bigcap_{i \in \iota} t_i$ if and only if for all $i \in \iota$, $f(s) \subseteq t_i$.

Set.mapsTo_iInter₂ theorem

 {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} : MapsTo f s (⋂ (i) (j), t i j) ↔ ∀ i j, MapsTo f s (t i j)

Full source

theorem mapsTo_iInter₂ {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} :
    MapsToMapsTo f s (⋂ (i) (j), t i j) ↔ ∀ i j, MapsTo f s (t i j) := by
  simp only [mapsTo_iInter]

Characterization of Maps to Double Intersection via Componentwise Maps

Informal description

For a function $f : \alpha \to \beta$, a set $s \subseteq \alpha$, and a family of sets $t_i : \kappa_i \to \text{Set } \beta$ indexed by $i$, the following are equivalent: 1. $f$ maps $s$ into the intersection $\bigcap_{i,j} t_i(j)$. 2. For every $i$ and $j$, $f$ maps $s$ into $t_i(j)$. In other words, $f(s) \subseteq \bigcap_{i,j} t_i(j)$ if and only if for all $i$ and $j$, $f(s) \subseteq t_i(j)$.

Set.mapsTo_iInter_iInter theorem

 {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, MapsTo f (s i) (t i)) : MapsTo f (⋂ i, s i) (⋂ i, t i)

Full source

theorem mapsTo_iInter_iInter {s : ι → Set α} {t : ι → Set β} {f : α → β}
    (H : ∀ i, MapsTo f (s i) (t i)) : MapsTo f (⋂ i, s i) (⋂ i, t i) :=
  mapsTo_iInter.2 fun i => (H i).mono_left (iInter_subset s i)

Preservation of Intersections under Componentwise Maps

Informal description

For a function $f \colon \alpha \to \beta$ and families of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and $\{t_i\}_{i \in \iota}$ in $\beta$, if for every index $i \in \iota$ the function $f$ maps $s_i$ into $t_i$, then $f$ maps the intersection $\bigcap_{i \in \iota} s_i$ into the intersection $\bigcap_{i \in \iota} t_i$. In other words, if $\forall i \in \iota, f(s_i) \subseteq t_i$, then $f\left(\bigcap_{i \in \iota} s_i\right) \subseteq \bigcap_{i \in \iota} t_i$.

Set.mapsTo_iInter₂_iInter₂ theorem

 {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β} (H : ∀ i j, MapsTo f (s i j) (t i j)) :
  MapsTo f (⋂ (i) (j), s i j) (⋂ (i) (j), t i j)

Full source

theorem mapsTo_iInter₂_iInter₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, MapsTo f (s i j) (t i j)) : MapsTo f (⋂ (i) (j), s i j) (⋂ (i) (j), t i j) :=
  mapsTo_iInter_iInter fun i => mapsTo_iInter_iInter (H i)

Preservation of Double Intersections under Componentwise Maps

Informal description

For a function $f \colon \alpha \to \beta$ and doubly-indexed families of sets $\{s_{i,j}\}_{i,j}$ in $\alpha$ and $\{t_{i,j}\}_{i,j}$ in $\beta$, if for every pair of indices $(i,j)$ the function $f$ maps $s_{i,j}$ into $t_{i,j}$, then $f$ maps the double intersection $\bigcap_{i,j} s_{i,j}$ into the double intersection $\bigcap_{i,j} t_{i,j}$. In other words, if $\forall i j, f(s_{i,j}) \subseteq t_{i,j}$, then $f\left(\bigcap_{i,j} s_{i,j}\right) \subseteq \bigcap_{i,j} t_{i,j}$.

Set.image_iInter_subset theorem

(s : ι → Set α) (f : α → β) : (f '' ⋂ i, s i) ⊆ ⋂ i, f '' s i

Full source

theorem image_iInter_subset (s : ι → Set α) (f : α → β) : (f '' ⋂ i, s i) ⊆ ⋂ i, f '' s i :=
  (mapsTo_iInter_iInter fun i => mapsTo_image f (s i)).image_subset

Image of Intersection is Subset of Intersection of Images

Informal description

For any function $f \colon \alpha \to \beta$ and any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$, the image of the intersection $\bigcap_{i \in \iota} s_i$ under $f$ is contained in the intersection of the images $\bigcap_{i \in \iota} f(s_i)$. In other words, $f\left(\bigcap_{i \in \iota} s_i\right) \subseteq \bigcap_{i \in \iota} f(s_i)$.

Set.image_iInter₂_subset theorem

(s : ∀ i, κ i → Set α) (f : α → β) : (f '' ⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), f '' s i j

Full source

theorem image_iInter₂_subset (s : ∀ i, κ i → Set α) (f : α → β) :
    (f '' ⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), f '' s i j :=
  (mapsTo_iInter₂_iInter₂ fun i hi => mapsTo_image f (s i hi)).image_subset

Image of Double Intersection is Subset of Double Intersection of Images

Informal description

For any function $f \colon \alpha \to \beta$ and any doubly-indexed family of sets $\{s_{i,j}\}_{i,j}$ in $\alpha$, the image of the double intersection $\bigcap_{i,j} s_{i,j}$ under $f$ is contained in the double intersection of the images $\bigcap_{i,j} f(s_{i,j})$. In other words, $f\left(\bigcap_{i,j} s_{i,j}\right) \subseteq \bigcap_{i,j} f(s_{i,j})$.

Set.image_sInter_subset theorem

(S : Set (Set α)) (f : α → β) : f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Full source

theorem image_sInter_subset (S : Set (Set α)) (f : α → β) : f '' ⋂₀ Sf '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s := by
  rw [sInter_eq_biInter]
  apply image_iInter₂_subset

Image of Set Intersection is Subset of Intersection of Images

Informal description

For any function $f \colon \alpha \to \beta$ and any family of sets $S$ in $\alpha$, the image of the intersection $\bigcap S$ under $f$ is contained in the intersection of the images $\bigcap_{s \in S} f(s)$. In other words, $f\left(\bigcap S\right) \subseteq \bigcap_{s \in S} f(s)$.

Set.image2_sInter_right_subset theorem

(t : Set α) (S : Set (Set β)) (f : α → β → γ) : image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s

Full source

theorem image2_sInter_right_subset (t : Set α) (S : Set (Set β)) (f : α → β → γ) :
    image2image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s := by
  aesop

Image of Intersection under Binary Function is Contained in Intersection of Images

Informal description

Let $t$ be a subset of $\alpha$, $S$ a family of subsets of $\beta$, and $f : \alpha \to \beta \to \gamma$ a function. Then the image of $t$ and the intersection of $S$ under $f$ is contained in the intersection over $s \in S$ of the images of $t$ and $s$ under $f$. In symbols: \[ f(t, \bigcap S) \subseteq \bigcap_{s \in S} f(t, s). \]

Set.image2_sInter_left_subset theorem

(S : Set (Set α)) (t : Set β) (f : α → β → γ) : image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Full source

theorem image2_sInter_left_subset (S : Set (Set α)) (t : Set β)  (f : α → β → γ) :
    image2image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t := by
  aesop

Image of Intersection under Binary Function is Subset of Intersection of Images

Informal description

For any family of sets $S$ in $\alpha$, any set $t$ in $\beta$, and any function $f : \alpha \to \beta \to \gamma$, the image of the intersection of $S$ under $f$ applied to $t$ is contained in the intersection of the images of each set $s \in S$ under $f$ applied to $t$. In symbols: $$ f(\bigcap S, t) \subseteq \bigcap_{s \in S} f(s, t) $$

Set.injective_iff_injective_of_iUnion_eq_univ theorem

: Injective f ↔ ∀ i, Injective ((U i).restrictPreimage f)

Full source

theorem injective_iff_injective_of_iUnion_eq_univ :
    InjectiveInjective f ↔ ∀ i, Injective ((U i).restrictPreimage f) := by
  refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)
  injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

Injectivity Characterization via Union Covering Codomain

Informal description

A function $f : \alpha \to \beta$ is injective if and only if for every index $i$, the restriction of $f$ to the preimage of $U_i$ is injective, where $\{U_i\}$ is a family of sets whose union equals the entire codomain $\beta$.

Set.surjective_iff_surjective_of_iUnion_eq_univ theorem

: Surjective f ↔ ∀ i, Surjective ((U i).restrictPreimage f)

Full source

theorem surjective_iff_surjective_of_iUnion_eq_univ :
    SurjectiveSurjective f ↔ ∀ i, Surjective ((U i).restrictPreimage f) := by
  refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩
  obtain ⟨i, hi⟩ :=
    Set.mem_iUnion.mp
      (show x ∈ Set.iUnion U by rw [hU]; trivial)
  exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

Surjectivity Characterization via Union Covering Codomain

Informal description

A function $f : \alpha \to \beta$ is surjective if and only if for every index $i$, the restriction of $f$ to the preimage of $U_i$ is surjective, where $\{U_i\}$ is a family of sets whose union equals the entire codomain $\beta$.

Set.bijective_iff_bijective_of_iUnion_eq_univ theorem

: Bijective f ↔ ∀ i, Bijective ((U i).restrictPreimage f)

Full source

theorem bijective_iff_bijective_of_iUnion_eq_univ :
    BijectiveBijective f ↔ ∀ i, Bijective ((U i).restrictPreimage f) := by
  rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
    surjective_iff_surjective_of_iUnion_eq_univ hU]
  simp [Bijective, forall_and]

Bijectivity Characterization via Union Covering Codomain

Informal description

A function $f : \alpha \to \beta$ is bijective if and only if for every index $i$, the restriction of $f$ to the preimage of $U_i$ is bijective, where $\{U_i\}$ is a family of sets whose union equals the entire codomain $\beta$.

Set.InjOn.image_iInter_eq theorem

[Nonempty ι] {s : ι → Set α} {f : α → β} (h : InjOn f (⋃ i, s i)) : (f '' ⋂ i, s i) = ⋂ i, f '' s i

Full source

theorem InjOn.image_iInter_eq [Nonempty ι] {s : ι → Set α} {f : α → β} (h : InjOn f (⋃ i, s i)) :
    (f '' ⋂ i, s i) = ⋂ i, f '' s i := by
  inhabit ι
  refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_
  simp only [mem_iInter, mem_image] at hy
  choose x hx hy using hy
  refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
  suffices x default = x i by
    rw [this]
    apply hx
  replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
  apply h (hx _) (hx _)
  simp only [hy]

Image of Intersection under Injective Function Equals Intersection of Images

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$, where $\iota$ is nonempty, and let $f \colon \alpha \to \beta$ be a function that is injective on the union $\bigcup_{i \in \iota} s_i$. Then the image of the intersection $\bigcap_{i \in \iota} s_i$ under $f$ equals the intersection of the images $\bigcap_{i \in \iota} f(s_i)$. In other words, $f\left(\bigcap_{i \in \iota} s_i\right) = \bigcap_{i \in \iota} f(s_i)$.

Set.InjOn.image_biInter_eq theorem

 {p : ι → Prop} {s : ∀ i, p i → Set α} (hp : ∃ i, p i) {f : α → β} (h : InjOn f (⋃ (i) (hi), s i hi)) :
  (f '' ⋂ (i) (hi), s i hi) = ⋂ (i) (hi), f '' s i hi

Full source

theorem InjOn.image_biInter_eq {p : ι → Prop} {s : ∀ i, p i → Set α} (hp : ∃ i, p i)
    {f : α → β} (h : InjOn f (⋃ (i) (hi), s i hi)) :
    (f '' ⋂ (i) (hi), s i hi) = ⋂ (i) (hi), f '' s i hi := by
  simp only [iInter, iInf_subtype']
  haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
  apply InjOn.image_iInter_eq
  simpa only [iUnion, iSup_subtype'] using h

Image of Bounded Intersection under Injective Function Equals Bounded Intersection of Images

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by a predicate $p$ (with at least one $i$ satisfying $p(i)$), and let $f \colon \alpha \to \beta$ be a function that is injective on the union $\bigcup_{i, h_i} s_i h_i$. Then the image of the intersection $\bigcap_{i, h_i} s_i h_i$ under $f$ equals the intersection of the images $\bigcap_{i, h_i} f(s_i h_i)$. In other words, $f\left(\bigcap_{i, h_i} s_i h_i\right) = \bigcap_{i, h_i} f(s_i h_i)$.

Set.image_iInter theorem

{f : α → β} (hf : Bijective f) (s : ι → Set α) : (f '' ⋂ i, s i) = ⋂ i, f '' s i

Full source

theorem image_iInter {f : α → β} (hf : Bijective f) (s : ι → Set α) :
    (f '' ⋂ i, s i) = ⋂ i, f '' s i := by
  cases isEmpty_or_nonempty ι
  · simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
  · exact hf.injective.injOn.image_iInter_eq

Image of Intersection under Bijective Function Equals Intersection of Images

Informal description

Let $f \colon \alpha \to \beta$ be a bijective function and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$. Then the image of the intersection $\bigcap_{i \in \iota} s_i$ under $f$ equals the intersection of the images $\bigcap_{i \in \iota} f(s_i)$. In other words, $f\left(\bigcap_{i \in \iota} s_i\right) = \bigcap_{i \in \iota} f(s_i)$.

Set.image_iInter₂ theorem

{f : α → β} (hf : Bijective f) (s : ∀ i, κ i → Set α) : (f '' ⋂ (i) (j), s i j) = ⋂ (i) (j), f '' s i j

Full source

theorem image_iInter₂ {f : α → β} (hf : Bijective f) (s : ∀ i, κ i → Set α) :
    (f '' ⋂ (i) (j), s i j) = ⋂ (i) (j), f '' s i j := by simp_rw [image_iInter hf]

Image of Double Intersection under Bijective Function Equals Double Intersection of Images

Informal description

Let $f \colon \alpha \to \beta$ be a bijective function and let $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly-indexed family of subsets of $\alpha$. Then the image of the double intersection $\bigcap_{i,j} s_{i,j}$ under $f$ equals the double intersection of the images $\bigcap_{i,j} f(s_{i,j})$. In other words, $f\left(\bigcap_{i,j} s_{i,j}\right) = \bigcap_{i,j} f(s_{i,j})$.

Set.inj_on_iUnion_of_directed theorem

{s : ι → Set α} (hs : Directed (· ⊆ ·) s) {f : α → β} (hf : ∀ i, InjOn f (s i)) : InjOn f (⋃ i, s i)

Full source

theorem inj_on_iUnion_of_directed {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {f : α → β}
    (hf : ∀ i, InjOn f (s i)) : InjOn f (⋃ i, s i) := by
  intro x hx y hy hxy
  rcases mem_iUnion.1 hx with ⟨i, hx⟩
  rcases mem_iUnion.1 hy with ⟨j, hy⟩
  rcases hs i j with ⟨k, hi, hj⟩
  exact hf k (hi hx) (hj hy) hxy

Injectivity Preserved Under Directed Unions

Informal description

Let $\{s_i\}_{i \in \iota}$ be a directed family of subsets of $\alpha$ with respect to inclusion, and let $f : \alpha \to \beta$ be a function. If $f$ is injective on each $s_i$, then $f$ is injective on their union $\bigcup_{i} s_i$.

Set.surjOn_sUnion theorem

{s : Set α} {T : Set (Set β)} {f : α → β} (H : ∀ t ∈ T, SurjOn f s t) : SurjOn f s (⋃₀ T)

Full source

theorem surjOn_sUnion {s : Set α} {T : Set (Set β)} {f : α → β} (H : ∀ t ∈ T, SurjOn f s t) :
    SurjOn f s (⋃₀ T) := fun _ ⟨t, ht, hx⟩ => H t ht hx

Surjectivity Preserved Under Union of Codomains

Informal description

Let $s$ be a subset of $\alpha$, $T$ be a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $t \in T$, $f$ is surjective from $s$ to $t$, then $f$ is surjective from $s$ to the union of all sets in $T$, i.e., $\bigcup_{t \in T} t$.

Set.surjOn_iUnion theorem

{s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f s (t i)) : SurjOn f s (⋃ i, t i)

Full source

theorem surjOn_iUnion {s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f s (t i)) :
    SurjOn f s (⋃ i, t i) :=
  surjOn_sUnion <| forall_mem_range.2 H

Surjectivity Preserved Under Union of Indexed Codomains

Informal description

Let $s$ be a subset of $\alpha$, $\{t_i\}_{i \in \iota}$ be a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $i \in \iota$, $f$ is surjective from $s$ to $t_i$, then $f$ is surjective from $s$ to the union $\bigcup_{i \in \iota} t_i$.

Set.surjOn_iUnion_iUnion theorem

 {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f (s i) (t i)) : SurjOn f (⋃ i, s i) (⋃ i, t i)

Full source

theorem surjOn_iUnion_iUnion {s : ι → Set α} {t : ι → Set β} {f : α → β}
    (H : ∀ i, SurjOn f (s i) (t i)) : SurjOn f (⋃ i, s i) (⋃ i, t i) :=
  surjOn_iUnion fun i => (H i).mono (subset_iUnion _ _) (Subset.refl _)

Surjectivity Preserved Under Union of Indexed Domains and Codomains

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$, $\{t_i\}_{i \in \iota}$ be a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $i \in \iota$, $f$ is surjective from $s_i$ to $t_i$, then $f$ is surjective from the union $\bigcup_{i \in \iota} s_i$ to the union $\bigcup_{i \in \iota} t_i$.

Set.surjOn_iUnion₂ theorem

 {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} (H : ∀ i j, SurjOn f s (t i j)) : SurjOn f s (⋃ (i) (j), t i j)

Full source

theorem surjOn_iUnion₂ {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, SurjOn f s (t i j)) : SurjOn f s (⋃ (i) (j), t i j) :=
  surjOn_iUnion fun i => surjOn_iUnion (H i)

Surjectivity Preserved Under Double Union of Indexed Codomains

Informal description

Let $s$ be a subset of $\alpha$, $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly-indexed family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $i \in \iota$ and $j \in \kappa_i$, $f$ is surjective from $s$ to $t_{i,j}$, then $f$ is surjective from $s$ to the double union $\bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} t_{i,j}$.

Set.surjOn_iUnion₂_iUnion₂ theorem

 {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β} (H : ∀ i j, SurjOn f (s i j) (t i j)) :
  SurjOn f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j)

Full source

theorem surjOn_iUnion₂_iUnion₂ {s : ∀ i, κ i → Set α} {t : ∀ i, κ i → Set β} {f : α → β}
    (H : ∀ i j, SurjOn f (s i j) (t i j)) : SurjOn f (⋃ (i) (j), s i j) (⋃ (i) (j), t i j) :=
  surjOn_iUnion_iUnion fun i => surjOn_iUnion_iUnion (H i)

Surjectivity Preserved Under Double Union of Indexed Domains and Codomains

Informal description

Let $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly-indexed family of subsets of $\alpha$, $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly-indexed family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every $i \in \iota$ and $j \in \kappa_i$, $f$ is surjective from $s_{i,j}$ to $t_{i,j}$, then $f$ is surjective from the double union $\bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} s_{i,j}$ to the double union $\bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} t_{i,j}$.

Set.surjOn_iInter theorem

 [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

Full source

theorem surjOn_iInter [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 := by
  intro y hy
  rw [Hinj.image_iInter_eq, mem_iInter]
  exact fun i => H i hy

Surjectivity from Intersection Preserved Under Injectivity on Union

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ where $\iota$ is nonempty, $t$ a subset of $\beta$, and $f \colon \alpha \to \beta$ a function. If for every $i \in \iota$, $f$ is surjective from $s_i$ to $t$, and $f$ is injective on the union $\bigcup_{i \in \iota} s_i$, then $f$ is surjective from the intersection $\bigcap_{i \in \iota} s_i$ to $t$. In other words, under the given conditions, $f\left(\bigcap_{i \in \iota} s_i\right) = t$.

Set.surjOn_iInter_iInter theorem

 [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)

Full source

theorem surjOn_iInter_iInter [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) :=
  surjOn_iInter (fun i => (H i).mono (Subset.refl _) (iInter_subset _ _)) Hinj

Surjectivity from Intersection to Intersection Under Injectivity on Union

Informal description

Let $\{s_i\}_{i \in \iota}$ be a nonempty family of subsets of $\alpha$, $\{t_i\}_{i \in \iota}$ a family of subsets of $\beta$, and $f \colon \alpha \to \beta$ a function. If for every $i \in \iota$, $f$ is surjective from $s_i$ to $t_i$, and $f$ is injective on the union $\bigcup_{i \in \iota} s_i$, then $f$ is surjective from the intersection $\bigcap_{i \in \iota} s_i$ to the intersection $\bigcap_{i \in \iota} t_i$. In other words, under the given conditions, $f\left(\bigcap_{i \in \iota} s_i\right) = \bigcap_{i \in \iota} t_i$.

Set.bijOn_iUnion theorem

 {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)

Full source

theorem bijOn_iUnion {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) :=
  ⟨mapsTo_iUnion_iUnion fun i => (H i).mapsTo, Hinj, surjOn_iUnion_iUnion fun i => (H i).surjOn⟩

Bijectivity Preserved Under Union of Indexed Domains and Codomains

Informal description

Let $(s_i)_{i \in \iota}$ be a family of subsets of $\alpha$, $(t_i)_{i \in \iota}$ a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. Suppose that for every index $i$, $f$ is bijective from $s_i$ to $t_i$, and that $f$ is injective on the union $\bigcup_{i} s_i$. Then $f$ is bijective from the union $\bigcup_{i} s_i$ to the union $\bigcup_{i} t_i$.

Set.bijOn_iInter theorem

 [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)

Full source

theorem bijOn_iInter [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) :=
  ⟨mapsTo_iInter_iInter fun i => (H i).mapsTo,
    hi.elim fun i => (H i).injOn.mono (iInter_subset _ _),
    surjOn_iInter_iInter (fun i => (H i).surjOn) Hinj⟩

Bijectivity from Intersection to Intersection Under Injectivity on Union

Informal description

Let $\{s_i\}_{i \in \iota}$ be a nonempty family of subsets of $\alpha$, $\{t_i\}_{i \in \iota}$ a family of subsets of $\beta$, and $f \colon \alpha \to \beta$ a function. If for every $i \in \iota$, $f$ is bijective from $s_i$ to $t_i$, and $f$ is injective on the union $\bigcup_{i \in \iota} s_i$, then $f$ is bijective from the intersection $\bigcap_{i \in \iota} s_i$ to the intersection $\bigcap_{i \in \iota} t_i$. In other words, under the given conditions, $f$ restricts to a bijection between $\bigcap_{i \in \iota} s_i$ and $\bigcap_{i \in \iota} t_i$.

Set.bijOn_iUnion_of_directed theorem

 {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {t : ι → Set β} {f : α → β} (H : ∀ i, BijOn f (s i) (t i)) :
  BijOn f (⋃ i, s i) (⋃ i, t i)

Full source

theorem bijOn_iUnion_of_directed {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {t : ι → Set β}
    {f : α → β} (H : ∀ i, BijOn f (s i) (t i)) : BijOn f (⋃ i, s i) (⋃ i, t i) :=
  bijOn_iUnion H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn

Bijectivity Preserved Under Directed Unions of Domains and Codomains

Informal description

Let $\{s_i\}_{i \in \iota}$ be a directed family of subsets of $\alpha$ with respect to inclusion, $\{t_i\}_{i \in \iota}$ a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every index $i$, $f$ is bijective from $s_i$ to $t_i$, then $f$ is bijective from the union $\bigcup_{i} s_i$ to the union $\bigcup_{i} t_i$.

Set.bijOn_iInter_of_directed theorem

 [Nonempty ι] {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {t : ι → Set β} {f : α → β} (H : ∀ i, BijOn f (s i) (t i)) :
  BijOn f (⋂ i, s i) (⋂ i, t i)

Full source

theorem bijOn_iInter_of_directed [Nonempty ι] {s : ι → Set α} (hs : Directed (· ⊆ ·) s)
    {t : ι → Set β} {f : α → β} (H : ∀ i, BijOn f (s i) (t i)) : BijOn f (⋂ i, s i) (⋂ i, t i) :=
  bijOn_iInter H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn

Bijectivity Preserved Under Directed Intersections of Domains and Codomains

Informal description

Let $\{s_i\}_{i \in \iota}$ be a nonempty directed family of subsets of $\alpha$ with respect to inclusion, $\{t_i\}_{i \in \iota}$ a family of subsets of $\beta$, and $f : \alpha \to \beta$ a function. If for every index $i$, $f$ is bijective from $s_i$ to $t_i$, then $f$ is bijective from the intersection $\bigcap_{i} s_i$ to the intersection $\bigcap_{i} t_i$.

Set.image_iUnion theorem

{f : α → β} {s : ι → Set α} : (f '' ⋃ i, s i) = ⋃ i, f '' s i

Full source

theorem image_iUnion {f : α → β} {s : ι → Set α} : (f '' ⋃ i, s i) = ⋃ i, f '' s i := by
  ext1 x
  simp only [mem_image, mem_iUnion, ← exists_and_right, ← exists_and_left, exists_swap (α := α)]

Image of Union Equals Union of Images

Informal description

For any function $f : \alpha \to \beta$ and any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$, the image of the union $\bigcup_{i} s_i$ under $f$ equals the union of the images $\bigcup_{i} f(s_i)$. In symbols: $$ f\left(\bigcup_{i} s_i\right) = \bigcup_{i} f(s_i). $$

Set.image_iUnion₂ theorem

(f : α → β) (s : ∀ i, κ i → Set α) : (f '' ⋃ (i) (j), s i j) = ⋃ (i) (j), f '' s i j

Full source

theorem image_iUnion₂ (f : α → β) (s : ∀ i, κ i → Set α) :
    (f '' ⋃ (i) (j), s i j) = ⋃ (i) (j), f '' s i j := by simp_rw [image_iUnion]

Image of Double Union Equals Double Union of Images

Informal description

For any function $f : \alpha \to \beta$ and any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the image under $f$ of the double union $\bigcup_{i,j} s_{i,j}$ equals the double union of the images $\bigcup_{i,j} f(s_{i,j})$. In symbols: $$ f\left(\bigcup_{i,j} s_{i,j}\right) = \bigcup_{i,j} f(s_{i,j}). $$

Set.univ_subtype theorem

{p : α → Prop} : (univ : Set (Subtype p)) = ⋃ (x) (h : p x), {⟨x, h⟩}

Full source

theorem univ_subtype {p : α → Prop} : (univ : Set (Subtype p)) = ⋃ (x) (h : p x), {⟨x, h⟩} :=
  Set.ext fun ⟨x, h⟩ => by simp [h]

Universal Set of Subtype as Union of Singletons

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the universal set of the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the union over all $x \in \alpha$ satisfying $p(x)$ of the singleton sets containing the subtype element $\langle x, h\rangle$ (where $h$ is a proof that $p(x)$ holds). In symbols: $$ \mathrm{univ} = \bigcup_{x \in \alpha, h : p(x)} \{\langle x, h \rangle\} $$

Set.range_eq_iUnion theorem

{ι} (f : ι → α) : range f = ⋃ i, {f i}

Full source

theorem range_eq_iUnion {ι} (f : ι → α) : range f = ⋃ i, {f i} :=
  Set.ext fun a => by simp [@eq_comm α a]

Range as Union of Singletons

Informal description

For any function $f : \iota \to \alpha$, the range of $f$ is equal to the union of all singleton sets $\{f(i)\}$ for $i \in \iota$. That is, \[ \text{range}(f) = \bigcup_{i \in \iota} \{f(i)\}. \]

Set.image_eq_iUnion theorem

(f : α → β) (s : Set α) : f '' s = ⋃ i ∈ s, {f i}

Full source

theorem image_eq_iUnion (f : α → β) (s : Set α) : f '' s = ⋃ i ∈ s, {f i} :=
  Set.ext fun b => by simp [@eq_comm β b]

Image as Union of Singletons

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ equals the union over all elements $i \in s$ of the singletons $\{f(i)\}$. In other words: $$ f(s) = \bigcup_{i \in s} \{f(i)\} $$

Set.biUnion_range theorem

{f : ι → α} {g : α → Set β} : ⋃ x ∈ range f, g x = ⋃ y, g (f y)

Full source

theorem biUnion_range {f : ι → α} {g : α → Set β} : ⋃ x ∈ range f, g x = ⋃ y, g (f y) :=
  iSup_range

Union over Range Equals Union over Preimages

Informal description

For any function $f \colon \iota \to \alpha$ and any family of sets $g \colon \alpha \to \text{Set} \beta$, the union of $g(x)$ over all $x$ in the range of $f$ is equal to the union of $g(f(y))$ over all $y \in \iota$. In symbols: \[ \bigcup_{x \in \text{range } f} g(x) = \bigcup_{y} g(f(y)). \]

Set.iUnion_iUnion_eq' theorem

{f : ι → α} {g : α → Set β} : ⋃ (x) (y) (_ : f y = x), g x = ⋃ y, g (f y)

Full source

@[simp]
theorem iUnion_iUnion_eq' {f : ι → α} {g : α → Set β} :
    ⋃ (x) (y) (_ : f y = x), g x = ⋃ y, g (f y) := by simpa using biUnion_range

Double Union Equality for Function Images

Informal description

For any function $f \colon \iota \to \alpha$ and any family of sets $g \colon \alpha \to \mathcal{P}(\beta)$, the union over all $x \in \alpha$ and $y \in \iota$ such that $f(y) = x$ of the sets $g(x)$ is equal to the union over all $y \in \iota$ of the sets $g(f(y))$. In symbols: \[ \bigcup_{x \in \alpha, y \in \iota, f(y) = x} g(x) = \bigcup_{y \in \iota} g(f(y)). \]

Set.biInter_range theorem

{f : ι → α} {g : α → Set β} : ⋂ x ∈ range f, g x = ⋂ y, g (f y)

Full source

theorem biInter_range {f : ι → α} {g : α → Set β} : ⋂ x ∈ range f, g x = ⋂ y, g (f y) :=
  iInf_range

Intersection over Range Equals Intersection over Domain

Informal description

For any function $f \colon \iota \to \alpha$ and any family of sets $g \colon \alpha \to \mathcal{P}(\beta)$, the intersection of all sets $g(x)$ where $x$ ranges over the image of $f$ is equal to the intersection of all sets $g(f(y))$ where $y$ ranges over $\iota$. In symbols: \[ \bigcap_{x \in \mathrm{range}\, f} g(x) = \bigcap_{y \in \iota} g(f(y)). \]

Set.iInter_iInter_eq' theorem

{f : ι → α} {g : α → Set β} : ⋂ (x) (y) (_ : f y = x), g x = ⋂ y, g (f y)

Full source

@[simp]
theorem iInter_iInter_eq' {f : ι → α} {g : α → Set β} :
    ⋂ (x) (y) (_ : f y = x), g x = ⋂ y, g (f y) := by simpa using biInter_range

Double Intersection Equals Single Intersection under Function Application

Informal description

For any function $f \colon \iota \to \alpha$ and any family of sets $g \colon \alpha \to \mathcal{P}(\beta)$, the intersection of all sets $g(x)$ over pairs $(x, y)$ where $f(y) = x$ is equal to the intersection of all sets $g(f(y))$ over $y \in \iota$. In symbols: \[ \bigcap_{x, y \atop f(y) = x} g(x) = \bigcap_{y} g(f(y)). \]

Set.biUnion_image theorem

: ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y)

Full source

theorem biUnion_image : ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y) :=
  iSup_image

Union of Images Equals Union of Preimages under Function Application

Informal description

For any function $f : \alpha \to \beta$, set $s \subseteq \alpha$, and function $g : \beta \to \text{Set } \gamma$, the union of $g(x)$ over all $x$ in the image of $f$ on $s$ equals the union of $g(f(y))$ over all $y \in s$. In symbols: \[ \bigcup_{x \in f(s)} g(x) = \bigcup_{y \in s} g(f(y)) \]

Set.biInter_image theorem

: ⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y)

Full source

theorem biInter_image : ⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y) :=
  iInf_image

Intersection over Image Equals Intersection over Preimage

Informal description

For any function $f : \alpha \to \beta$ and any set $s \subseteq \alpha$, the intersection of $g(x)$ over all $x$ in the image of $f$ on $s$ equals the intersection of $g(f(y))$ over all $y \in s$. In symbols: \[ \bigcap_{x \in f(s)} g(x) = \bigcap_{y \in s} g(f(y)) \]

Set.biUnion_image2 theorem

 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) : ⋃ c ∈ image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g (f a b)

Full source

lemma biUnion_image2 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) :
    ⋃ c ∈ image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g (f a b) := iSup_image2 ..

Union of Images Equals Union of Pointwise Images

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$, a function $f : \alpha \to \beta \to \gamma$, and a function $g : \gamma \to \text{Set } \delta$, the union of $g(c)$ over all $c$ in the image of $f$ on $s \times t$ equals the union of $g(f(a,b))$ over all $a \in s$ and $b \in t$. In symbols: \[ \bigcup_{c \in f(s,t)} g(c) = \bigcup_{a \in s} \bigcup_{b \in t} g(f(a,b)) \]

Set.biInter_image2 theorem

 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) : ⋂ c ∈ image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g (f a b)

Full source

lemma biInter_image2 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) :
    ⋂ c ∈ image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g (f a b) := iInf_image2 ..

Double Intersection of Set-Valued Function over Binary Image Equals Nested Intersections

Informal description

Let $s$ be a set in type $\alpha$, $t$ a set in type $\beta$, $f : \alpha \to \beta \to \gamma$ a binary function, and $g : \gamma \to \text{Set } \delta$ a set-valued function. Then the intersection of $g(c)$ over all $c$ in the image of $f$ on $s \times t$ equals the double intersection of $g(f(a,b))$ over all $a \in s$ and $b \in t$. In symbols: \[ \bigcap_{c \in f(s,t)} g(c) = \bigcap_{a \in s} \bigcap_{b \in t} g(f(a,b)) \]

Set.iUnion_inter_iUnion theorem

{ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) : (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j

Full source

lemma iUnion_inter_iUnion {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j := by simp_rw [iUnion_inter, inter_iUnion]

Distributivity of Intersection over Union for Indexed Families of Sets

Informal description

For any indexed families of sets $\{f_i\}_{i \in I}$ and $\{g_j\}_{j \in J}$ in a type $\alpha$, the intersection of their unions equals the union of pairwise intersections: \[ \left(\bigcup_{i \in I} f_i\right) \cap \left(\bigcup_{j \in J} g_j\right) = \bigcup_{i \in I} \bigcup_{j \in J} (f_i \cap g_j). \]

Set.iInter_union_iInter theorem

{ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) : (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Full source

lemma iInter_union_iInter {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j := by simp_rw [iInter_union, union_iInter]

Distributivity of Union over Intersection for Indexed Families of Sets

Informal description

For any indexed families of sets $\{f_i\}_{i \in \iota}$ and $\{g_j\}_{j \in \kappa}$ in a type $\alpha$, the union of their intersections equals the intersection of all pairwise unions: \[ \left(\bigcap_{i} f_i\right) \cup \left(\bigcap_{j} g_j\right) = \bigcap_{i} \bigcap_{j} (f_i \cup g_j). \]

Set.iUnion₂_inter_iUnion₂ theorem

 {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*} (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
  (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Full source

lemma iUnion₂_inter_iUnion₂ {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*}
    (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
    (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂ := by
  simp_rw [iUnion_inter, inter_iUnion]

Distributivity of Intersection over Double Union for Doubly Indexed Families of Sets

Informal description

For any doubly indexed families of sets $\{f_{i_1,i_2}\}_{i_1 \in I_1, i_2 \in I_2(i_1)}$ and $\{g_{j_1,j_2}\}_{j_1 \in J_1, j_2 \in J_2(j_1)}$ in a type $\alpha$, the intersection of their double unions equals the quadruple union of all pairwise intersections: \[ \left(\bigcup_{i_1 \in I_1} \bigcup_{i_2 \in I_2(i_1)} f_{i_1,i_2}\right) \cap \left(\bigcup_{j_1 \in J_1} \bigcup_{j_2 \in J_2(j_1)} g_{j_1,j_2}\right) = \bigcup_{i_1 \in I_1} \bigcup_{i_2 \in I_2(i_1)} \bigcup_{j_1 \in J_1} \bigcup_{j_2 \in J_2(j_1)} (f_{i_1,i_2} \cap g_{j_1,j_2}). \]

Set.iInter₂_union_iInter₂ theorem

 {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*} (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
  (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Full source

lemma iInter₂_union_iInter₂ {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*}
    (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
    (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂ := by
  simp_rw [iInter_union, union_iInter]

Distributivity of Union over Double Intersection for Indexed Families of Sets

Informal description

For any doubly indexed families of sets $\{f_{i_1,i_2}\}_{i_1 \in \iota_1, i_2 \in \iota_2(i_1)}$ and $\{g_{j_1,j_2}\}_{j_1 \in \kappa_1, j_2 \in \kappa_2(j_1)}$ in a type $\alpha$, the union of their intersections equals the intersection of all pairwise unions: \[ \left(\bigcap_{i_1} \bigcap_{i_2} f_{i_1,i_2}\right) \cup \left(\bigcap_{j_1} \bigcap_{j_2} g_{j_1,j_2}\right) = \bigcap_{i_1} \bigcap_{i_2} \bigcap_{j_1} \bigcap_{j_2} (f_{i_1,i_2} \cup g_{j_1,j_2}). \]

Set.monotone_preimage theorem

{f : α → β} : Monotone (preimage f)

Full source

theorem monotone_preimage {f : α → β} : Monotone (preimage f) := fun _ _ h => preimage_mono h

Monotonicity of Preimage Operation

Informal description

For any function $f \colon \alpha \to \beta$, the preimage operation $f^{-1} \colon \mathcal{P}(\beta) \to \mathcal{P}(\alpha)$ is monotone. That is, for any sets $A, B \subseteq \beta$, if $A \subseteq B$ then $f^{-1}(A) \subseteq f^{-1}(B)$.

Set.preimage_iUnion theorem

{f : α → β} {s : ι → Set β} : (f ⁻¹' ⋃ i, s i) = ⋃ i, f ⁻¹' s i

Full source

@[simp]
theorem preimage_iUnion {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋃ i, s i) = ⋃ i, f ⁻¹' s i :=
  Set.ext <| by simp [preimage]

Preimage of Union Equals Union of Preimages

Informal description

For any function $f \colon \alpha \to \beta$ and any family of sets $\{s_i\}_{i \in \iota}$ in $\beta$, the preimage of the union $\bigcup_{i} s_i$ under $f$ is equal to the union of the preimages $\bigcup_{i} f^{-1}(s_i)$. In symbols: $$ f^{-1}\left(\bigcup_{i} s_i\right) = \bigcup_{i} f^{-1}(s_i) $$

Set.preimage_iUnion₂ theorem

{f : α → β} {s : ∀ i, κ i → Set β} : (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j

Full source

theorem preimage_iUnion₂ {f : α → β} {s : ∀ i, κ i → Set β} :
    (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j := by simp_rw [preimage_iUnion]

Preimage of Double Union Equals Double Union of Preimages

Informal description

For any function $f \colon \alpha \to \beta$ and any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\beta$, the preimage of the double union $\bigcup_{i,j} s_{i,j}$ under $f$ is equal to the double union of the preimages $\bigcup_{i,j} f^{-1}(s_{i,j})$. In symbols: $$ f^{-1}\left(\bigcup_{i,j} s_{i,j}\right) = \bigcup_{i,j} f^{-1}(s_{i,j}) $$

Set.image_sUnion theorem

{f : α → β} {s : Set (Set α)} : (f '' ⋃₀ s) = ⋃₀ (image f '' s)

Full source

theorem image_sUnion {f : α → β} {s : Set (Set α)} : (f '' ⋃₀ s) = ⋃₀ (image f '' s) := by
  ext b
  simp only [mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
  constructor
  · rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
    exact ⟨t, ht₁, a, ht₂, rfl⟩
  · rintro ⟨t, ht₁, a, ht₂, rfl⟩
    exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩

Image of Union Equals Union of Images

Informal description

For any function $f : \alpha \to \beta$ and any family of sets $s$ of subsets of $\alpha$, the image of the union of all sets in $s$ under $f$ equals the union of all images of sets in $s$ under $f$. In symbols: $$ f\left(\bigcup_{T \in s} T\right) = \bigcup_{T \in s} f(T) $$

Set.preimage_sUnion theorem

{f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Full source

@[simp]
theorem preimage_sUnion {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t := by
  rw [sUnion_eq_biUnion, preimage_iUnion₂]

Preimage of Union Equals Union of Preimages

Informal description

For any function $f \colon \alpha \to \beta$ and any collection of sets $s$ (where each $t \in s$ is a subset of $\beta$), the preimage of the union $\bigcup_{t \in s} t$ under $f$ equals the union of the preimages $\bigcup_{t \in s} f^{-1}(t)$. In symbols: $$ f^{-1}\left(\bigcup_{t \in s} t\right) = \bigcup_{t \in s} f^{-1}(t) $$

Set.preimage_iInter theorem

{f : α → β} {s : ι → Set β} : (f ⁻¹' ⋂ i, s i) = ⋂ i, f ⁻¹' s i

Full source

theorem preimage_iInter {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋂ i, s i) = ⋂ i, f ⁻¹' s i := by
  ext; simp

Preimage of Intersection Equals Intersection of Preimages

Informal description

For any function $f : \alpha \to \beta$ and any family of sets $\{s_i\}_{i \in \iota}$ in $\beta$, the preimage of the intersection $\bigcap_{i} s_i$ under $f$ is equal to the intersection of the preimages: \[ f^{-1}\left(\bigcap_{i} s_i\right) = \bigcap_{i} f^{-1}(s_i). \]

Set.preimage_iInter₂ theorem

{f : α → β} {s : ∀ i, κ i → Set β} : (f ⁻¹' ⋂ (i) (j), s i j) = ⋂ (i) (j), f ⁻¹' s i j

Full source

theorem preimage_iInter₂ {f : α → β} {s : ∀ i, κ i → Set β} :
    (f ⁻¹' ⋂ (i) (j), s i j) = ⋂ (i) (j), f ⁻¹' s i j := by simp_rw [preimage_iInter]

Preimage of Double Intersection Equals Double Intersection of Preimages

Informal description

For any function $f \colon \alpha \to \beta$ and any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\beta$, the preimage of the double intersection $\bigcap_{i,j} s_{i,j}$ under $f$ is equal to the double intersection of the preimages: \[ f^{-1}\left(\bigcap_{i,j} s_{i,j}\right) = \bigcap_{i,j} f^{-1}(s_{i,j}). \]

Set.preimage_sInter theorem

{f : α → β} {s : Set (Set β)} : f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t

Full source

@[simp]
theorem preimage_sInter {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t := by
  rw [sInter_eq_biInter, preimage_iInter₂]

Preimage of Set Intersection Equals Intersection of Preimages

Informal description

For any function $f \colon \alpha \to \beta$ and any collection of sets $s \subseteq \mathcal{P}(\beta)$, the preimage of the intersection $\bigcap_{t \in s} t$ under $f$ is equal to the intersection of the preimages: \[ f^{-1}\left(\bigcap_{t \in s} t\right) = \bigcap_{t \in s} f^{-1}(t). \]

Set.biUnion_preimage_singleton theorem

(f : α → β) (s : Set β) : ⋃ y ∈ s, f ⁻¹' { y } = f ⁻¹' s

Full source

@[simp]
theorem biUnion_preimage_singleton (f : α → β) (s : Set β) : ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s := by
  rw [← preimage_iUnion₂, biUnion_of_singleton]

Union of Preimages of Singletons Equals Preimage of Set

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the union of the preimages of singletons $\{y\}$ for all $y \in s$ is equal to the preimage of $s$ under $f$. In symbols: $$ \bigcup_{y \in s} f^{-1}(\{y\}) = f^{-1}(s). $$

Set.biUnion_range_preimage_singleton theorem

(f : α → β) : ⋃ y ∈ range f, f ⁻¹' { y } = univ

Full source

theorem biUnion_range_preimage_singleton (f : α → β) : ⋃ y ∈ range f, f ⁻¹' {y} = univ := by
  rw [biUnion_preimage_singleton, preimage_range]

Universal Coverage by Preimages of Range Singletons

Informal description

For any function $f \colon \alpha \to \beta$, the union of the preimages of singletons $\{y\}$ for all $y$ in the range of $f$ is equal to the universal set. In symbols: $$ \bigcup_{y \in \text{range } f} f^{-1}(\{y\}) = \text{univ}. $$

Set.prod_iUnion theorem

{s : Set α} {t : ι → Set β} : (s ×ˢ ⋃ i, t i) = ⋃ i, s ×ˢ t i

Full source

theorem prod_iUnion {s : Set α} {t : ι → Set β} : (s ×ˢ ⋃ i, t i) = ⋃ i, s ×ˢ t i := by
  ext
  simp

Distributivity of Cartesian Product over Indexed Union

Informal description

For any set $s \subseteq \alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the Cartesian product of $s$ with the union $\bigcup_{i} t_i$ is equal to the union of the Cartesian products $\bigcup_{i} (s \times t_i)$. In symbols: $$ s \times \left( \bigcup_{i} t_i \right) = \bigcup_{i} (s \times t_i) $$

Set.prod_iUnion₂ theorem

{s : Set α} {t : ∀ i, κ i → Set β} : (s ×ˢ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ×ˢ t i j

Full source

theorem prod_iUnion₂ {s : Set α} {t : ∀ i, κ i → Set β} :
    (s ×ˢ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ×ˢ t i j := by simp_rw [prod_iUnion]

Distributivity of Cartesian Product over Doubly-Indexed Union

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 Cartesian product of $s$ with the double union $\bigcup_{i,j} t_{i,j}$ is equal to the double union of the Cartesian products $\bigcup_{i,j} (s \times t_{i,j})$. In symbols: $$ s \times \left( \bigcup_{i,j} t_{i,j} \right) = \bigcup_{i,j} (s \times t_{i,j}) $$

Set.prod_sUnion theorem

{s : Set α} {C : Set (Set β)} : s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)

Full source

theorem prod_sUnion {s : Set α} {C : Set (Set β)} : s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C) := by
  simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]

Distributivity of Cartesian Product over Set Union: $s \times (\bigcup C) = \bigcup \{s \times t \mid t \in C\}$

Informal description

For any set $s \subseteq \alpha$ and any collection of sets $C \subseteq \mathcal{P}(\beta)$, the Cartesian product of $s$ with the union $\bigcup C$ equals the union of the Cartesian products $\{s \times t \mid t \in C\}$. In symbols: $$ s \times \left( \bigcup C \right) = \bigcup \{s \times t \mid t \in C\} $$

Set.iUnion_prod_const theorem

{s : ι → Set α} {t : Set β} : (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Full source

theorem iUnion_prod_const {s : ι → Set α} {t : Set β} : (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t := by
  ext
  simp

Union-Cartesian Product Distributivity: $(\bigcup_i s_i) \times t = \bigcup_i (s_i \times t)$

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t$ in $\beta$, the Cartesian product of the union $\bigcup_i s_i$ with $t$ equals the union of the Cartesian products $s_i \times t$ for all $i \in \iota$. That is, $$ \left(\bigcup_{i \in \iota} s_i\right) \times t = \bigcup_{i \in \iota} (s_i \times t). $$

Set.iUnion₂_prod_const theorem

{s : ∀ i, κ i → Set α} {t : Set β} : (⋃ (i) (j), s i j) ×ˢ t = ⋃ (i) (j), s i j ×ˢ t

Full source

theorem iUnion₂_prod_const {s : ∀ i, κ i → Set α} {t : Set β} :
    (⋃ (i) (j), s i j) ×ˢ t = ⋃ (i) (j), s i j ×ˢ t := by simp_rw [iUnion_prod_const]

Double Union-Cartesian Product Distributivity: $(\bigcup_{i,j} s_{i,j}) \times t = \bigcup_{i,j} (s_{i,j} \times t)$

Informal description

For any doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\alpha$ and any set $t$ in $\beta$, the Cartesian product of the union $\bigcup_{i,j} s_{i,j}$ with $t$ equals the union of the Cartesian products $s_{i,j} \times t$ for all $i \in \iota$ and $j \in \kappa_i$. That is, $$ \left(\bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} s_{i,j}\right) \times t = \bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} (s_{i,j} \times t). $$

Set.sUnion_prod_const theorem

{C : Set (Set α)} {t : Set β} : ⋃₀ C ×ˢ t = ⋃₀ ((fun s : Set α => s ×ˢ t) '' C)

Full source

theorem sUnion_prod_const {C : Set (Set α)} {t : Set β} :
    ⋃₀ C ×ˢ t = ⋃₀ ((fun s : Set α => s ×ˢ t) '' C) := by
  simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]

Union of Sets in Cartesian Product with Fixed Set: $\bigcup C \times t = \bigcup_{s \in C} (s \times t)$

Informal description

For any collection of sets $C \subseteq \mathcal{P}(\alpha)$ and any set $t \subseteq \beta$, the Cartesian product of the union of all sets in $C$ with $t$ equals the union of all Cartesian products $s \times t$ where $s$ ranges over $C$. In symbols: \[ \left(\bigcup_{s \in C} s\right) \times t = \bigcup_{s \in C} (s \times t). \]

Set.iUnion_prod theorem

 {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) : ⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i

Full source

theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) :
    ⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i := by
  ext
  simp

Union of Cartesian Products Equals Product of Unions

Informal description

For any indexed families of sets $s : \iota \to \mathcal{P}(\alpha)$ and $t : \iota' \to \mathcal{P}(\beta)$, the union of all Cartesian products $s_i \times t_j$ over all pairs $(i,j) \in \iota \times \iota'$ equals the Cartesian product of the union of all $s_i$ with the union of all $t_j$. In symbols: \[ \bigcup_{(i,j) \in \iota \times \iota'} s_i \times t_j = \left(\bigcup_{i \in \iota} s_i\right) \times \left(\bigcup_{j \in \iota'} t_j\right) \]

Set.iUnion_prod' theorem

(f : β × γ → Set α) : ⋃ x : β × γ, f x = ⋃ (i : β) (j : γ), f (i, j)

Full source

/-- Analogue of `iSup_prod` for sets. -/
lemma iUnion_prod' (f : β × γ → Set α) : ⋃ x : β × γ, f x = ⋃ (i : β) (j : γ), f (i, j) :=
  iSup_prod

Union of Product Indexed Sets Equals Double Union

Informal description

For any function $f$ mapping pairs $(i,j) \in \beta \times \gamma$ to subsets of $\alpha$, the union of all $f(x)$ over $x \in \beta \times \gamma$ equals the union over $i \in \beta$ and $j \in \gamma$ of $f(i,j)$. In symbols: \[ \bigcup_{x \in \beta \times \gamma} f(x) = \bigcup_{i \in \beta} \bigcup_{j \in \gamma} f(i,j). \]

Set.iUnion_prod_of_monotone theorem

 [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) :
  ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x

Full source

theorem iUnion_prod_of_monotone [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s)
    (ht : Monotone t) : ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x := by
  ext ⟨z, w⟩; simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]; constructor
  · intro x hz hw
    exact ⟨⟨x, hz⟩, x, hw⟩
  · intro x hz x' hw
    exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

Union of Product Sets Equals Product of Unions for Monotone Families

Informal description

Let $\alpha$ be a semilattice with a supremum operation, and let $s : \alpha \to \mathcal{P}(\beta)$ and $t : \alpha \to \mathcal{P}(\gamma)$ be monotone set-valued functions. Then the union over $x \in \alpha$ of the product sets $s(x) \times t(x)$ is equal to the product of the unions: \[ \bigcup_{x \in \alpha} (s(x) \times t(x)) = \left(\bigcup_{x \in \alpha} s(x)\right) \times \left(\bigcup_{x \in \alpha} t(x)\right). \]

Set.sInter_prod_sInter_subset theorem

(S : Set (Set α)) (T : Set (Set β)) : ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Full source

theorem sInter_prod_sInter_subset (S : Set (Set α)) (T : Set (Set β)) :
    ⋂₀ S⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 :=
  subset_iInter₂ fun x hx _ hy => ⟨hy.1 x.1 hx.1, hy.2 x.2 hx.2⟩

Subset Relation for Product of Set Intersections

Informal description

For any families of sets $S \subseteq \mathcal{P}(\alpha)$ and $T \subseteq \mathcal{P}(\beta)$, the Cartesian product of their intersections satisfies \[ \bigcap S \times \bigcap T \subseteq \bigcap_{(s,t) \in S \times T} (s \times t). \]

Set.sInter_prod_sInter theorem

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

Full source

theorem sInter_prod_sInter {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) :
    ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 := by
  obtain ⟨s₁, h₁⟩ := hS
  obtain ⟨s₂, h₂⟩ := hT
  refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_
  rw [mem_iInter₂] at hx
  exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

Product of Set Intersections Equals Intersection of Products for Nonempty Families

Informal description

For any nonempty families of sets $S \subseteq \mathcal{P}(\alpha)$ and $T \subseteq \mathcal{P}(\beta)$, the Cartesian product of their intersections satisfies \[ \bigcap S \times \bigcap T = \bigcap_{(s,t) \in S \times T} (s \times t). \]

Set.sInter_prod theorem

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

Full source

theorem sInter_prod {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) :
    ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t := by
  rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]
  simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Cartesian Product Distributes over Intersection: $\left( \bigcap S \right) \times t = \bigcap_{s \in S} (s \times t)$

Informal description

For any nonempty family of sets $S \subseteq \mathcal{P}(\alpha)$ and any set $t \subseteq \beta$, the Cartesian product of the intersection of $S$ with $t$ equals the intersection over all $s \in S$ of the Cartesian products $s \times t$. That is, \[ \bigcap S \times t = \bigcap_{s \in S} (s \times t). \]

Set.prod_sInter theorem

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

Full source

theorem prod_sInter {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) :
    s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t := by
  rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
  simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Cartesian Product Distributes over Intersection: $s \times \left( \bigcap T \right) = \bigcap_{t \in T} (s \times t)$

Informal description

For any nonempty family of sets $T \subseteq \mathcal{P}(\beta)$ and any set $s \subseteq \alpha$, the Cartesian product of $s$ with the intersection of $T$ equals the intersection over all $t \in T$ of the Cartesian products $s \times t$. That is, \[ s \times \left( \bigcap T \right) = \bigcap_{t \in T} (s \times t). \]

Set.prod_iInter theorem

{s : Set α} {t : ι → Set β} [hι : Nonempty ι] : (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i

Full source

theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
    (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i := by
  ext x
  simp only [mem_prod, mem_iInter]
  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

Cartesian Product Distributes over Intersection: $s \times \left( \bigcap_i t_i \right) = \bigcap_i (s \times t_i)$

Informal description

For any set $s \subseteq \alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$ (where $\iota$ is nonempty), the Cartesian product of $s$ with the intersection of the $t_i$'s equals the intersection of the Cartesian products of $s$ with each $t_i$. That is, \[ s \times \left( \bigcap_{i} t_i \right) = \bigcap_{i} (s \times t_i). \]

Set.image2_eq_iUnion theorem

(s : Set α) (t : Set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j}

Full source

/-- The `Set.image2` version of `Set.image_eq_iUnion` -/
theorem image2_eq_iUnion (s : Set α) (t : Set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j} := by
  ext; simp [eq_comm]

Image of Product Set as Union of Singletons

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of $s$ and $t$ under the function $f : \alpha \to \beta \to \gamma$ can be expressed as the union over all $i \in s$ and $j \in t$ of the singletons $\{f(i, j)\}$. In other words: \[ f(s, t) = \bigcup_{i \in s} \bigcup_{j \in t} \{f(i, j)\} \]

Set.iUnion_image_left theorem

: ⋃ a ∈ s, f a '' t = image2 f s t

Full source

theorem iUnion_image_left : ⋃ a ∈ s, f a '' t = image2 f s t := by
  simp only [image2_eq_iUnion, image_eq_iUnion]

Union of Images Equals Image of Product Set

Informal description

For any function $f : \alpha \to \beta \to \gamma$, any set $s \subseteq \alpha$, and any set $t \subseteq \beta$, the union over all $a \in s$ of the images $f(a)(t)$ equals the image of $s$ and $t$ under $f$. In other words: \[ \bigcup_{a \in s} f(a)(t) = f(s, t) \]

Set.iUnion_image_right theorem

: ⋃ b ∈ t, (f · b) '' s = image2 f s t

Full source

theorem iUnion_image_right : ⋃ b ∈ t, (f · b) '' s = image2 f s t := by
  rw [image2_swap, iUnion_image_left]

Union of Right Images Equals Image of Product Set

Informal description

For any function $f : \alpha \to \beta \to \gamma$, any set $s \subseteq \alpha$, and any set $t \subseteq \beta$, the union over all $b \in t$ of the images $f(\cdot, b)(s)$ equals the image of $s$ and $t$ under $f$. In other words: \[ \bigcup_{b \in t} \{f(a, b) \mid a \in s\} = f(s, t) \]

Set.image2_iUnion_left theorem

(s : ι → Set α) (t : Set β) : image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t

Full source

theorem image2_iUnion_left (s : ι → Set α) (t : Set β) :
    image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t := by
  simp only [← image_prod, iUnion_prod_const, image_iUnion]

Image of Union under Binary Operation: $f(\bigcup_i s_i, t) = \bigcup_i f(s_i, t)$

Informal description

For any function $f : \alpha \times \beta \to \gamma$, any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$, and any set $t \subseteq \beta$, the image of the union $\bigcup_i s_i$ and $t$ under $f$ equals the union of the images $f(s_i, t)$ for all $i \in \iota$. In symbols: $$ f\left(\bigcup_{i} s_i, t\right) = \bigcup_{i} f(s_i, t). $$

Set.image2_iUnion_right theorem

(s : Set α) (t : ι → Set β) : image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i)

Full source

theorem image2_iUnion_right (s : Set α) (t : ι → Set β) :
    image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i) := by
  simp only [← image_prod, prod_iUnion, image_iUnion]

Image of Union under Binary Operation: $f(s, \bigcup_i t_i) = \bigcup_i f(s, t_i)$

Informal description

For any function $f : \alpha \times \beta \to \gamma$, any set $s \subseteq \alpha$, and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the image of $s$ and the union $\bigcup_i t_i$ under $f$ equals the union of the images $f(s, t_i)$ for all $i \in \iota$. In symbols: $$ f\left(s, \bigcup_{i} t_i\right) = \bigcup_{i} f(s, t_i). $$

Set.image2_sUnion_left theorem

(S : Set (Set α)) (t : Set β) : image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t

Full source

theorem image2_sUnion_left (S : Set (Set α)) (t : Set β) :
    image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t := by
  aesop

Image of Union under Binary Operation

Informal description

For any family of sets $S$ in $\alpha$ and any set $t \subseteq \beta$, the image of the union $\bigcup S$ under the binary operation $f$ paired with $t$ equals the union over all $s \in S$ of the images $f(s, t)$. In symbols: $$ f\left(\bigcup S, t\right) = \bigcup_{s \in S} f(s, t) $$

Set.image2_sUnion_right theorem

(s : Set α) (T : Set (Set β)) : image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t

Full source

theorem image2_sUnion_right (s : Set α) (T : Set (Set β)) :
    image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t := by
  aesop

Image of Union under Binary Operation

Informal description

For any set $s \subseteq \alpha$ and any family of sets $T \subseteq \mathcal{P}(\beta)$, the image of $s$ under the binary operation $f$ with respect to the union of all sets in $T$ is equal to the union over all $t \in T$ of the images of $s$ under $f$ with respect to $t$. In symbols: $$ f(s, \bigcup T) = \bigcup_{t \in T} f(s, t) $$

Set.image2_iUnion₂_left theorem

(s : ∀ i, κ i → Set α) (t : Set β) : image2 f (⋃ (i) (j), s i j) t = ⋃ (i) (j), image2 f (s i j) t

Full source

theorem image2_iUnion₂_left (s : ∀ i, κ i → Set α) (t : Set β) :
    image2 f (⋃ (i) (j), s i j) t = ⋃ (i) (j), image2 f (s i j) t := by simp_rw [image2_iUnion_left]

Image of Doubly-Indexed Union under Binary Operation: $f(\bigcup_{i,j} s_{i,j}, t) = \bigcup_{i,j} f(s_{i,j}, t)$

Informal description

For any function $f : \alpha \times \beta \to \gamma$, any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $\alpha$, and any set $t \subseteq \beta$, the image of the union $\bigcup_{i,j} s_{i,j}$ and $t$ under $f$ equals the union of the images $f(s_{i,j}, t)$ for all $i \in \iota$ and $j \in \kappa_i$. In symbols: $$ f\left(\bigcup_{i,j} s_{i,j}, t\right) = \bigcup_{i,j} f(s_{i,j}, t). $$

Set.image2_iUnion₂_right theorem

(s : Set α) (t : ∀ i, κ i → Set β) : image2 f s (⋃ (i) (j), t i j) = ⋃ (i) (j), image2 f s (t i j)

Full source

theorem image2_iUnion₂_right (s : Set α) (t : ∀ i, κ i → Set β) :
    image2 f s (⋃ (i) (j), t i j) = ⋃ (i) (j), image2 f s (t i j) := by
  simp_rw [image2_iUnion_right]

Image of Doubly-Indexed Union under Binary Operation: $f(s, \bigcup_{i,j} t_{i,j}) = \bigcup_{i,j} f(s, t_{i,j})$

Informal description

For any function $f : \alpha \times \beta \to \gamma$, 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 image of $s$ and the union $\bigcup_{i,j} t_{i,j}$ under $f$ equals the union of the images $f(s, t_{i,j})$ for all $i \in \iota$ and $j \in \kappa_i$. In symbols: $$ f\left(s, \bigcup_{i,j} t_{i,j}\right) = \bigcup_{i,j} f(s, t_{i,j}). $$

Set.image2_iInter_subset_left theorem

(s : ι → Set α) (t : Set β) : image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

Full source

theorem image2_iInter_subset_left (s : ι → Set α) (t : Set β) :
    image2image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t := by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i => mem_image2_of_mem (hx _) hy

Image of Intersection under Binary Operation is Subset of Intersection of Images

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ and any set $t \subseteq \beta$, the image of the intersection $\bigcap_i s_i$ under the binary operation $f$ applied with $t$ is contained in the intersection of the images of each $s_i$ under $f$ with $t$. That is, $$ f\left(\bigcap_{i} s_i, t\right) \subseteq \bigcap_{i} f(s_i, t). $$

Set.image2_iInter_subset_right theorem

(s : Set α) (t : ι → Set β) : image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Full source

theorem image2_iInter_subset_right (s : Set α) (t : ι → Set β) :
    image2image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i) := by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

Image of Intersection is Subset of Intersection of Images (Right Argument)

Informal description

For any set $s \subseteq \alpha$ and any family of sets $t_i \subseteq \beta$ indexed by $i \in \iota$, the image of $s$ and the intersection of the $t_i$ under a function $f$ is contained in the intersection of the images of $s$ and each $t_i$ under $f$. In symbols: $$ f(s, \bigcap_{i} t_i) \subseteq \bigcap_{i} f(s, t_i) $$

Set.image2_iInter₂_subset_left theorem

(s : ∀ i, κ i → Set α) (t : Set β) : image2 f (⋂ (i) (j), s i j) t ⊆ ⋂ (i) (j), image2 f (s i j) t

Full source

theorem image2_iInter₂_subset_left (s : ∀ i, κ i → Set α) (t : Set β) :
    image2image2 f (⋂ (i) (j), s i j) t ⊆ ⋂ (i) (j), image2 f (s i j) t := by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

Image of Intersection under Binary Operation is Contained in Intersection of Images

Informal description

Let $f : \alpha \times \beta \to \gamma$ be a function, 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 image of the intersection $\bigcap_{i,j} s_{i,j}$ and $t$ under $f$ is contained in the intersection of the images of each $s_{i,j}$ and $t$ under $f$, i.e., $$ f\left(\bigcap_{i,j} s_{i,j} \times t\right) \subseteq \bigcap_{i,j} f(s_{i,j} \times t). $$

Set.image2_iInter₂_subset_right theorem

(s : Set α) (t : ∀ i, κ i → Set β) : image2 f s (⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), image2 f s (t i j)

Full source

theorem image2_iInter₂_subset_right (s : Set α) (t : ∀ i, κ i → Set β) :
    image2image2 f s (⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), image2 f s (t i j) := by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)

Image of Intersection Under Binary Operation is Contained in Intersection of Images

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, $s$ be a subset of $\alpha$, and for each $i$ and $j$, let $t_{i,j}$ be a subset of $\beta$. Then the image of $s$ and the intersection of all $t_{i,j}$ under $f$ is contained in the intersection of all images of $s$ and $t_{i,j}$ under $f$. In symbols: $$ f(s, \bigcap_{i,j} t_{i,j}) \subseteq \bigcap_{i,j} f(s, t_{i,j}) $$

Set.image2_sInter_subset_left theorem

(S : Set (Set α)) (t : Set β) : image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Full source

theorem image2_sInter_subset_left (S : Set (Set α)) (t : Set β) :
    image2image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t := by
  rw [sInter_eq_biInter]
  exact image2_iInter₂_subset_left ..

Image of Set Intersection under Binary Operation is Contained in Intersection of Images

Informal description

Let $f : \alpha \times \beta \to \gamma$ be a function, let $S$ be a family of subsets of $\alpha$, and let $t$ be a subset of $\beta$. Then the image of the intersection $\bigcap S$ and $t$ under $f$ is contained in the intersection of the images of each $s \in S$ and $t$ under $f$, i.e., $$ f\left(\bigcap S \times t\right) \subseteq \bigcap_{s \in S} f(s \times t). $$

Set.image2_sInter_subset_right theorem

(s : Set α) (T : Set (Set β)) : image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Full source

theorem image2_sInter_subset_right (s : Set α) (T : Set (Set β)) :
    image2image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t := by
  rw [sInter_eq_biInter]
  exact image2_iInter₂_subset_right ..

Image of Intersection Under Binary Operation is Contained in Intersection of Images (Right Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, $s$ be a subset of $\alpha$, and $T$ be a set of subsets of $\beta$. Then the image of $s$ and the intersection of all sets in $T$ under $f$ is contained in the intersection of all images of $s$ and each individual set $t \in T$ under $f$. In symbols: $$ f(s, \bigcap T) \subseteq \bigcap_{t \in T} f(s, t) $$

Set.prod_eq_biUnion_left theorem

: s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t

Full source

theorem prod_eq_biUnion_left : s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t := by
  rw [iUnion_image_left, image2_mk_eq_prod]

Cartesian Product as Union of Fibers Over First Component

Informal description

For any sets $s$ and $t$, the Cartesian product $s \times t$ is equal to the union over all elements $a \in s$ of the images of $t$ under the function $b \mapsto (a, b)$. In other words: \[ s \times t = \bigcup_{a \in s} \{ (a, b) \mid b \in t \} \]

Set.prod_eq_biUnion_right theorem

: s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s

Full source

theorem prod_eq_biUnion_right : s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s := by
  rw [iUnion_image_right, image2_mk_eq_prod]

Cartesian Product as Union of Fibers Over Second Component

Informal description

For any sets $s$ and $t$, the Cartesian product $s \times t$ is equal to the union over all elements $b \in t$ of the images of $s$ under the function $a \mapsto (a, b)$. In other words: \[ s \times t = \bigcup_{b \in t} \{ (a, b) \mid a \in s \} \]

Set.seq_def theorem

{s : Set (α → β)} {t : Set α} : seq s t = ⋃ f ∈ s, f '' t

Full source

theorem seq_def {s : Set (α → β)} {t : Set α} : seq s t = ⋃ f ∈ s, f '' t := by
  rw [seq_eq_image2, iUnion_image_left]

Sequential Composition as Union of Images

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$ and any set $t \subseteq \alpha$, the sequential composition $s \mathbin{\texttt{seq}} t$ is equal to the union over all functions $f \in s$ of the image of $t$ under $f$. In other words: \[ s \mathbin{\texttt{seq}} t = \bigcup_{f \in s} f(t) \]

Set.seq_subset theorem

{s : Set (α → β)} {t : Set α} {u : Set β} : seq s t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, (f : α → β) a ∈ u

Full source

theorem seq_subset {s : Set (α → β)} {t : Set α} {u : Set β} :
    seqseq s t ⊆ useq s t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, (f : α → β) a ∈ u :=
  image2_subset_iff

Sequential Composition Subset Criterion

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$, any set $t \subseteq \alpha$, and any set $u \subseteq \beta$, the sequential composition $s \mathbin{\texttt{seq}} t$ is a subset of $u$ if and only if for every function $f \in s$ and every element $a \in t$, the application $f(a)$ belongs to $u$.

Set.seq_mono theorem

 {s₀ s₁ : Set (α → β)} {t₀ t₁ : Set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) : seq s₀ t₀ ⊆ seq s₁ t₁

Full source

@[gcongr, mono]
theorem seq_mono {s₀ s₁ : Set (α → β)} {t₀ t₁ : Set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) :
    seqseq s₀ t₀ ⊆ seq s₁ t₁ := image2_subset hs ht

Monotonicity of Sequential Composition with Respect to Subsets

Informal description

For any sets $s_0, s_1$ of functions from $\alpha$ to $\beta$ and any sets $t_0, t_1$ of elements of $\alpha$, if $s_0 \subseteq s_1$ and $t_0 \subseteq t_1$, then the sequential composition of $s_0$ and $t_0$ is a subset of the sequential composition of $s_1$ and $t_1$.

Set.singleton_seq theorem

{f : α → β} {t : Set α} : Set.seq ({ f } : Set (α → β)) t = f '' t

Full source

theorem singleton_seq {f : α → β} {t : Set α} : Set.seq ({f} : Set (α → β)) t = f '' t :=
  image2_singleton_left

Sequential Application of Singleton Function Set Equals Image

Informal description

For any function $f : \alpha \to \beta$ and any subset $t \subseteq \alpha$, the sequential application of the singleton set $\{f\}$ to $t$ equals the image of $t$ under $f$, i.e., $$\{f\} \mathbin{\text{seq}} t = f(t).$$

Set.seq_singleton theorem

{s : Set (α → β)} {a : α} : Set.seq s { a } = (fun f : α → β => f a) '' s

Full source

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

Evaluation of Function Set on Singleton

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$ and any singleton set $\{a\}$ in $\alpha$, the sequential application of $s$ to $\{a\}$ is equal to the image of $s$ under the evaluation map at $a$, i.e., $$ s \cdot \{a\} = \{ f(a) \mid f \in s \}. $$

Set.seq_seq theorem

{s : Set (β → γ)} {t : Set (α → β)} {u : Set α} : seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u

Full source

theorem seq_seq {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} :
    seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u := by
  simp only [seq_eq_image2, image2_image_left]
  exact .symm <| image2_assoc fun _ _ _ ↦ rfl

Associativity of Sequential Composition of Function Sets

Informal description

For any sets $s$ of functions from $\beta$ to $\gamma$, $t$ of functions from $\alpha$ to $\beta$, and $u$ of elements in $\alpha$, the sequential composition of $s$ with the sequential composition of $t$ and $u$ is equal to the sequential composition of the sequential composition of the set of function compositions $\{f \circ g \mid f \in s\}$ with $t$, and $u$. In symbols: $$ s \mathbin{\text{seq}} (t \mathbin{\text{seq}} u) = \big(\{f \circ g \mid f \in s\} \mathbin{\text{seq}} t\big) \mathbin{\text{seq}} u $$

Set.image_seq theorem

{f : β → γ} {s : Set (α → β)} {t : Set α} : f '' seq s t = seq ((f ∘ ·) '' s) t

Full source

theorem image_seq {f : β → γ} {s : Set (α → β)} {t : Set α} :
    f '' seq s t = seq ((f ∘ ·) '' s) t := by
  simp only [seq, image_image2, image2_image_left, comp_apply]

Image of Sequential Application Equals Sequential Application of Composed Functions

Informal description

For any function $f : \beta \to \gamma$, set of functions $s \subseteq (\alpha \to \beta)$, and set $t \subseteq \alpha$, the image of the sequential application $f(s(t))$ equals the sequential application of the composed functions $(f \circ \cdot)(s)$ to $t$. In symbols: $$ f \text{''} (s \text{ seq } t) = (f \circ \cdot) \text{''} s \text{ seq } t $$

Set.prod_eq_seq theorem

{s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t

Full source

theorem prod_eq_seq {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mkProd.mk '' s).seq t := by
  rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

Cartesian Product as Sequential Image Application

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is equal to the sequential application of the image of the pairing function $\text{Prod.mk}$ on $s$ followed by $t$. In symbols: $s \times t = \text{seq}(\text{Prod.mk} \ '' \ s) \ t$.

Set.prod_image_seq_comm theorem

(s : Set α) (t : Set β) : (Prod.mk '' s).seq t = seq ((fun b a => (a, b)) '' t) s

Full source

theorem prod_image_seq_comm (s : Set α) (t : Set β) :
    (Prod.mkProd.mk '' s).seq t = seq ((fun b a => (a, b)) '' t) s := by
  rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]; rfl

Commutativity of Sequential Application for Cartesian Product Construction

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the sequential application of the image of the pairing function $\text{Prod.mk}$ on $s$ to $t$ is equal to the sequential application of the image of the reversed pairing function $\lambda b a \mapsto (a, b)$ on $t$ to $s$. In symbols: $$ \text{seq}(\text{Prod.mk} \ '' \ s) \ t = \text{seq}((\lambda b a \mapsto (a, b)) \ '' \ t) \ s $$

Set.image2_eq_seq theorem

(f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = seq (f '' s) t

Full source

theorem image2_eq_seq (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = seq (f '' s) t := by
  rw [seq_eq_image2, image2_image_left]

Image of Binary Function as Sequential Application

Informal description

For any function $f \colon \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ over $s$ and $t$ is equal to the sequential application of the image of $f$ over $s$ to $t$, i.e., \[ \text{image2}(f, s, t) = \text{seq}(f '' s, t). \]

Mathlib.Data.Set.Lattice.Image

Naming convention

Notation