data.set.lattice

# The set lattice #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides usual set notation for unions and intersections, a `complete_lattice` instance for `set α`, and some more set constructions.

## Main declarations #

• `set.Union`: Union of an indexed family of sets.
• `set.Inter`: Intersection of an indexed family of sets.
• `set.sInter`: set Inter. Intersection of sets belonging to a set of sets.
• `set.sUnion`: set Union. Union of sets belonging to a set of sets. This is actually defined in core Lean.
• `set.sInter_eq_bInter`, `set.sUnion_eq_bInter`: Shows that `⋂₀ s = ⋂ x ∈ s, x` and `⋃₀ s = ⋃ x ∈ s, x`.
• `set.complete_boolean_algebra`: `set α` is a `complete_boolean_algebra` with `≤ = ⊆`, `< = ⊂`, `⊓ = ∩`, `⊔ = ∪`, `⨅ = ⋂`, `⨆ = ⋃` and `\` as the set difference. See `set.boolean_algebra`.
• `set.kern_image`: For a function `f : α → β`, `s.kern_image f` is the set of `y` such that `f ⁻¹ y ⊆ s`.
• `set.seq`: Union of the image of a set under a sequence of functions. `seq s t` is the union of `f '' t` over all `f ∈ s`, where `t : set α` and `s : set (α → β)`.
• `set.Union_eq_sigma_of_disjoint`: Equivalence between `⋃ i, t i` and `Σ i, t i`, where `t` is an indexed family of disjoint sets.

## Naming convention #

In lemma names,

• `⋃ i, s i` is called `Union`
• `⋂ i, s i` is called `Inter`
• `⋃ i j, s i j` is called `Union₂`. This is a `Union` inside a `Union`.
• `⋂ i j, s i j` is called `Inter₂`. This is an `Inter` inside an `Inter`.
• `⋃ i ∈ s, t i` is called `bUnion` for "bounded `Union`". This is the special case of `Union₂` where `j : i ∈ s`.
• `⋂ i ∈ s, t i` is called `bInter` for "bounded `Inter`". This is the special case of `Inter₂` where `j : i ∈ s`.

## Notation #

• `⋃`: `set.Union`
• `⋂`: `set.Inter`
• `⋃₀`: `set.sUnion`
• `⋂₀`: `set.sInter`

### Complete lattice and complete Boolean algebra instances #

@[protected, instance]
def set.has_Inf {α : Type u_1} :
Equations
@[protected, instance]
def set.has_Sup {α : Type u_1} :
Equations
def set.sInter {α : Type u_1} (S : set (set α)) :
set α

Intersection of a set of sets.

Equations
def set.sUnion {α : Type u_1} (S : set (set α)) :
set α

Union of a set of sets.

Equations
Instances for `↥set.sUnion`
@[simp]
theorem set.mem_sInter {α : Type u_1} {x : α} {S : set (set α)} :
x ⋂₀ S (t : set α), t S x t
@[simp]
theorem set.mem_sUnion {α : Type u_1} {x : α} {S : set (set α)} :
x ⋃₀ S (t : set α) (H : t S), x t
def set.Union {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
set β

Indexed union of a family of sets

Equations
Instances for `↥set.Union`
def set.Inter {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
set β

Indexed intersection of a family of sets

Equations
Instances for `set.Inter`
Instances for `↥set.Inter`
@[simp]
theorem set.Sup_eq_sUnion {α : Type u_1} (S : set (set α)) :
@[simp]
theorem set.Inf_eq_sInter {α : Type u_1} (S : set (set α)) :
@[simp]
theorem set.supr_eq_Union {α : Type u_1} {ι : Sort u_4} (s : ι set α) :
supr s =
@[simp]
theorem set.infi_eq_Inter {α : Type u_1} {ι : Sort u_4} (s : ι set α) :
infi s =
@[simp]
theorem set.mem_Union {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι set α} :
(x (i : ι), s i) (i : ι), x s i
@[simp]
theorem set.mem_Inter {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι set α} :
(x (i : ι), s i) (i : ι), x s i
theorem set.mem_Union₂ {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} {x : γ} {s : Π (i : ι), κ i set γ} :
(x (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), x s i j
theorem set.mem_Inter₂ {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} {x : γ} {s : Π (i : ι), κ i set γ} :
(x (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), x s i j
theorem set.mem_Union_of_mem {α : Type u_1} {ι : Sort u_4} {s : ι set α} {a : α} (i : ι) (ha : a s i) :
a (i : ι), s i
theorem set.mem_Union₂_of_mem {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {a : α} {i : ι} (j : κ i) (ha : a s i j) :
a (i : ι) (j : κ i), s i j
theorem set.mem_Inter_of_mem {α : Type u_1} {ι : Sort u_4} {s : ι set α} {a : α} (h : (i : ι), a s i) :
a (i : ι), s i
theorem set.mem_Inter₂_of_mem {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {a : α} (h : (i : ι) (j : κ i), a s i j) :
a (i : ι) (j : κ i), s i j
@[protected, instance]
Equations
@[protected]
theorem set.image_preimage {α : Type u_1} {β : Type u_2} {f : α β} :
def set.kern_image {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
set β

`kern_image f s` is the set of `y` such that `f ⁻¹ y ⊆ s`.

Equations
@[protected]
theorem set.preimage_kern_image {α : Type u_1} {β : Type u_2} {f : α β} :

### Union and intersection over an indexed family of sets #

@[protected, instance]
def set.order_top {α : Type u_1} :
Equations
theorem set.Union_congr_Prop {α : Type u_1} {p q : Prop} {f₁ : p set α} {f₂ : q set α} (pq : p q) (f : (x : q), f₁ _ = f₂ x) :
=
theorem set.Inter_congr_Prop {α : Type u_1} {p q : Prop} {f₁ : p set α} {f₂ : q set α} (pq : p q) (f : (x : q), f₁ _ = f₂ x) :
=
theorem set.Union_plift_up {α : Type u_1} {ι : Sort u_4} (f : set α) :
( (i : ι), f {down := i}) = (i : plift ι), f i
theorem set.Union_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι set α) :
( (i : plift ι), f i.down) = (i : ι), f i
theorem set.Inter_plift_up {α : Type u_1} {ι : Sort u_4} (f : set α) :
( (i : ι), f {down := i}) = (i : plift ι), f i
theorem set.Inter_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι set α) :
( (i : plift ι), f i.down) = (i : ι), f i
theorem set.Union_eq_if {α : Type u_1} {p : Prop} [decidable p] (s : set α) :
( (h : p), s) = ite p s
theorem set.Union_eq_dif {α : Type u_1} {p : Prop} [decidable p] (s : p set α) :
( (h : p), s h) = dite p (λ (h : p), s h) (λ (h : ¬p), )
theorem set.Inter_eq_if {α : Type u_1} {p : Prop} [decidable p] (s : set α) :
( (h : p), s) = ite p s set.univ
theorem set.Infi_eq_dif {α : Type u_1} {p : Prop} [decidable p] (s : p set α) :
( (h : p), s h) = dite p (λ (h : p), s h) (λ (h : ¬p), set.univ)
theorem set.exists_set_mem_of_union_eq_top {β : Type u_2} {ι : Type u_1} (t : set ι) (s : ι set β) (w : ( (i : ι) (H : i t), s i) = ) (x : β) :
(i : ι) (H : i t), x s i
theorem set.nonempty_of_union_eq_top_of_nonempty {α : Type u_1} {ι : Type u_2} (t : set ι) (s : ι set α) (H : nonempty α) (w : ( (i : ι) (H : i t), s i) = ) :
theorem set.set_of_exists {β : Type u_2} {ι : Sort u_4} (p : ι β Prop) :
{x : β | (i : ι), p i x} = (i : ι), {x : β | p i x}
theorem set.set_of_forall {β : Type u_2} {ι : Sort u_4} (p : ι β Prop) :
{x : β | (i : ι), p i x} = (i : ι), {x : β | p i x}
theorem set.Union_subset {α : Type u_1} {ι : Sort u_4} {s : ι set α} {t : set α} (h : (i : ι), s i t) :
( (i : ι), s i) t
theorem set.Union₂_subset {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : set α} (h : (i : ι) (j : κ i), s i j t) :
( (i : ι) (j : κ i), s i j) t
theorem set.subset_Inter {β : Type u_2} {ι : Sort u_4} {t : set β} {s : ι set β} (h : (i : ι), t s i) :
t (i : ι), s i
theorem set.subset_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set α} (h : (i : ι) (j : κ i), s t i j) :
s (i : ι) (j : κ i), t i j
@[simp]
theorem set.Union_subset_iff {α : Type u_1} {ι : Sort u_4} {s : ι set α} {t : set α} :
( (i : ι), s i) t (i : ι), s i t
theorem set.Union₂_subset_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : set α} :
( (i : ι) (j : κ i), s i j) t (i : ι) (j : κ i), s i j t
@[simp]
theorem set.subset_Inter_iff {α : Type u_1} {ι : Sort u_4} {s : set α} {t : ι set α} :
(s (i : ι), t i) (i : ι), s t i
@[simp]
theorem set.subset_Inter₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set α} :
(s (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), s t i j
theorem set.subset_Union {β : Type u_2} {ι : Sort u_4} (s : ι set β) (i : ι) :
s i (i : ι), s i
theorem set.Inter_subset {β : Type u_2} {ι : Sort u_4} (s : ι set β) (i : ι) :
( (i : ι), s i) s i
theorem set.subset_Union₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} (i : ι) (j : κ i) :
s i j (i : ι) (j : κ i), s i j
theorem set.Inter₂_subset {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} (i : ι) (j : κ i) :
( (i : ι) (j : κ i), s i j) s i j
theorem set.subset_Union_of_subset {α : Type u_1} {ι : Sort u_4} {s : set α} {t : ι set α} (i : ι) (h : s t i) :
s (i : ι), t i

This rather trivial consequence of `subset_Union`is convenient with `apply`, and has `i` explicit for this purpose.

theorem set.Inter_subset_of_subset {α : Type u_1} {ι : Sort u_4} {s : ι set α} {t : set α} (i : ι) (h : s i t) :
( (i : ι), s i) t

This rather trivial consequence of `Inter_subset`is convenient with `apply`, and has `i` explicit for this purpose.

theorem set.subset_Union₂_of_subset {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set α} (i : ι) (j : κ i) (h : s t i j) :
s (i : ι) (j : κ i), t i j

This rather trivial consequence of `subset_Union₂` is convenient with `apply`, and has `i` and `j` explicit for this purpose.

theorem set.Inter₂_subset_of_subset {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : set α} (i : ι) (j : κ i) (h : s i j t) :
( (i : ι) (j : κ i), s i j) t

This rather trivial consequence of `Inter₂_subset` is convenient with `apply`, and has `i` and `j` explicit for this purpose.

theorem set.Union_mono {α : Type u_1} {ι : Sort u_4} {s t : ι set α} (h : (i : ι), s i t i) :
( (i : ι), s i) (i : ι), t i
theorem set.Union₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s t : Π (i : ι), κ i set α} (h : (i : ι) (j : κ i), s i j t i j) :
( (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), t i j
theorem set.Inter_mono {α : Type u_1} {ι : Sort u_4} {s t : ι set α} (h : (i : ι), s i t i) :
( (i : ι), s i) (i : ι), t i
theorem set.Inter₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s t : Π (i : ι), κ i set α} (h : (i : ι) (j : κ i), s i j t i j) :
( (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), t i j
theorem set.Union_mono' {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : ι set α} {t : ι₂ set α} (h : (i : ι), (j : ι₂), s i t j) :
( (i : ι), s i) (i : ι₂), t i
theorem set.Union₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι Sort u_7} {κ' : ι' Sort u_10} {s : Π (i : ι), κ i set α} {t : Π (i' : ι'), κ' i' set α} (h : (i : ι) (j : κ i), (i' : ι') (j' : κ' i'), s i j t i' j') :
( (i : ι) (j : κ i), s i j) (i' : ι') (j' : κ' i'), t i' j'
theorem set.Inter_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ι set α} {t : ι' set α} (h : (j : ι'), (i : ι), s i t j) :
( (i : ι), s i) (j : ι'), t j
theorem set.Inter₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι Sort u_7} {κ' : ι' Sort u_10} {s : Π (i : ι), κ i set α} {t : Π (i' : ι'), κ' i' set α} (h : (i' : ι') (j' : κ' i'), (i : ι) (j : κ i), s i j t i' j') :
( (i : ι) (j : κ i), s i j) (i' : ι') (j' : κ' i'), t i' j'
theorem set.Union₂_subset_Union {α : Type u_1} {ι : Sort u_4} (κ : ι Sort u_2) (s : ι set α) :
( (i : ι) (j : κ i), s i) (i : ι), s i
theorem set.Inter_subset_Inter₂ {α : Type u_1} {ι : Sort u_4} (κ : ι Sort u_2) (s : ι set α) :
( (i : ι), s i) (i : ι) (j : κ i), s i
theorem set.Union_set_of {α : Type u_1} {ι : Sort u_4} (P : ι α Prop) :
( (i : ι), {x : α | P i x}) = {x : α | (i : ι), P i x}
theorem set.Inter_set_of {α : Type u_1} {ι : Sort u_4} (P : ι α Prop) :
( (i : ι), {x : α | P i x}) = {x : α | (i : ι), P i x}
theorem set.Union_congr_of_surjective {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι set α} {g : ι₂ set α} (h : ι ι₂) (h1 : function.surjective h) (h2 : (x : ι), g (h x) = f x) :
( (x : ι), f x) = (y : ι₂), g y
theorem set.Inter_congr_of_surjective {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι set α} {g : ι₂ set α} (h : ι ι₂) (h1 : function.surjective h) (h2 : (x : ι), g (h x) = f x) :
( (x : ι), f x) = (y : ι₂), g y
theorem set.Union_congr {α : Type u_1} {ι : Sort u_4} {s t : ι set α} (h : (i : ι), s i = t i) :
( (i : ι), s i) = (i : ι), t i
theorem set.Inter_congr {α : Type u_1} {ι : Sort u_4} {s t : ι set α} (h : (i : ι), s i = t i) :
( (i : ι), s i) = (i : ι), t i
theorem set.Union₂_congr {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s t : Π (i : ι), κ i set α} (h : (i : ι) (j : κ i), s i j = t i j) :
( (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), t i j
theorem set.Inter₂_congr {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s t : Π (i : ι), κ i set α} (h : (i : ι) (j : κ i), s i j = t i j) :
( (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), t i j
theorem set.Union_const {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) :
( (i : ι), s) = s
theorem set.Inter_const {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) :
( (i : ι), s) = s
theorem set.Union_eq_const {α : Type u_1} {ι : Sort u_4} [nonempty ι] {f : ι set α} {s : set α} (hf : (i : ι), f i = s) :
( (i : ι), f i) = s
theorem set.Inter_eq_const {α : Type u_1} {ι : Sort u_4} [nonempty ι] {f : ι set α} {s : set α} (hf : (i : ι), f i = s) :
( (i : ι), f i) = s
@[simp]
theorem set.compl_Union {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
( (i : ι), s i) = (i : ι), (s i)
theorem set.compl_Union₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) :
( (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), (s i j)
@[simp]
theorem set.compl_Inter {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
( (i : ι), s i) = (i : ι), (s i)
theorem set.compl_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) :
( (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), (s i j)
theorem set.Union_eq_compl_Inter_compl {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
( (i : ι), s i) = ( (i : ι), (s i))
theorem set.Inter_eq_compl_Union_compl {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
( (i : ι), s i) = ( (i : ι), (s i))
theorem set.inter_Union {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι set β) :
(s (i : ι), t i) = (i : ι), s t i
theorem set.Union_inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι set β) :
( (i : ι), t i) s = (i : ι), t i s
theorem set.Union_union_distrib {β : Type u_2} {ι : Sort u_4} (s t : ι set β) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.Inter_inter_distrib {β : Type u_2} {ι : Sort u_4} (s t : ι set β) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.union_Union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι set β) :
(s (i : ι), t i) = (i : ι), s t i
theorem set.Union_union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι set β) :
( (i : ι), t i) s = (i : ι), t i s
theorem set.inter_Inter {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι set β) :
(s (i : ι), t i) = (i : ι), s t i
theorem set.Inter_inter {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι set β) :
( (i : ι), t i) s = (i : ι), t i s
theorem set.union_Inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι set β) :
(s (i : ι), t i) = (i : ι), s t i
theorem set.Inter_union {β : Type u_2} {ι : Sort u_4} (s : ι set β) (t : set β) :
( (i : ι), s i) t = (i : ι), s i t
theorem set.Union_diff {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι set β) :
( (i : ι), t i) \ s = (i : ι), t i \ s
theorem set.diff_Union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι set β) :
(s \ (i : ι), t i) = (i : ι), s \ t i
theorem set.diff_Inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι set β) :
(s \ (i : ι), t i) = (i : ι), s \ t i
theorem set.directed_on_Union {α : Type u_1} {ι : Sort u_4} {r : α α Prop} {f : ι set α} (hd : f) (h : (x : ι), (f x)) :
( (x : ι), f x)
theorem set.Union_inter_subset {ι : Sort u_1} {α : Type u_2} {s t : ι set α} :
( (i : ι), s i t i) ( (i : ι), s i) (i : ι), t i
theorem set.Union_inter_of_monotone {ι : Type u_1} {α : Type u_2} [preorder ι] {s t : ι set α} (hs : monotone s) (ht : monotone t) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.Union_inter_of_antitone {ι : Type u_1} {α : Type u_2} [preorder ι] {s t : ι set α} (hs : antitone s) (ht : antitone t) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.Inter_union_of_monotone {ι : Type u_1} {α : Type u_2} [preorder ι] {s t : ι set α} (hs : monotone s) (ht : monotone t) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.Inter_union_of_antitone {ι : Type u_1} {α : Type u_2} [preorder ι] {s t : ι set α} (hs : antitone s) (ht : antitone t) :
( (i : ι), s i t i) = ( (i : ι), s i) (i : ι), t i
theorem set.Union_Inter_subset {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ι ι' set α} :
( (j : ι'), (i : ι), s i j) (i : ι), (j : ι'), s i j

An equality version of this lemma is `Union_Inter_of_monotone` in `data.set.finite`.

theorem set.Union_option {α : Type u_1} {ι : Type u_2} (s : set α) :
( (o : option ι), s o) = (i : ι), s (option.some i)
theorem set.Inter_option {α : Type u_1} {ι : Type u_2} (s : set α) :
( (o : option ι), s o) = (i : ι), s (option.some i)
theorem set.Union_dite {α : Type u_1} {ι : Sort u_4} (p : ι Prop) (f : Π (i : ι), p i set α) (g : Π (i : ι), ¬p i set α) :
( (i : ι), dite (p i) (λ (h : p i), f i h) (λ (h : ¬p i), g i h)) = ( (i : ι) (h : p i), f i h) (i : ι) (h : ¬p i), g i h
theorem set.Union_ite {α : Type u_1} {ι : Sort u_4} (p : ι Prop) (f g : ι set α) :
( (i : ι), ite (p i) (f i) (g i)) = ( (i : ι) (h : p i), f i) (i : ι) (h : ¬p i), g i
theorem set.Inter_dite {α : Type u_1} {ι : Sort u_4} (p : ι Prop) (f : Π (i : ι), p i set α) (g : Π (i : ι), ¬p i set α) :
( (i : ι), dite (p i) (λ (h : p i), f i h) (λ (h : ¬p i), g i h)) = ( (i : ι) (h : p i), f i h) (i : ι) (h : ¬p i), g i h
theorem set.Inter_ite {α : Type u_1} {ι : Sort u_4} (p : ι Prop) (f g : ι set α) :
( (i : ι), ite (p i) (f i) (g i)) = ( (i : ι) (h : p i), f i) (i : ι) (h : ¬p i), g i
theorem set.image_projection_prod {ι : Type u_1} {α : ι Type u_2} {v : Π (i : ι), set (α i)} (hv : (set.univ.pi v).nonempty) (i : ι) :
((λ (x : Π (i : ι), α i), x i) '' (k : ι), (λ (x : Π (j : ι), α j), x k) ⁻¹' v k) = v i

### Unions and intersections indexed by `Prop`#

theorem set.Inter_false {α : Type u_1} {s : false set α} :
theorem set.Union_false {α : Type u_1} {s : false set α} :
@[simp]
theorem set.Inter_true {α : Type u_1} {s : true set α} :
@[simp]
theorem set.Union_true {α : Type u_1} {s : true set α} :
@[simp]
theorem set.Inter_exists {α : Type u_1} {ι : Sort u_4} {p : ι Prop} {f : set α} :
( (x : Exists p), f x) = (i : ι) (h : p i), f _
@[simp]
theorem set.Union_exists {α : Type u_1} {ι : Sort u_4} {p : ι Prop} {f : set α} :
( (x : Exists p), f x) = (i : ι) (h : p i), f _
@[simp]
theorem set.Union_empty {α : Type u_1} {ι : Sort u_4} :
( (i : ι), ) =
@[simp]
theorem set.Inter_univ {α : Type u_1} {ι : Sort u_4} :
( (i : ι), set.univ) = set.univ
@[simp]
theorem set.Union_eq_empty {α : Type u_1} {ι : Sort u_4} {s : ι set α} :
( (i : ι), s i) = (i : ι), s i =
@[simp]
theorem set.Inter_eq_univ {α : Type u_1} {ι : Sort u_4} {s : ι set α} :
( (i : ι), s i) = set.univ (i : ι), s i = set.univ
@[simp]
theorem set.nonempty_Union {α : Type u_1} {ι : Sort u_4} {s : ι set α} :
( (i : ι), s i).nonempty (i : ι), (s i).nonempty
@[simp]
theorem set.nonempty_bUnion {α : Type u_1} {β : Type u_2} {t : set α} {s : α set β} :
( (i : α) (H : i t), s i).nonempty (i : α) (H : i t), (s i).nonempty
theorem set.Union_nonempty_index {α : Type u_1} {β : Type u_2} (s : set α) (t : s.nonempty set β) :
( (h : s.nonempty), t h) = (x : α) (H : x s), t _
@[simp]
theorem set.Inter_Inter_eq_left {α : Type u_1} {β : Type u_2} {b : β} {s : Π (x : β), x = b set α} :
( (x : β) (h : x = b), s x h) = s b rfl
@[simp]
theorem set.Inter_Inter_eq_right {α : Type u_1} {β : Type u_2} {b : β} {s : Π (x : β), b = x set α} :
( (x : β) (h : b = x), s x h) = s b rfl
@[simp]
theorem set.Union_Union_eq_left {α : Type u_1} {β : Type u_2} {b : β} {s : Π (x : β), x = b set α} :
( (x : β) (h : x = b), s x h) = s b rfl
@[simp]
theorem set.Union_Union_eq_right {α : Type u_1} {β : Type u_2} {b : β} {s : Π (x : β), b = x set α} :
( (x : β) (h : b = x), s x h) = s b rfl
theorem set.Inter_or {α : Type u_1} {p q : Prop} (s : p q set α) :
( (h : p q), s h) = ( (h : p), s _) (h : q), s _
theorem set.Union_or {α : Type u_1} {p q : Prop} (s : p q set α) :
( (h : p q), s h) = ( (i : p), s _) (j : q), s _
theorem set.Union_and {α : Type u_1} {p q : Prop} (s : p q set α) :
( (h : p q), s h) = (hp : p) (hq : q), s _
theorem set.Inter_and {α : Type u_1} {p q : Prop} (s : p q set α) :
( (h : p q), s h) = (hp : p) (hq : q), s _
theorem set.Union_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ι ι' set α) :
( (i : ι) (i' : ι'), s i i') = (i' : ι') (i : ι), s i i'
theorem set.Inter_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ι ι' set α) :
( (i : ι) (i' : ι'), s i i') = (i' : ι') (i : ι), s i i'
theorem set.Union₂_comm {α : Type u_1} {ι : Sort u_4} {κ₁ : ι Sort u_8} {κ₂ : ι Sort u_9} (s : Π (i₁ : ι), κ₁ i₁ Π (i₂ : ι), κ₂ i₂ set α) :
( (i₁ : ι) (j₁ : κ₁ i₁) (i₂ : ι) (j₂ : κ₂ i₂), s i₁ j₁ i₂ j₂) = (i₂ : ι) (j₂ : κ₂ i₂) (i₁ : ι) (j₁ : κ₁ i₁), s i₁ j₁ i₂ j₂
theorem set.Inter₂_comm {α : Type u_1} {ι : Sort u_4} {κ₁ : ι Sort u_8} {κ₂ : ι Sort u_9} (s : Π (i₁ : ι), κ₁ i₁ Π (i₂ : ι), κ₂ i₂ set α) :
( (i₁ : ι) (j₁ : κ₁ i₁) (i₂ : ι) (j₂ : κ₂ i₂), s i₁ j₁ i₂ j₂) = (i₂ : ι) (j₂ : κ₂ i₂) (i₁ : ι) (j₁ : κ₁ i₁), s i₁ j₁ i₂ j₂
@[simp]
theorem set.bUnion_and {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι Prop) (q : ι ι' Prop) (s : Π (x : ι) (y : ι'), p x q x y set α) :
( (x : ι) (y : ι') (h : p x q x y), s x y h) = (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y _
@[simp]
theorem set.bUnion_and' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι' Prop) (q : ι ι' Prop) (s : Π (x : ι) (y : ι'), p y q x y set α) :
( (x : ι) (y : ι') (h : p y q x y), s x y h) = (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y _
@[simp]
theorem set.bInter_and {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι Prop) (q : ι ι' Prop) (s : Π (x : ι) (y : ι'), p x q x y set α) :
( (x : ι) (y : ι') (h : p x q x y), s x y h) = (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y _
@[simp]
theorem set.bInter_and' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι' Prop) (q : ι ι' Prop) (s : Π (x : ι) (y : ι'), p y q x y set α) :
( (x : ι) (y : ι') (h : p y q x y), s x y h) = (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y _
@[simp]
theorem set.Union_Union_eq_or_left {α : Type u_1} {β : Type u_2} {b : β} {p : β Prop} {s : Π (x : β), x = b p x set α} :
( (x : β) (h : x = b p x), s x h) = s b _ (x : β) (h : p x), s x _
@[simp]
theorem set.Inter_Inter_eq_or_left {α : Type u_1} {β : Type u_2} {b : β} {p : β Prop} {s : Π (x : β), x = b p x set α} :
( (x : β) (h : x = b p x), s x h) = s b _ (x : β) (h : p x), s x _

### Bounded unions and intersections #

theorem set.mem_bUnion {α : Type u_1} {β : Type u_2} {s : set α} {t : α set β} {x : α} {y : β} (xs : x s) (ytx : y t x) :
y (x : α) (H : x s), t x

A specialization of `mem_Union₂`.

theorem set.mem_bInter {α : Type u_1} {β : Type u_2} {s : set α} {t : α set β} {y : β} (h : (x : α), x s y t x) :
y (x : α) (H : x s), t x

A specialization of `mem_Inter₂`.

theorem set.subset_bUnion_of_mem {α : Type u_1} {β : Type u_2} {s : set α} {u : α set β} {x : α} (xs : x s) :
u x (x : α) (H : x s), u x

A specialization of `subset_Union₂`.

theorem set.bInter_subset_of_mem {α : Type u_1} {β : Type u_2} {s : set α} {t : α set β} {x : α} (xs : x s) :
( (x : α) (H : x s), t x) t x

A specialization of `Inter₂_subset`.

theorem set.bUnion_subset_bUnion_left {α : Type u_1} {β : Type u_2} {s s' : set α} {t : α set β} (h : s s') :
( (x : α) (H : x s), t x) (x : α) (H : x s'), t x
theorem set.bInter_subset_bInter_left {α : Type u_1} {β : Type u_2} {s s' : set α} {t : α set β} (h : s' s) :
( (x : α) (H : x s), t x) (x : α) (H : x s'), t x
theorem set.bUnion_mono {α : Type u_1} {β : Type u_2} {s s' : set α} {t t' : α set β} (hs : s' s) (h : (x : α), x s t x t' x) :
( (x : α) (H : x s'), t x) (x : α) (H : x s), t' x
theorem set.bInter_mono {α : Type u_1} {β : Type u_2} {s s' : set α} {t t' : α set β} (hs : s s') (h : (x : α), x s t x t' x) :
( (x : α) (H : x s'), t x) (x : α) (H : x s), t' x
theorem set.bUnion_eq_Union {α : Type u_1} {β : Type u_2} (s : set α) (t : Π (x : α), x s set β) :
( (x : α) (H : x s), t x H) = (x : s), t x _
theorem set.bInter_eq_Inter {α : Type u_1} {β : Type u_2} (s : set α) (t : Π (x : α), x s set β) :
( (x : α) (H : x s), t x H) = (x : s), t x _
theorem set.Union_subtype {α : Type u_1} {β : Type u_2} (p : α Prop) (s : {x // p x} set β) :
( (x : {x // p x}), s x) = (x : α) (hx : p x), s x, hx⟩
theorem set.Inter_subtype {α : Type u_1} {β : Type u_2} (p : α Prop) (s : {x // p x} set β) :
( (x : {x // p x}), s x) = (x : α) (hx : p x), s x, hx⟩
theorem set.bInter_empty {α : Type u_1} {β : Type u_2} (u : α set β) :
( (x : α) (H : x ), u x) = set.univ
theorem set.bInter_univ {α : Type u_1} {β : Type u_2} (u : α set β) :
( (x : α) (H : , u x) = (x : α), u x
@[simp]
theorem set.bUnion_self {α : Type u_1} (s : set α) :
( (x : α) (H : x s), s) = s
@[simp]
theorem set.Union_nonempty_self {α : Type u_1} (s : set α) :
( (h : s.nonempty), s) = s
theorem set.bInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α set β) :
( (x : α) (H : x {a}), s x) = s a
theorem set.bInter_union {α : Type u_1} {β : Type u_2} (s t : set α) (u : α set β) :
( (x : α) (H : x s t), u x) = ( (x : α) (H : x s), u x) (x : α) (H : x t), u x
theorem set.bInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : set α) (t : α set β) :
( (x : α) (H : x , t x) = t a (x : α) (H : x s), t x
theorem set.bInter_pair {α : Type u_1} {β : Type u_2} (a b : α) (s : α set β) :
( (x : α) (H : x {a, b}), s x) = s a s b
theorem set.bInter_inter {ι : Type u_1} {α : Type u_2} {s : set ι} (hs : s.nonempty) (f : ι set α) (t : set α) :
( (i : ι) (H : i s), f i t) = ( (i : ι) (H : i s), f i) t
theorem set.inter_bInter {ι : Type u_1} {α : Type u_2} {s : set ι} (hs : s.nonempty) (f : ι set α) (t : set α) :
( (i : ι) (H : i s), t f i) = t (i : ι) (H : i s), f i
theorem set.bUnion_empty {α : Type u_1} {β : Type u_2} (s : α set β) :
( (x : α) (H : x ), s x) =
theorem set.bUnion_univ {α : Type u_1} {β : Type u_2} (s : α set β) :
( (x : α) (H : , s x) = (x : α), s x
theorem set.bUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α set β) :
( (x : α) (H : x {a}), s x) = s a
@[simp]
theorem set.bUnion_of_singleton {α : Type u_1} (s : set α) :
( (x : α) (H : x s), {x}) = s
theorem set.bUnion_union {α : Type u_1} {β : Type u_2} (s t : set α) (u : α set β) :
( (x : α) (H : x s t), u x) = ( (x : α) (H : x s), u x) (x : α) (H : x t), u x
@[simp]
theorem set.Union_coe_set {α : Type u_1} {β : Type u_2} (s : set α) (f : s set β) :
( (i : s), f i) = (i : α) (H : i s), f i, H⟩
@[simp]
theorem set.Inter_coe_set {α : Type u_1} {β : Type u_2} (s : set α) (f : s set β) :
( (i : s), f i) = (i : α) (H : i s), f i, H⟩
theorem set.bUnion_insert {α : Type u_1} {β : Type u_2} (a : α) (s : set α) (t : α set β) :
( (x : α) (H : x , t x) = t a (x : α) (H : x s), t x
theorem set.bUnion_pair {α : Type u_1} {β : Type u_2} (a b : α) (s : α set β) :
( (x : α) (H : x {a, b}), s x) = s a s b
theorem set.inter_Union₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : set α) (t : Π (i : ι), κ i set α) :
(s (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s t i j
theorem set.Union₂_inter {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) (t : set α) :
( (i : ι) (j : κ i), s i j) t = (i : ι) (j : κ i), s i j t
theorem set.union_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : set α) (t : Π (i : ι), κ i set α) :
(s (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s t i j
theorem set.Inter₂_union {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) (t : set α) :
( (i : ι) (j : κ i), s i j) t = (i : ι) (j : κ i), s i j t
theorem set.mem_sUnion_of_mem {α : Type u_1} {x : α} {t : set α} {S : set (set α)} (hx : x t) (ht : t S) :
theorem set.not_mem_of_not_mem_sUnion {α : Type u_1} {x : α} {t : set α} {S : set (set α)} (hx : x ⋃₀ S) (ht : t S) :
x t
theorem set.sInter_subset_of_mem {α : Type u_1} {S : set (set α)} {t : set α} (tS : t S) :
theorem set.subset_sUnion_of_mem {α : Type u_1} {S : set (set α)} {t : set α} (tS : t S) :
theorem set.subset_sUnion_of_subset {α : Type u_1} {s : set α} (t : set (set α)) (u : set α) (h₁ : s u) (h₂ : u t) :
theorem set.sUnion_subset {α : Type u_1} {S : set (set α)} {t : set α} (h : (t' : set α), t' S t' t) :
@[simp]
theorem set.sUnion_subset_iff {α : Type u_1} {s : set (set α)} {t : set α} :
⋃₀ s t (t' : set α), t' s t' t
theorem set.subset_sInter {α : Type u_1} {S : set (set α)} {t : set α} (h : (t' : set α), t' S t t') :
@[simp]
theorem set.subset_sInter_iff {α : Type u_1} {S : set (set α)} {t : set α} :
t ⋂₀ S (t' : set α), t' S t t'
theorem set.sUnion_subset_sUnion {α : Type u_1} {S T : set (set α)} (h : S T) :
theorem set.sInter_subset_sInter {α : Type u_1} {S T : set (set α)} (h : S T) :
@[simp]
theorem set.sUnion_empty {α : Type u_1} :
@[simp]
theorem set.sInter_empty {α : Type u_1} :
@[simp]
theorem set.sUnion_singleton {α : Type u_1} (s : set α) :
⋃₀ {s} = s
@[simp]
theorem set.sInter_singleton {α : Type u_1} (s : set α) :
⋂₀ {s} = s
@[simp]
theorem set.sUnion_eq_empty {α : Type u_1} {S : set (set α)} :
⋃₀ S = (s : set α), s S s =
@[simp]
theorem set.sInter_eq_univ {α : Type u_1} {S : set (set α)} :
(s : set α), s S
@[simp]
theorem set.nonempty_sUnion {α : Type u_1} {S : set (set α)} :
(⋃₀ S).nonempty (s : set α) (H : s S), s.nonempty
theorem set.nonempty.of_sUnion {α : Type u_1} {s : set (set α)} (h : (⋃₀ s).nonempty) :
theorem set.nonempty.of_sUnion_eq_univ {α : Type u_1} [nonempty α] {s : set (set α)} (h : ⋃₀ s = set.univ) :
theorem set.sUnion_union {α : Type u_1} (S T : set (set α)) :
theorem set.sInter_union {α : Type u_1} (S T : set (set α)) :
@[simp]
theorem set.sUnion_insert {α : Type u_1} (s : set α) (T : set (set α)) :
= s ⋃₀ T
@[simp]
theorem set.sInter_insert {α : Type u_1} (s : set α) (T : set (set α)) :
= s ⋂₀ T
@[simp]
theorem set.sUnion_diff_singleton_empty {α : Type u_1} (s : set (set α)) :
⋃₀ (s \ {}) = ⋃₀ s
@[simp]
theorem set.sInter_diff_singleton_univ {α : Type u_1} (s : set (set α)) :
theorem set.sUnion_pair {α : Type u_1} (s t : set α) :
⋃₀ {s, t} = s t
theorem set.sInter_pair {α : Type u_1} (s t : set α) :
⋂₀ {s, t} = s t
@[simp]
theorem set.sUnion_image {α : Type u_1} {β : Type u_2} (f : α set β) (s : set α) :
⋃₀ (f '' s) = (x : α) (H : x s), f x
@[simp]
theorem set.sInter_image {α : Type u_1} {β : Type u_2} (f : α set β) (s : set α) :
⋂₀ (f '' s) = (x : α) (H : x s), f x
@[simp]
theorem set.sUnion_range {β : Type u_2} {ι : Sort u_4} (f : ι set β) :
= (x : ι), f x
@[simp]
theorem set.sInter_range {β : Type u_2} {ι : Sort u_4} (f : ι set β) :
= (x : ι), f x
theorem set.Union_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {f : ι set α} :
( (i : ι), f i) = set.univ (x : α), (i : ι), x f i
theorem set.Union₂_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} :
( (i : ι) (j : κ i), s i j) = set.univ (a : α), (i : ι) (j : κ i), a s i j
theorem set.sUnion_eq_univ_iff {α : Type u_1} {c : set (set α)} :
(a : α), (b : set α) (H : b c), a b
theorem set.Inter_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι set α} :
( (i : ι), f i) = (x : α), (i : ι), x f i
theorem set.Inter₂_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} :
( (i : ι) (j : κ i), s i j) = (a : α), (i : ι) (j : κ i), a s i j
theorem set.sInter_eq_empty_iff {α : Type u_1} {c : set (set α)} :
⋂₀ c = (a : α), (b : set α) (H : b c), a b
@[simp]
theorem set.nonempty_Inter {α : Type u_1} {ι : Sort u_4} {f : ι set α} :
( (i : ι), f i).nonempty (x : α), (i : ι), x f i
@[simp]
theorem set.nonempty_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} :
( (i : ι) (j : κ i), s i j).nonempty (a : α), (i : ι) (j : κ i), a s i j
@[simp]
theorem set.nonempty_sInter {α : Type u_1} {c : set (set α)} :
(⋂₀ c).nonempty (a : α), (b : set α), b c a b
theorem set.compl_sUnion {α : Type u_1} (S : set (set α)) :
theorem set.sUnion_eq_compl_sInter_compl {α : Type u_1} (S : set (set α)) :
theorem set.compl_sInter {α : Type u_1} (S : set (set α)) :
theorem set.sInter_eq_compl_sUnion_compl {α : Type u_1} (S : set (set α)) :
theorem set.inter_empty_of_inter_sUnion_empty {α : Type u_1} {s t : set α} {S : set (set α)} (hs : t S) (h : s ⋃₀ S = ) :
s t =
theorem set.range_sigma_eq_Union_range {α : Type u_1} {β : Type u_2} {γ : α Type u_3} (f : β) :
= (a : α), set.range (λ (b : γ a), f a, b⟩)
theorem set.Union_eq_range_sigma {α : Type u_1} {β : Type u_2} (s : α set β) :
( (i : α), s i) = set.range (λ (a : Σ (i : α), (s i)), (a.snd))
theorem set.Union_eq_range_psigma {β : Type u_2} {ι : Sort u_4} (s : ι set β) :
( (i : ι), s i) = set.range (λ (a : Σ' (i : ι), (s i)), (a.snd))
theorem set.Union_image_preimage_sigma_mk_eq_self {ι : Type u_1} {σ : ι Type u_2} (s : set (sigma σ)) :
( (i : ι), '' (sigma.mk i ⁻¹' s)) = s
theorem set.sigma.univ {α : Type u_1} (X : α Type u_2) :
set.univ = (a : α),
theorem set.sUnion_mono {α : Type u_1} {s t : set (set α)} (h : s t) :
theorem set.Union_subset_Union_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : set α} (h : ι ι₂) :
( (i : ι), s) (j : ι₂), s
@[simp]
theorem set.Union_singleton_eq_range {α : Type u_1} {β : Type u_2} (f : α β) :
( (x : α), {f x}) =
theorem set.Union_of_singleton (α : Type u_1) :
( (x : α), {x}) = set.univ
theorem set.Union_of_singleton_coe {α : Type u_1} (s : set α) :
( (i : s), {i}) = s
theorem set.sUnion_eq_bUnion {α : Type u_1} {s : set (set α)} :
⋃₀ s = (i : set α) (h : i s), i
theorem set.sInter_eq_bInter {α : Type u_1} {s : set (set α)} :
⋂₀ s = (i : set α) (h : i s), i
theorem set.sUnion_eq_Union {α : Type u_1} {s : set (set α)} :
⋃₀ s = (i : s), i
theorem set.sInter_eq_Inter {α : Type u_1} {s : set (set α)} :
⋂₀ s = (i : s), i
@[simp]
theorem set.Union_of_empty {α : Type u_1} {ι : Sort u_4} [is_empty ι] (s : ι set α) :
( (i : ι), s i) =
@[simp]
theorem set.Inter_of_empty {α : Type u_1} {ι : Sort u_4} [is_empty ι] (s : ι set α) :
( (i : ι), s i) = set.univ
theorem set.union_eq_Union {α : Type u_1} {s₁ s₂ : set α} :
s₁ s₂ = (b : bool), cond b s₁ s₂
theorem set.inter_eq_Inter {α : Type u_1} {s₁ s₂ : set α} :
s₁ s₂ = (b : bool), cond b s₁ s₂
theorem set.sInter_union_sInter {α : Type u_1} {S T : set (set α)} :
⋂₀ S ⋂₀ T = (p : set α × set α) (H : p S ×ˢ T), p.fst p.snd
theorem set.sUnion_inter_sUnion {α : Type u_1} {s t : set (set α)} :
⋃₀ s ⋃₀ t = (p : set α × set α) (H : p s ×ˢ t), p.fst p.snd
theorem set.bUnion_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι set α) (t : α set β) :
( (x : α) (H : x (i : ι), s i), t x) = (i : ι) (x : α) (H : x s i), t x
theorem set.bInter_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι set α) (t : α set β) :
( (x : α) (H : x (i : ι), s i), t x) = (i : ι) (x : α) (H : x s i), t x
theorem set.sUnion_Union {α : Type u_1} {ι : Sort u_4} (s : ι set (set α)) :
(⋃₀ (i : ι), s i) = (i : ι), ⋃₀ s i
theorem set.sInter_Union {α : Type u_1} {ι : Sort u_4} (s : ι set (set α)) :
(⋂₀ (i : ι), s i) = (i : ι), ⋂₀ s i
theorem set.Union_range_eq_sUnion {α : Type u_1} {β : Type u_2} (C : set (set α)) {f : Π (s : C), β s} (hf : (s : C), function.surjective (f s)) :
( (y : β), set.range (λ (s : C), (f s y).val)) = ⋃₀ C
theorem set.Union_range_eq_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (C : ι set α) {f : Π (x : ι), β (C x)} (hf : (x : ι), function.surjective (f x)) :
( (y : β), set.range (λ (x : ι), (f x y).val)) = (x : ι), C x
theorem set.union_distrib_Inter_left {α : Type u_1} {ι : Sort u_4} (s : ι set α) (t : set α) :
(t (i : ι), s i) = (i : ι), t s i
theorem set.union_distrib_Inter₂_left {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : set α) (t : Π (i : ι), κ i set α) :
(s (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s t i j
theorem set.union_distrib_Inter_right {α : Type u_1} {ι : Sort u_4} (s : ι set α) (t : set α) :
( (i : ι), s i) t = (i : ι), s i t
theorem set.union_distrib_Inter₂_right {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) (t : set α) :
( (i : ι) (j : κ i), s i j) t = (i : ι) (j : κ i), s i j t

### `maps_to`#

theorem set.maps_to_sUnion {α : Type u_1} {β : Type u_2} {S : set (set α)} {t : set β} {f : α β} (H : (s : set α), s S s t) :
(⋃₀ S) t
theorem set.maps_to_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : set β} {f : α β} (H : (i : ι), (s i) t) :
( (i : ι), s i) t
theorem set.maps_to_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : set β} {f : α β} (H : (i : ι) (j : κ i), (s i j) t) :
( (i : ι) (j : κ i), s i j) t
theorem set.maps_to_Union_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.maps_to_Union₂_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : Π (i : ι), κ i set β} {f : α β} (H : (i : ι) (j : κ i), (s i j) (t i j)) :
( (i : ι) (j : κ i), s i j) ( (i : ι) (j : κ i), t i j)
theorem set.maps_to_sInter {α : Type u_1} {β : Type u_2} {s : set α} {T : set (set β)} {f : α β} (H : (t : set β), t T s t) :
s (⋂₀ T)
theorem set.maps_to_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : set α} {t : ι set β} {f : α β} (H : (i : ι), s (t i)) :
s ( (i : ι), t i)
theorem set.maps_to_Inter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set β} {f : α β} (H : (i : ι) (j : κ i), s (t i j)) :
s ( (i : ι) (j : κ i), t i j)
theorem set.maps_to_Inter_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.maps_to_Inter₂_Inter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : Π (i : ι), κ i set β} {f : α β} (H : (i : ι) (j : κ i), (s i j) (t i j)) :
( (i : ι) (j : κ i), s i j) ( (i : ι) (j : κ i), t i j)
theorem set.image_Inter_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι set α) (f : α β) :
(f '' (i : ι), s i) (i : ι), f '' s i
theorem set.image_Inter₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} (s : Π (i : ι), κ i set α) (f : α β) :
(f '' (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), f '' s i j
theorem set.image_sInter_subset {α : Type u_1} {β : Type u_2} (S : set (set α)) (f : α β) :
f '' ⋂₀ S (s : set α) (H : s S), f '' s

### `restrict_preimage`#

theorem set.injective_iff_injective_of_Union_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {U : ι set β} (hU : = set.univ) :
theorem set.surjective_iff_surjective_of_Union_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {U : ι set β} (hU : = set.univ) :
theorem set.bijective_iff_bijective_of_Union_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {U : ι set β} (hU : = set.univ) :

### `inj_on`#

theorem set.inj_on.image_Inter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {s : ι set α} {f : α β} (h : ( (i : ι), s i)) :
(f '' (i : ι), s i) = (i : ι), f '' s i
theorem set.inj_on.image_bInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {p : ι Prop} {s : Π (i : ι), p i set α} (hp : (i : ι), p i) {f : α β} (h : ( (i : ι) (hi : p i), s i hi)) :
(f '' (i : ι) (hi : p i), s i hi) = (i : ι) (hi : p i), f '' s i hi
theorem set.image_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} (hf : function.bijective f) (s : ι set α) :
(f '' (i : ι), s i) = (i : ι), f '' s i
theorem set.image_Inter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {f : α β} (hf : function.bijective f) (s : Π (i : ι), κ i set α) :
(f '' (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), f '' s i j
theorem set.inj_on_Union_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} (hs : s) {f : α β} (hf : (i : ι), (s i)) :
( (i : ι), s i)

### `surj_on`#

theorem set.surj_on_sUnion {α : Type u_1} {β : Type u_2} {s : set α} {T : set (set β)} {f : α β} (H : (t : set β), t T s t) :
s (⋃₀ T)
theorem set.surj_on_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : set α} {t : ι set β} {f : α β} (H : (i : ι), s (t i)) :
s ( (i : ι), t i)
theorem set.surj_on_Union_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.surj_on_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set β} {f : α β} (H : (i : ι) (j : κ i), s (t i j)) :
s ( (i : ι) (j : κ i), t i j)
theorem set.surj_on_Union₂_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : Π (i : ι), κ i set β} {f : α β} (H : (i : ι) (j : κ i), (s i j) (t i j)) :
( (i : ι) (j : κ i), s i j) ( (i : ι) (j : κ i), t i j)
theorem set.surj_on_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι set α} {t : set β} {f : α β} (H : (i : ι), (s i) t) (Hinj : ( (i : ι), s i)) :
( (i : ι), s i) t
theorem set.surj_on_Inter_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) (Hinj : ( (i : ι), s i)) :
( (i : ι), s i) ( (i : ι), t i)

### `bij_on`#

theorem set.bij_on_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) (Hinj : ( (i : ι), s i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.bij_on_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι set α} {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) (Hinj : ( (i : ι), s i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.bij_on_Union_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} (hs : s) {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) :
( (i : ι), s i) ( (i : ι), t i)
theorem set.bij_on_Inter_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {s : ι set α} (hs : s) {t : ι set β} {f : α β} (H : (i : ι), (s i) (t i)) :
( (i : ι), s i) ( (i : ι), t i)

### `image`, `preimage`#

theorem set.image_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {s : ι set α} :
(f '' (i : ι), s i) = (i : ι), f '' s i
theorem set.image_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} (f : α β) (s : Π (i : ι), κ i set α) :
(f '' (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), f '' s i j
theorem set.univ_subtype {α : Type u_1} {p : α Prop} :
set.univ = (x : α) (h : p x), {x, h⟩}
theorem set.range_eq_Union {α : Type u_1} {ι : Sort u_2} (f : ι α) :
= (i : ι), {f i}
theorem set.image_eq_Union {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
f '' s = (i : α) (H : i s), {f i}
theorem set.bUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι α} {g : α set β} :
( (x : α) (H : x , g x) = (y : ι), g (f y)
@[simp]
theorem set.Union_Union_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι α} {g : α set β} :
( (x : α) (y : ι) (h : f y = x), g x) = (y : ι), g (f y)
theorem set.bInter_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι α} {g : α set β} :
( (x : α) (H : x , g x) = (y : ι), g (f y)
@[simp]
theorem set.Inter_Inter_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι α} {g : α set β} :
( (x : α) (y : ι) (h : f y = x), g x) = (y : ι), g (f y)
theorem set.bUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set γ} {f : γ α} {g : α set β} :
( (x : α) (H : x f '' s), g x) = (y : γ) (H : y s), g (f y)
theorem set.bInter_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set γ} {f : γ α} {g : α set β} :
( (x : α) (H : x f '' s), g x) = (y : γ) (H : y s), g (f y)
theorem set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : α β} :
@[simp]
theorem set.preimage_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {s : ι set β} :
(f ⁻¹' (i : ι), s i) = (i : ι), f ⁻¹' s i
theorem set.preimage_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {f : α β} {s : Π (i : ι), κ i set β} :
(f ⁻¹' (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), f ⁻¹' s i j
@[simp]
theorem set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : α β} {s : set (set β)} :
f ⁻¹' ⋃₀ s = (t : set β) (H : t s), f ⁻¹' t
theorem set.preimage_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α β} {s : ι set β} :
(f ⁻¹' (i : ι), s i) = (i : ι), f ⁻¹' s i
theorem set.preimage_Inter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {f : α β} {s : Π (i : ι), κ i set β} :
(f ⁻¹' (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), f ⁻¹' s i j
@[simp]
theorem set.preimage_sInter {α : Type u_1} {β : Type u_2} {f : α β} {s : set (set β)} :
f ⁻¹' ⋂₀ s = (t : set β) (H : t s), f ⁻¹' t
@[simp]
theorem set.bUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α β) (s : set β) :
( (y : β) (H : y s), f ⁻¹' {y}) = f ⁻¹' s
theorem set.bUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α β) :
( (y : β) (H : y , f ⁻¹' {y}) = set.univ
theorem set.prod_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : set α} {t : ι set β} :
(s ×ˢ (i : ι), t i) = (i : ι), s ×ˢ t i
theorem set.prod_Union₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : set α} {t : Π (i : ι), κ i set β} :
(s ×ˢ (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s ×ˢ t i j
theorem set.prod_sUnion {α : Type u_1} {β : Type u_2} {s : set α} {C : set (set β)} :
s ×ˢ ⋃₀ C = ⋃₀ ((λ (t : set β), s ×ˢ t) '' C)
theorem set.Union_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι set α} {t : set β} :
( (i : ι), s i) ×ˢ t = (i : ι), s i ×ˢ t
theorem set.Union₂_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι Sort u_7} {s : Π (i : ι), κ i set α} {t : set β} :
( (i : ι) (j : κ i), s i j) ×ˢ t = (i : ι) (j : κ i), s i j ×ˢ t
theorem set.sUnion_prod_const {α : Type u_1} {β : Type u_2} {C : set (set α)} {t : set β} :
⋃₀ C ×ˢ t = ⋃₀ ((λ (s : set α), s ×ˢ t) '' C)
theorem set.Union_prod {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} (s : ι set α) (t : ι' set β) :
( (x : ι × ι'), s x.fst ×ˢ t x.snd) = ( (i : ι), s i) ×ˢ (i : ι'), t i
theorem set.Union_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α set β} {t : α set γ} (hs : monotone s) (ht : monotone t) :
( (x : α), s x ×ˢ t x) = ( (x : α), s x) ×ˢ (x : α), t x
theorem set.sInter_prod_sInter_subset {α : Type u_1} {β : Type u_2} (S : set (set α)) (T : set (set β)) :
⋂₀ S ×ˢ ⋂₀ T (r : set α × set β) (H : r S ×ˢ T), r.fst ×ˢ r.snd
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 : set α × set β) (H : r S ×ˢ T), r.fst ×ˢ r.snd
theorem set.sInter_prod {α : Type u_1} {β : Type u_2} {S : set (set α)} (hS : S.nonempty) (t : set β) :
⋂₀ S ×ˢ t = (s : set α) (H : s S), s ×ˢ t
theorem set.prod_sInter {α : Type u_1} {β : Type u_2} {T : set (set β)} (hT : T.nonempty) (s : set α) :
s ×ˢ ⋂₀ T = (t : set β) (H : t T), s ×ˢ t
theorem set.Union_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) {s : set α} {t : set β} :
( (a : α) (H : a s), f a '' t) = s t
theorem set.Union_image_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) {s : set α} {t : set β} :
( (b : β) (H : b t), (λ (a : α), f a b) '' s) = s t
theorem set.image2_Union_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α β γ) (s : ι set α) (t : set β) :
( (i : ι), s i) t = (i : ι), (s i) t
theorem set.image2_Union_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α β γ) (s : set α) (t : ι set β) :
s ( (i : ι), t i) = (i : ι), s (t i)
theorem set.image2_Union₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} (f : α β γ) (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) t = (i : ι) (j : κ i), (s i j) t
theorem set.image2_Union₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} (f : α β γ) (s : set α) (t : Π (i : ι), κ i set β) :
s ( (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s (t i j)
theorem set.image2_Inter_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α β γ) (s : ι set α) (t : set β) :
( (i : ι), s i) t (i : ι), (s i) t
theorem set.image2_Inter_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α β γ) (s : set α) (t : ι set β) :
s ( (i : ι), t i) (i : ι), s (t i)
theorem set.image2_Inter₂_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} (f : α β γ) (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) t (i : ι) (j : κ i), (s i j) t
theorem set.image2_Inter₂_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι Sort u_7} (f : α β γ) (s : set α) (t : Π (i : ι), κ i set β) :
s ( (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), s (t i j)
theorem set.image2_eq_Union {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (s : set α) (t : set β) :
s t = (i : α) (H : i s) (j : β) (H : j t), {f i j}

The `set.image2` version of `set.image_eq_Union`

theorem set.prod_eq_bUnion_left {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s ×ˢ t = (a : α) (H : a s), (λ (b : β), (a, b)) '' t
theorem set.prod_eq_bUnion_right {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s ×ˢ t = (b : β) (H : b t), (λ (a : α), (a, b)) '' s
def set.seq {α : Type u_1} {β : Type u_2} (s : set β)) (t : set α) :
set β

Given a set `s` of functions `α → β` and `t : set α`, `seq s t` is the union of `f '' t` over all `f ∈ s`.

Equations
Instances for `↥set.seq`
theorem set.seq_def {α : Type u_1} {β : Type u_2} {s : set β)} {t : set α} :
s.seq t = (f : α β) (H : f s), f '' t
@[simp]
theorem set.mem_seq_iff {α : Type u_1} {β : Type u_2} {s : set β)} {t : set α} {b : β} :
b s.seq t (f : α β) (H : f s) (a : α) (H : a t), f a = b
theorem set.seq_subset {α : Type u_1} {β : Type u_2} {s : set β)} {t : set α} {u : set β} :
s.seq t u (f : α β), f s (a : α), a t f a u
theorem set.seq_mono {α : Type u_1} {β : Type u_2} {s₀ s₁ : set β)} {t₀ t₁ : set α} (hs : s₀ s₁) (ht : t₀ t₁) :
s₀.seq t₀ s₁.seq t₁
theorem set.singleton_seq {α : Type u_1} {β : Type u_2} {f : α β} {t : set α} :
{f}.seq t = f '' t
theorem set.seq_singleton {α : Type u_1} {β : Type u_2} {s : set β)} {a : α} :
s.seq {a} = (λ (f : α β), f a) '' s
theorem set.seq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set γ)} {t : set β)} {u : set α} :
s.seq (t.seq u) = ((function.comp '' s).seq t).seq u
theorem set.image_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β γ} {s : set β)} {t : set α} :
f '' s.seq t = '' s).seq t
theorem set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s ×ˢ t = (prod.mk '' s).seq t
theorem set.prod_image_seq_comm {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
(prod.mk '' s).seq t = ((λ (b : β) (a : α), (a, b)) '' t).seq s
theorem set.image2_eq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (s : set α) (t : set β) :
s t = (f '' s).seq t
theorem set.pi_def {α : Type u_1} {π : α Type u_11} (i : set α) (s : Π (a : α), set (π a)) :
i.pi s = (a : α) (H : a i), ⁻¹' s a
theorem set.univ_pi_eq_Inter {α : Type u_1} {π : α Type u_11} (t : Π (i : α), set (π i)) :
= (i : α), ⁻¹' t i
theorem set.pi_diff_pi_subset {α : Type u_1} {π : α Type u_11} (i : set α) (s t : Π (a : α), set (π a)) :
i.pi s \ i.pi t (a : α) (H : a i), ⁻¹' (s a \ t a)
theorem set.Union_univ_pi {α : Type u_1} {ι : Sort u_4} {π : α Type u_11} (t : Π (i : α), ι set (π i)) :
( (x : α ι), set.univ.pi (λ (i : α), t i (x i))) = set.univ.pi (λ (i : α), (j : ι), t i j)
theorem function.surjective.Union_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι ι₂} (hf : function.surjective f) (g : ι₂ set α) :
( (x : ι), g (f x)) = (y : ι₂), g y
theorem function.surjective.Inter_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι ι₂} (hf : function.surjective f) (g : ι₂ set α) :
( (x : ι), g (f x)) = (y : ι₂), g y

### Disjoint sets #

We define some lemmas in the `disjoint` namespace to be able to use projection notation.

@[simp]
theorem set.disjoint_Union_left {α : Type u_1} {t : set α} {ι : Sort u_2} {s : ι