mathlib documentation

data.set.lattice

@[instance]
def set.lattice_set {α : Type u} :

Equations
theorem set.monotone_image {α : Type u} {β : Type v} {f : α → β} :

Image is monotone. See set.image_image for the statement in terms of .

theorem set.monotone_inter {α : Type u} {β : Type v} [preorder β] {f g : β → set α} :
monotone fmonotone gmonotone (λ (x : β), f x g x)

theorem set.monotone_union {α : Type u} {β : Type v} [preorder β] {f g : β → set α} :
monotone fmonotone gmonotone (λ (x : β), f x g x)

theorem set.monotone_set_of {α : Type u} {β : Type v} [preorder α] {p : α → β → Prop} :
(∀ (b : β), monotone (λ (a : α), p a b))monotone (λ (a : α), {b : β | p a b})

theorem set.image_preimage {α : Type u} {β : Type v} {f : α → β} :

def set.kern_image {α : Type u} {β : Type v} :
(α → β)set αset β

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

Equations
theorem set.preimage_kern_image {α : Type u} {β : Type v} {f : α → β} :

def set.Union {β : Type v} {ι : Sort x} :
(ι → set β)set β

Indexed union of a family of sets

Equations
def set.Inter {β : Type v} {ι : Sort x} :
(ι → set β)set β

Indexed intersection of a family of sets

Equations
@[simp]
theorem set.mem_Union {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :
x set.Union s ∃ (i : ι), x s i

theorem set.set_of_exists {β : Type v} {ι : Sort x} (p : ι → β → Prop) :
{x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}

@[simp]
theorem set.mem_Inter {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :
x set.Inter s ∀ (i : ι), x s i

theorem set.set_of_forall {β : Type v} {ι : Sort x} (p : ι → β → Prop) :
{x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}

theorem set.Union_subset {β : Type v} {ι : Sort x} {s : ι → set β} {t : set β} :
(∀ (i : ι), s i t)(⋃ (i : ι), s i) t

theorem set.Union_subset_iff {β : Type v} {ι : Sort x} {s : ι → set β} {t : set β} :
(⋃ (i : ι), s i) t ∀ (i : ι), s i t

theorem set.mem_Inter_of_mem {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :
(∀ (i : ι), x s i)(x ⋂ (i : ι), s i)

theorem set.subset_Inter {β : Type v} {ι : Sort x} {t : set β} {s : ι → set β} :
(∀ (i : ι), t s i)(t ⋂ (i : ι), s i)

theorem set.subset_Inter_iff {β : Type v} {ι : Sort x} {t : set β} {s : ι → set β} :
(t ⋂ (i : ι), s i) ∀ (i : ι), t s i

theorem set.subset_Union {β : Type v} {ι : Sort x} (s : ι → set β) (i : ι) :
s i ⋃ (i : ι), s i

theorem set.subset_subset_Union {β : Type v} {ι : Sort x} {A : set β} {s : ι → set β} (i : ι) :
A s i(A ⋃ (i : ι), s i)

theorem set.Inter_subset {β : Type v} {ι : Sort x} (s : ι → set β) (i : ι) :
(⋂ (i : ι), s i) s i

theorem set.Inter_subset_of_subset {α : Type u} {ι : Sort x} {s : ι → set α} {t : set α} (i : ι) :
s i t(⋂ (i : ι), s i) t

theorem set.Inter_subset_Inter {α : Type u} {ι : Sort x} {s t : ι → set α} :
(∀ (i : ι), s i t i)((⋂ (i : ι), s i) ⋂ (i : ι), t i)

theorem set.Inter_subset_Inter2 {α : Type u} {ι : Sort x} {ι' : Sort y} {s : ι → set α} {t : ι' → set α} :
(∀ (j : ι'), ∃ (i : ι), s i t j)((⋂ (i : ι), s i) ⋂ (j : ι'), t j)

theorem set.Inter_set_of {α : Type u} {ι : Sort x} (P : ι → α → Prop) :
(⋂ (i : ι), {x : α | P i x}) = {x : α | ∀ (i : ι), P i x}

theorem set.Union_const {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) :
(⋃ (i : ι), s) = s

theorem set.Inter_const {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) :
(⋂ (i : ι), s) = s

@[simp]
theorem set.compl_Union {β : Type v} {ι : Sort x} (s : ι → set β) :
(⋃ (i : ι), s i) = ⋂ (i : ι), (s i)

theorem set.compl_Inter {β : Type v} {ι : Sort x} (s : ι → set β) :
(⋂ (i : ι), s i) = ⋃ (i : ι), (s i)

theorem set.Union_eq_comp_Inter_comp {β : Type v} {ι : Sort x} (s : ι → set β) :
(⋃ (i : ι), s i) = (⋂ (i : ι), (s i))

theorem set.Inter_eq_comp_Union_comp {β : Type v} {ι : Sort x} (s : ι → set β) :
(⋂ (i : ι), s i) = (⋃ (i : ι), (s i))

theorem set.inter_Union {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :
(s ⋃ (i : ι), t i) = ⋃ (i : ι), s t i

theorem set.Union_inter {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) s = ⋃ (i : ι), t i s

theorem set.Union_union_distrib {β : Type v} {ι : Sort x} (s t : ι → set β) :
(⋃ (i : ι), s i t i) = (⋃ (i : ι), s i) ⋃ (i : ι), t i

theorem set.Inter_inter_distrib {β : Type v} {ι : Sort x} (s t : ι → set β) :
(⋂ (i : ι), s i t i) = (⋂ (i : ι), s i) ⋂ (i : ι), t i

theorem set.union_Union {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :
(s ⋃ (i : ι), t i) = ⋃ (i : ι), s t i

theorem set.Union_union {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) s = ⋃ (i : ι), t i s

theorem set.inter_Inter {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :
(s ⋂ (i : ι), t i) = ⋂ (i : ι), s t i

theorem set.Inter_inter {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :
(⋂ (i : ι), t i) s = ⋂ (i : ι), t i s

theorem set.union_Inter {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :
(s ⋂ (i : ι), t i) = ⋂ (i : ι), s t i

theorem set.Union_diff {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s

theorem set.diff_Union {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :
(s \ ⋃ (i : ι), t i) = ⋂ (i : ι), s \ t i

theorem set.diff_Inter {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :
(s \ ⋂ (i : ι), t i) = ⋃ (i : ι), s \ t i

theorem set.directed_on_Union {α : Type u} {r : α → α → Prop} {ι : Sort v} {f : ι → set α} :
directed has_subset.subset f(∀ (x : ι), directed_on r (f x))directed_on r (⋃ (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} [semilattice_sup ι] {s t : ι → set α} :
monotone smonotone t((⋃ (i : ι), s i t i) = (⋃ (i : ι), s i) ⋃ (i : ι), t i)

theorem set.Union_Inter_subset {ι : Sort u_1} {ι' : Sort u_2} {α : Type u_3} {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.mem_bUnion_iff {α : Type u} {β : Type v} {s : set α} {t : α → set β} {y : β} :
(y ⋃ (x : α) (H : x s), t x) ∃ (x : α) (H : x s), y t x

theorem set.mem_bInter_iff {α : Type u} {β : Type v} {s : set α} {t : α → set β} {y : β} :
(y ⋂ (x : α) (H : x s), t x) ∀ (x : α), x sy t x

theorem set.mem_bUnion {α : Type u} {β : Type v} {s : set α} {t : α → set β} {x : α} {y : β} :
x sy t x(y ⋃ (x : α) (H : x s), t x)

theorem set.mem_bInter {α : Type u} {β : Type v} {s : set α} {t : α → set β} {y : β} :
(∀ (x : α), x sy t x)(y ⋂ (x : α) (H : x s), t x)

theorem set.bUnion_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {u : α → set β} :
(∀ (x : α), x su x t)(⋃ (x : α) (H : x s), u x) t

theorem set.subset_bInter {α : Type u} {β : Type v} {s : set α} {t : set β} {u : α → set β} :
(∀ (x : α), x st u x)(t ⋂ (x : α) (H : x s), u x)

theorem set.subset_bUnion_of_mem {α : Type u} {β : Type v} {s : set α} {u : α → set β} {x : α} :
x s(u x ⋃ (x : α) (H : x s), u x)

theorem set.bInter_subset_of_mem {α : Type u} {β : Type v} {s : set α} {t : α → set β} {x : α} :
x s(⋂ (x : α) (H : x s), t x) t x

theorem set.bUnion_subset_bUnion_left {α : Type u} {β : Type v} {s s' : set α} {t : α → set β} :
s s'((⋃ (x : α) (H : x s), t x) ⋃ (x : α) (H : x s'), t x)

theorem set.bInter_subset_bInter_left {α : Type u} {β : Type v} {s s' : set α} {t : α → set β} :
s' s((⋂ (x : α) (H : x s), t x) ⋂ (x : α) (H : x s'), t x)

theorem set.bUnion_subset_bUnion_right {α : Type u} {β : Type v} {s : set α} {t1 t2 : α → set β} :
(∀ (x : α), x st1 x t2 x)((⋃ (x : α) (H : x s), t1 x) ⋃ (x : α) (H : x s), t2 x)

theorem set.bInter_subset_bInter_right {α : Type u} {β : Type v} {s : set α} {t1 t2 : α → set β} :
(∀ (x : α), x st1 x t2 x)((⋂ (x : α) (H : x s), t1 x) ⋂ (x : α) (H : x s), t2 x)

theorem set.bUnion_subset_bUnion {α : Type u} {β : Type v} {γ : Type u_1} {s : set α} {t : α → set β} {s' : set γ} {t' : γ → set β} :
(∀ (x : α), x s(∃ (y : γ) (H : y s'), t x t' y))((⋃ (x : α) (H : x s), t x) ⋃ (y : γ) (H : y s'), t' y)

theorem set.bInter_mono' {α : Type u} {β : Type v} {s s' : set α} {t t' : α → set β} :
s s'(∀ (x : α), x st x t' x)((⋂ (x : α) (H : x s'), t x) ⋂ (x : α) (H : x s), t' x)

theorem set.bInter_mono {α : Type u} {β : Type v} {s : set α} {t t' : α → set β} :
(∀ (x : α), x st x t' x)((⋂ (x : α) (H : x s), t x) ⋂ (x : α) (H : x s), t' x)

theorem set.bUnion_mono {α : Type u} {β : Type v} {s : set α} {t t' : α → set β} :
(∀ (x : α), x st x t' x)((⋃ (x : α) (H : x s), t x) ⋃ (x : α) (H : x s), t' x)

theorem set.bUnion_eq_Union {α : Type u} {β : Type v} (s : set α) (t : Π (x : α), x sset β) :
(⋃ (x : α) (H : x s), t x H) = ⋃ (x : s), t x _

theorem set.bInter_eq_Inter {α : Type u} {β : Type v} (s : set α) (t : Π (x : α), x sset β) :
(⋂ (x : α) (H : x s), t x H) = ⋂ (x : s), t x _

theorem set.bInter_empty {α : Type u} {β : Type v} (u : α → set β) :
(⋂ (x : α) (H : x ), u x) = set.univ

theorem set.bInter_univ {α : Type u} {β : Type v} (u : α → set β) :
(⋂ (x : α) (H : x set.univ), u x) = ⋂ (x : α), u x

@[simp]
theorem set.bInter_singleton {α : Type u} {β : Type v} (a : α) (s : α → set β) :
(⋂ (x : α) (H : x {a}), s x) = s a

theorem set.bInter_union {α : Type u} {β : Type v} (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.bInter_insert {α : Type u} {β : Type v} (a : α) (s : set α) (t : α → set β) :
(⋂ (x : α) (H : x insert a s), t x) = t a ⋂ (x : α) (H : x s), t x

theorem set.bInter_pair {α : Type u} {β : Type v} (a b : α) (s : α → set β) :
(⋂ (x : α) (H : x {a, b}), s x) = s a s b

theorem set.bUnion_empty {α : Type u} {β : Type v} (s : α → set β) :
(⋃ (x : α) (H : x ), s x) =

theorem set.bUnion_univ {α : Type u} {β : Type v} (s : α → set β) :
(⋃ (x : α) (H : x set.univ), s x) = ⋃ (x : α), s x

@[simp]
theorem set.bUnion_singleton {α : Type u} {β : Type v} (a : α) (s : α → set β) :
(⋃ (x : α) (H : x {a}), s x) = s a

@[simp]
theorem set.bUnion_of_singleton {α : Type u} (s : set α) :
(⋃ (x : α) (H : x s), {x}) = s

theorem set.bUnion_union {α : Type u} {β : Type v} (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.bUnion_insert {α : Type u} {β : Type v} (a : α) (s : set α) (t : α → set β) :
(⋃ (x : α) (H : x insert a s), t x) = t a ⋃ (x : α) (H : x s), t x

theorem set.bUnion_pair {α : Type u} {β : Type v} (a b : α) (s : α → set β) :
(⋃ (x : α) (H : x {a, b}), s x) = s a s b

@[simp]
theorem set.compl_bUnion {α : Type u} {β : Type v} (s : set α) (t : α → set β) :
(⋃ (i : α) (H : i s), t i) = ⋂ (i : α) (H : i s), (t i)

theorem set.compl_bInter {α : Type u} {β : Type v} (s : set α) (t : α → set β) :
(⋂ (i : α) (H : i s), t i) = ⋃ (i : α) (H : i s), (t i)

theorem set.inter_bUnion {α : Type u} {β : Type v} (s : set α) (t : α → set β) (u : set β) :
(u ⋃ (i : α) (H : i s), t i) = ⋃ (i : α) (H : i s), u t i

theorem set.bUnion_inter {α : Type u} {β : Type v} (s : set α) (t : α → set β) (u : set β) :
(⋃ (i : α) (H : i s), t i) u = ⋃ (i : α) (H : i s), t i u

def set.sInter {α : Type u} :
set (set α)set α

Intersection of a set of sets.

Equations
theorem set.mem_sUnion_of_mem {α : Type u} {x : α} {t : set α} {S : set (set α)} :
x tt Sx ⋃₀S

theorem set.mem_sUnion {α : Type u} {x : α} {S : set (set α)} :
x ⋃₀S ∃ (t : set α) (H : t S), x t

theorem set.not_mem_of_not_mem_sUnion {α : Type u} {x : α} {t : set α} {S : set (set α)} :
x ⋃₀St Sx t

@[simp]
theorem set.mem_sInter {α : Type u} {x : α} {S : set (set α)} :
x ⋂₀S ∀ (t : set α), t Sx t

theorem set.sInter_subset_of_mem {α : Type u} {S : set (set α)} {t : set α} :
t S⋂₀S t

theorem set.subset_sUnion_of_mem {α : Type u} {S : set (set α)} {t : set α} :
t St ⋃₀S

theorem set.subset_sUnion_of_subset {α : Type u} {s : set α} (t : set (set α)) (u : set α) :
s uu ts ⋃₀t

theorem set.sUnion_subset {α : Type u} {S : set (set α)} {t : set α} :
(∀ (t' : set α), t' St' t)⋃₀S t

theorem set.sUnion_subset_iff {α : Type u} {s : set (set α)} {t : set α} :
⋃₀s t ∀ (t' : set α), t' st' t

theorem set.subset_sInter {α : Type u} {S : set (set α)} {t : set α} :
(∀ (t' : set α), t' St t')t ⋂₀S

theorem set.sUnion_subset_sUnion {α : Type u} {S T : set (set α)} :
S T⋃₀S ⋃₀T

theorem set.sInter_subset_sInter {α : Type u} {S T : set (set α)} :
S T⋂₀T ⋂₀S

@[simp]
theorem set.sUnion_empty {α : Type u} :

@[simp]
theorem set.sInter_empty {α : Type u} :

@[simp]
theorem set.sUnion_singleton {α : Type u} (s : set α) :
⋃₀{s} = s

@[simp]
theorem set.sInter_singleton {α : Type u} (s : set α) :
⋂₀{s} = s

theorem set.sUnion_union {α : Type u} (S T : set (set α)) :

theorem set.sInter_union {α : Type u} (S T : set (set α)) :

theorem set.sInter_Union {α : Type u} {ι : Sort x} (s : ι → set (set α)) :
(⋂₀⋃ (i : ι), s i) = ⋂ (i : ι), ⋂₀s i

@[simp]
theorem set.sUnion_insert {α : Type u} (s : set α) (T : set (set α)) :

@[simp]
theorem set.sInter_insert {α : Type u} (s : set α) (T : set (set α)) :

theorem set.sUnion_pair {α : Type u} (s t : set α) :
⋃₀{s, t} = s t

theorem set.sInter_pair {α : Type u} (s t : set α) :
⋂₀{s, t} = s t

@[simp]
theorem set.sUnion_image {α : Type u} {β : Type v} (f : α → set β) (s : set α) :
⋃₀(f '' s) = ⋃ (x : α) (H : x s), f x

@[simp]
theorem set.sInter_image {α : Type u} {β : Type v} (f : α → set β) (s : set α) :
⋂₀(f '' s) = ⋂ (x : α) (H : x s), f x

@[simp]
theorem set.sUnion_range {β : Type v} {ι : Sort x} (f : ι → set β) :
⋃₀set.range f = ⋃ (x : ι), f x

@[simp]
theorem set.sInter_range {β : Type v} {ι : Sort x} (f : ι → set β) :
⋂₀set.range f = ⋂ (x : ι), f x

theorem set.sUnion_eq_univ_iff {α : Type u} {c : set (set α)} :
⋃₀c = set.univ ∀ (a : α), ∃ (b : set α) (H : b c), a b

theorem set.compl_sUnion {α : Type u} (S : set (set α)) :

theorem set.sUnion_eq_compl_sInter_compl {α : Type u} (S : set (set α)) :

theorem set.compl_sInter {α : Type u} (S : set (set α)) :

theorem set.sInter_eq_comp_sUnion_compl {α : Type u} (S : set (set α)) :

theorem set.inter_empty_of_inter_sUnion_empty {α : Type u} {s t : set α} {S : set (set α)} :
t Ss ⋃₀S = s t =

theorem set.range_sigma_eq_Union_range {α : Type u} {β : Type v} {γ : α → Type u_1} (f : sigma γ → β) :
set.range f = ⋃ (a : α), set.range (λ (b : γ a), f a, b⟩)

theorem set.Union_eq_range_sigma {α : Type u} {β : Type v} (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 '' (sigma.mk i ⁻¹' s)) = s

theorem set.sUnion_mono {α : Type u} {s t : set (set α)} :
s t⋃₀s ⋃₀t

theorem set.Union_subset_Union {α : Type u} {ι : Sort x} {s t : ι → set α} :
(∀ (i : ι), s i t i)((⋃ (i : ι), s i) ⋃ (i : ι), t i)

theorem set.Union_subset_Union2 {α : Type u} {ι : Sort x} {ι₂ : Sort u_1} {s : ι → set α} {t : ι₂ → set α} :
(∀ (i : ι), ∃ (j : ι₂), s i t j)((⋃ (i : ι), s i) ⋃ (i : ι₂), t i)

theorem set.Union_subset_Union_const {α : Type u} {ι ι₂ : Sort x} {s : set α} :
(ι → ι₂)((⋃ (i : ι), s) ⋃ (j : ι₂), s)

@[simp]
theorem set.Union_of_singleton (α : Type u) :
(⋃ (x : α), {x}) = set.univ

theorem set.bUnion_subset_Union {α : Type u} {β : Type v} (s : set α) (t : α → set β) :
(⋃ (x : α) (H : x s), t x) ⋃ (x : α), t x

theorem set.sUnion_eq_bUnion {α : Type u} {s : set (set α)} :
⋃₀s = ⋃ (i : set α) (h : i s), i

theorem set.sInter_eq_bInter {α : Type u} {s : set (set α)} :
⋂₀s = ⋂ (i : set α) (h : i s), i

theorem set.sUnion_eq_Union {α : Type u} {s : set (set α)} :
⋃₀s = ⋃ (i : s), i

theorem set.sInter_eq_Inter {α : Type u} {s : set (set α)} :
⋂₀s = ⋂ (i : s), i

theorem set.union_eq_Union {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = ⋃ (b : bool), cond b s₁ s₂

theorem set.inter_eq_Inter {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = ⋂ (b : bool), cond b s₁ s₂

theorem set.sInter_union_sInter {α : Type u} {S T : set (set α)} :
⋂₀S ⋂₀T = ⋂ (p : set α × set α) (H : p S.prod T), p.fst p.snd

theorem set.sUnion_inter_sUnion {α : Type u} {s t : set (set α)} :
⋃₀s ⋃₀t = ⋃ (p : set α × set α) (H : p s.prod t), p.fst p.snd

theorem set.sInter_bUnion {α : Type u} {S : set (set α)} {T : Π (s : set α), s Sset (set α)} :
(∀ (s : set α) (H : s S), s = ⋂₀T s H)(⋂₀⋃ (s : set α) (H : s S), T s H) = ⋂₀S

If S is a set of sets, and each s ∈ S can be represented as an intersection of sets T s hs, then ⋂₀ S is the intersection of the union of all T s hs.

theorem set.sUnion_bUnion {α : Type u} {S : set (set α)} {T : Π (s : set α), s Sset (set α)} :
(∀ (s : set α) (H : s S), s = ⋃₀T s H)(⋃₀⋃ (s : set α) (H : s S), T s H) = ⋃₀S

If S is a set of sets, and each s ∈ S can be represented as an union of sets T s hs, then ⋃₀ S is the union of the union of all T s hs.

theorem set.Union_range_eq_sUnion {α : Type u_1} {β : Type u_2} (C : set (set α)) {f : Π (s : C), β → s} :
(∀ (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} {β : Type u_3} (C : ι → set α) {f : Π (x : ι), β → (C x)} :
(∀ (x : ι), function.surjective (f x))((⋃ (y : β), set.range (λ (x : ι), (f x y).val)) = ⋃ (x : ι), C x)

theorem set.union_distrib_Inter_right {α : Type u} {ι : Type u_1} (s : ι → set α) (t : set α) :
(⋂ (i : ι), s i) t = ⋂ (i : ι), s i t

theorem set.union_distrib_Inter_left {α : Type u} {ι : Type u_1} (s : ι → set α) (t : set α) :
(t ⋂ (i : ι), s i) = ⋂ (i : ι), t s i

maps_to

theorem set.maps_to_sUnion {α : Type u} {β : Type v} {S : set (set α)} {t : set β} {f : α → β} :
(∀ (s : set α), s Sset.maps_to f s t)set.maps_to f (⋃₀S) t

theorem set.maps_to_Union {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} {t : set β} {f : α → β} :
(∀ (i : ι), set.maps_to f (s i) t)set.maps_to f (⋃ (i : ι), s i) t

theorem set.maps_to_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p iset α} {t : set β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.maps_to f (s i hi) t)set.maps_to f (⋃ (i : ι) (hi : p i), s i hi) t

theorem set.maps_to_Union_Union {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.maps_to f (s i) (t i))set.maps_to f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem set.maps_to_bUnion_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p iset α} {t : Π (i : ι), p iset β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.maps_to f (s i hi) (t i hi))set.maps_to f (⋃ (i : ι) (hi : p i), s i hi) (⋃ (i : ι) (hi : p i), t i hi)

theorem set.maps_to_sInter {α : Type u} {β : Type v} {s : set α} {T : set (set β)} {f : α → β} :
(∀ (t : set β), t Tset.maps_to f s t)set.maps_to f s (⋂₀T)

theorem set.maps_to_Inter {α : Type u} {β : Type v} {ι : Sort x} {s : set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.maps_to f s (t i))set.maps_to f s (⋂ (i : ι), t i)

theorem set.maps_to_bInter {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : set α} {t : Π (i : ι), p iset β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.maps_to f s (t i hi))set.maps_to f s (⋂ (i : ι) (hi : p i), t i hi)

theorem set.maps_to_Inter_Inter {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.maps_to f (s i) (t i))set.maps_to f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

theorem set.maps_to_bInter_bInter {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p iset α} {t : Π (i : ι), p iset β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.maps_to f (s i hi) (t i hi))set.maps_to f (⋂ (i : ι) (hi : p i), s i hi) (⋂ (i : ι) (hi : p i), t i hi)

theorem set.image_Inter_subset {α : Type u} {β : Type v} {ι : Sort x} (s : ι → set α) (f : α → β) :
(f '' ⋂ (i : ι), s i) ⋂ (i : ι), f '' s i

theorem set.image_bInter_subset {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} (s : Π (i : ι), p iset α) (f : α → β) :
(f '' ⋂ (i : ι) (hi : p i), s i hi) ⋂ (i : ι) (hi : p i), f '' s i hi

theorem set.image_sInter_subset {α : Type u} {β : Type v} (S : set (set α)) (f : α → β) :
f '' ⋂₀S ⋂ (s : set α) (H : s S), f '' s

inj_on

theorem set.inj_on.image_Inter_eq {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {s : ι → set α} {f : α → β} :
set.inj_on f (⋃ (i : ι), s i)((f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i)

theorem set.inj_on.image_bInter_eq {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p iset α} (hp : ∃ (i : ι), p i) {f : α → β} :
set.inj_on f (⋃ (i : ι) (hi : p i), s i hi)((f '' ⋂ (i : ι) (hi : p i), s i hi) = ⋂ (i : ι) (hi : p i), f '' s i hi)

theorem set.inj_on_Union_of_directed {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} (hs : directed has_subset.subset s) {f : α → β} :
(∀ (i : ι), set.inj_on f (s i))set.inj_on f (⋃ (i : ι), s i)

surj_on

theorem set.surj_on_sUnion {α : Type u} {β : Type v} {s : set α} {T : set (set β)} {f : α → β} :
(∀ (t : set β), t Tset.surj_on f s t)set.surj_on f s (⋃₀T)

theorem set.surj_on_Union {α : Type u} {β : Type v} {ι : Sort x} {s : set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.surj_on f s (t i))set.surj_on f s (⋃ (i : ι), t i)

theorem set.surj_on_Union_Union {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.surj_on f (s i) (t i))set.surj_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem set.surj_on_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : set α} {t : Π (i : ι), p iset β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.surj_on f s (t i hi))set.surj_on f s (⋃ (i : ι) (hi : p i), t i hi)

theorem set.surj_on_bUnion_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p iset α} {t : Π (i : ι), p iset β} {f : α → β} :
(∀ (i : ι) (hi : p i), set.surj_on f (s i hi) (t i hi))set.surj_on f (⋃ (i : ι) (hi : p i), s i hi) (⋃ (i : ι) (hi : p i), t i hi)

theorem set.surj_on_Inter {α : Type u} {β : Type v} {ι : Sort x} [hi : nonempty ι] {s : ι → set α} {t : set β} {f : α → β} :
(∀ (i : ι), set.surj_on f (s i) t)set.inj_on f (⋃ (i : ι), s i)set.surj_on f (⋂ (i : ι), s i) t

theorem set.surj_on_Inter_Inter {α : Type u} {β : Type v} {ι : Sort x} [hi : nonempty ι] {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.surj_on f (s i) (t i))set.inj_on f (⋃ (i : ι), s i)set.surj_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

bij_on

theorem set.bij_on_Union {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.bij_on f (s i) (t i))set.inj_on f (⋃ (i : ι), s i)set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem set.bij_on_Inter {α : Type u} {β : Type v} {ι : Sort x} [hi : nonempty ι] {s : ι → set α} {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.bij_on f (s i) (t i))set.inj_on f (⋃ (i : ι), s i)set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

theorem set.bij_on_Union_of_directed {α : Type u} {β : Type v} {ι : Sort x} {s : ι → set α} (hs : directed has_subset.subset s) {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.bij_on f (s i) (t i))set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem set.bij_on_Inter_of_directed {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {s : ι → set α} (hs : directed has_subset.subset s) {t : ι → set β} {f : α → β} :
(∀ (i : ι), set.bij_on f (s i) (t i))set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

@[simp]
theorem set.Inter_pos {α : Type u} {p : Prop} {μ : p → set α} (hp : p) :
(⋂ (h : p), μ h) = μ hp

@[simp]
theorem set.Inter_neg {α : Type u} {p : Prop} {μ : p → set α} :
¬p → (⋂ (h : p), μ h) = set.univ

@[simp]
theorem set.Union_pos {α : Type u} {p : Prop} {μ : p → set α} (hp : p) :
(⋃ (h : p), μ h) = μ hp

@[simp]
theorem set.Union_neg {α : Type u} {p : Prop} {μ : p → set α} :
¬p → (⋃ (h : p), μ h) =

@[simp]
theorem set.Union_empty {α : Type u} {ι : Sort u_1} :
(⋃ (i : ι), ) =

@[simp]
theorem set.Inter_univ {α : Type u} {ι : Sort u_1} :
(⋂ (i : ι), set.univ) = set.univ

theorem set.image_Union {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {s : ι → set α} :
(f '' ⋃ (i : ι), s i) = ⋃ (i : ι), f '' s i

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

theorem set.range_eq_Union {α : Type u} {ι : Sort u_1} (f : ι → α) :
set.range f = ⋃ (i : ι), {f i}

theorem set.image_eq_Union {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f '' s = ⋃ (i : α) (H : i s), {f i}

@[simp]
theorem set.bUnion_range {α : Type u} {β : Type v} {ι : Sort x} {f : ι → α} {g : α → set β} :
(⋃ (x : α) (H : x set.range f), g x) = ⋃ (y : ι), g (f y)

@[simp]
theorem set.bInter_range {α : Type u} {β : Type v} {ι : Sort x} {f : ι → α} {g : α → set β} :
(⋂ (x : α) (H : x set.range f), g x) = ⋂ (y : ι), g (f y)

@[simp]
theorem set.bUnion_image {α : Type u} {β : Type v} {γ : Type w} {s : set γ} {f : γ → α} {g : α → set β} :
(⋃ (x : α) (H : x f '' s), g x) = ⋃ (y : γ) (H : y s), g (f y)

@[simp]
theorem set.bInter_image {α : Type u} {β : Type v} {γ : Type w} {s : set γ} {f : γ → α} {g : α → set β} :
(⋂ (x : α) (H : x f '' s), g x) = ⋂ (y : γ) (H : y s), g (f y)

theorem set.Union_image_left {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) {s : set α} {t : set β} :
(⋃ (a : α) (H : a s), f a '' t) = set.image2 f s t

theorem set.Union_image_right {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) {s : set α} {t : set β} :
(⋃ (b : β) (H : b t), (λ (a : α), f a b) '' s) = set.image2 f s t

theorem set.monotone_preimage {α : Type u} {β : Type v} {f : α → β} :

@[simp]
theorem set.preimage_Union {α : Type u} {β : Type v} {ι : Sort w} {f : α → β} {s : ι → set β} :
(f ⁻¹' ⋃ (i : ι), s i) = ⋃ (i : ι), f ⁻¹' s i

theorem set.preimage_bUnion {α : Type u} {β : Type v} {ι : Type u_1} {f : α → β} {s : set ι} {t : ι → set β} :
(f ⁻¹' ⋃ (i : ι) (H : i s), t i) = ⋃ (i : ι) (H : i s), f ⁻¹' t i

@[simp]
theorem set.preimage_sUnion {α : Type u} {β : Type v} {f : α → β} {s : set (set β)} :
f ⁻¹' ⋃₀s = ⋃ (t : set β) (H : t s), f ⁻¹' t

theorem set.preimage_Inter {α : Type u} {β : Type v} {ι : Sort u_1} {s : ι → set β} {f : α → β} :
(f ⁻¹' ⋂ (i : ι), s i) = ⋂ (i : ι), f ⁻¹' s i

theorem set.preimage_bInter {α : Type u} {β : Type v} {γ : Type w} {s : γ → set β} {t : set γ} {f : α → β} :
(f ⁻¹' ⋂ (i : γ) (H : i t), s i) = ⋂ (i : γ) (H : i t), f ⁻¹' s i

@[simp]
theorem set.bUnion_preimage_singleton {α : Type u} {β : Type v} (f : α → β) (s : set β) :
(⋃ (y : β) (H : y s), f ⁻¹' {y}) = f ⁻¹' s

theorem set.bUnion_range_preimage_singleton {α : Type u} {β : Type v} (f : α → β) :
(⋃ (y : β) (H : y set.range f), f ⁻¹' {y}) = set.univ

theorem set.monotone_prod {α : Type u} {β : Type v} {γ : Type w} [preorder α] {f : α → set β} {g : α → set γ} :
monotone fmonotone gmonotone (λ (x : α), (f x).prod (g x))

theorem set.prod_Union {α : Type u} {β : Type v} {ι : Sort u_1} {s : set α} {t : ι → set β} :
s.prod (⋃ (i : ι), t i) = ⋃ (i : ι), s.prod (t i)

theorem set.prod_bUnion {α : Type u} {β : Type v} {ι : Type u_1} {u : set ι} {s : set α} {t : ι → set β} :
s.prod (⋃ (i : ι) (H : i u), t i) = ⋃ (i : ι) (H : i u), s.prod (t i)

theorem set.prod_sUnion {α : Type u} {β : Type v} {s : set α} {C : set (set β)} :
s.prod (⋃₀C) = ⋃₀((λ (t : set β), s.prod t) '' C)

theorem set.Union_prod {α : Type u} {β : Type v} {ι : Sort u_1} {s : ι → set α} {t : set β} :
(⋃ (i : ι), s i).prod t = ⋃ (i : ι), (s i).prod t

theorem set.bUnion_prod {α : Type u} {β : Type v} {ι : Type u_1} {u : set ι} {s : ι → set α} {t : set β} :
(⋃ (i : ι) (H : i u), s i).prod t = ⋃ (i : ι) (H : i u), (s i).prod t

theorem set.sUnion_prod {α : Type u} {β : Type v} {C : set (set α)} {t : set β} :
(⋃₀C).prod t = ⋃₀((λ (s : set α), s.prod t) '' C)

theorem set.Union_prod_of_monotone {α : Type u} {β : Type v} {γ : Type w} [semilattice_sup α] {s : α → set β} {t : α → set γ} :
monotone smonotone t(⋃ (x : α), (s x).prod (t x)) = (⋃ (x : α), s x).prod (⋃ (x : α), t x)

def set.seq {α : Type u} {β : Type v} :
set (α → β)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
  • s.seq t = {b : β | ∃ (f : α → β) (H : f s) (a : α) (H : a t), f a = b}
theorem set.seq_def {α : Type u} {β : Type v} {s : set (α → β)} {t : set α} :
s.seq t = ⋃ (f : α → β) (H : f s), f '' t

@[simp]
theorem set.mem_seq_iff {α : Type u} {β : Type v} {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} {β : Type v} {s : set (α → β)} {t : set α} {u : set β} :
s.seq t u ∀ (f : α → β), f s∀ (a : α), a tf a u

theorem set.seq_mono {α : Type u} {β : Type v} {s₀ s₁ : set (α → β)} {t₀ t₁ : set α} :
s₀ s₁t₀ t₁s₀.seq t₀ s₁.seq t₁

theorem set.singleton_seq {α : Type u} {β : Type v} {f : α → β} {t : set α} :
{f}.seq t = f '' t

theorem set.seq_singleton {α : Type u} {β : Type v} {s : set (α → β)} {a : α} :
s.seq {a} = (λ (f : α → β), f a) '' s

theorem set.seq_seq {α : Type u} {β : Type v} {γ : Type w} {s : set (β → γ)} {t : set (α → β)} {u : set α} :
s.seq (t.seq u) = ((function.comp '' s).seq t).seq u

theorem set.image_seq {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {s : set (α → β)} {t : set α} :
f '' s.seq t = (function.comp f '' s).seq t

theorem set.prod_eq_seq {α : Type u} {β : Type v} {s : set α} {t : set β} :
s.prod t = (prod.mk '' s).seq t

theorem set.prod_image_seq_comm {α : Type u} {β : Type v} (s : set α) (t : set β) :
(prod.mk '' s).seq t = ((λ (b : β) (a : α), (a, b)) '' t).seq s

theorem set.image2_eq_seq {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s : set α) (t : set β) :
set.image2 f s t = (f '' s).seq t

@[instance]
def set.monad  :

Equations
@[simp]
theorem set.bind_def {α' β' : Type u} {s : set α'} {f : α' → set β'} :
s >>= f = ⋃ (i : α') (H : i s), f i

@[simp]
theorem set.fmap_eq_image {α' β' : Type u} {s : set α'} (f : α' → β') :
f <$> s = f '' s

@[simp]
theorem set.seq_eq_set_seq {α β : Type u_1} (s : set (α → β)) (t : set α) :
s <*> t = s.seq t

@[simp]
theorem set.pure_def {α : Type u} (a : α) :
pure a = {a}

theorem set.pi_def {α : Type u_1} {π : α → Type u_2} (i : set α) (s : Π (a : α), set («π» a)) :
i.pi s = ⋂ (a : α) (H : a i), (λ (f : Π (a : α), «π» a), f a) ⁻¹' s a

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

theorem disjoint.union_left {α : Type u} {s t u : set α} :
disjoint s udisjoint t udisjoint (s t) u

theorem disjoint.union_right {α : Type u} {s t u : set α} :
disjoint s tdisjoint s udisjoint s (t u)

theorem disjoint.preimage {α : Type u_1} {β : Type u_2} (f : α → β) {s t : set β} :
disjoint s tdisjoint (f ⁻¹' s) (f ⁻¹' t)

theorem set.disjoint_iff {α : Type u} {s t : set α} :

theorem set.disjoint_iff_inter_eq_empty {α : Type u} {s t : set α} :
disjoint s t s t =

theorem set.not_disjoint_iff {α : Type u} {s t : set α} :
¬disjoint s t ∃ (x : α), x s x t

theorem set.disjoint_left {α : Type u} {s t : set α} :
disjoint s t ∀ {a : α}, a sa t

theorem set.disjoint_right {α : Type u} {s t : set α} :
disjoint s t ∀ {a : α}, a ta s

theorem set.disjoint_of_subset_left {α : Type u} {s t u : set α} :
s udisjoint u tdisjoint s t

theorem set.disjoint_of_subset_right {α : Type u} {s t u : set α} :
t udisjoint s udisjoint s t

theorem set.disjoint_of_subset {α : Type u} {s t u v : set α} :
s ut vdisjoint u vdisjoint s t

@[simp]
theorem set.disjoint_union_left {α : Type u} {s t u : set α} :

@[simp]
theorem set.disjoint_union_right {α : Type u} {s t u : set α} :

theorem set.disjoint_diff {α : Type u} {a b : set α} :
disjoint a (b \ a)

theorem set.disjoint_compl_left {α : Type u} (s : set α) :

theorem set.disjoint_compl_right {α : Type u} (s : set α) :

@[simp]
theorem set.univ_disjoint {α : Type u} {s : set α} :

@[simp]
theorem set.disjoint_univ {α : Type u} {s : set α} :

@[simp]
theorem set.disjoint_singleton_left {α : Type u} {a : α} {s : set α} :
disjoint {a} s a s

@[simp]
theorem set.disjoint_singleton_right {α : Type u} {a : α} {s : set α} :
disjoint s {a} a s

theorem set.disjoint_image_image {α : Type u} {β : Type v} {γ : Type w} {f : β → α} {g : γ → α} {s : set β} {t : set γ} :
(∀ (b : β), b s∀ (c : γ), c tf b g c)disjoint (f '' s) (g '' t)

theorem set.pairwise_on_disjoint_fiber {α : Type u} {β : Type v} (f : α → β) (s : set β) :
s.pairwise_on (disjoint on λ (y : β), f ⁻¹' {y})

theorem set.preimage_eq_empty {α : Type u} {β : Type v} {f : α → β} {s : set β} :
disjoint s (set.range f)f ⁻¹' s =

theorem set.preimage_eq_empty_iff {α : Type u} {β : Type v} {f : α → β} {s : set β} :

def set.pairwise_disjoint {α : Type u} :
set (set α) → Prop

A collection of sets is pairwise_disjoint, if any two different sets in this collection are disjoint.

Equations
theorem set.pairwise_disjoint.subset {α : Type u} {s t : set (set α)} :

theorem set.pairwise_disjoint.range {α : Type u} {s : set (set α)} (f : s → set α) :
(∀ (x : s), f x x.val)s.pairwise_disjoint(set.range f).pairwise_disjoint

theorem set.pairwise_disjoint.elim {α : Type u} {s : set (set α)} (h : s.pairwise_disjoint) {x y : set α} (hx : x s) (hy : y s) (z : α) :
z xz yx = y

theorem set.subset_diff {α : Type u} {s t u : set α} :
s t \ u s t disjoint s u

def set.sigma_to_Union {α : Type u} {β : Type v} (t : α → set β) :
(Σ (i : α), (t i))(⋃ (i : α), t i)

If t is an indexed family of sets, then there is a natural map from Σ i, t i to ⋃ i, t i sending ⟨i, x⟩ to x.

Equations
theorem set.sigma_to_Union_surjective {α : Type u} {β : Type v} (t : α → set β) :

theorem set.sigma_to_Union_injective {α : Type u} {β : Type v} (t : α → set β) :
(∀ (i j : α), i jdisjoint (t i) (t j))function.injective (set.sigma_to_Union t)

theorem set.sigma_to_Union_bijective {α : Type u} {β : Type v} (t : α → set β) :
(∀ (i j : α), i jdisjoint (t i) (t j))function.bijective (set.sigma_to_Union t)

def set.Union_eq_sigma_of_disjoint {α : Type u} {β : Type v} {t : α → set β} :
(∀ (i j : α), i jdisjoint (t i) (t j))((⋃ (i : α), t i) Σ (i : α), (t i))

Equivalence between a disjoint union and a dependent sum.

Equations
def set.bUnion_eq_sigma_of_disjoint {α : Type u} {β : Type v} {s : set α} {t : α → set β} :
s.pairwise_on (disjoint on t)((⋃ (i : α) (H : i s), t i) Σ (i : s), (t i.val))

Equivalence between a disjoint bounded union and a dependent sum.

Equations