mathlib documentation

data.set.lattice

The set lattice #

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

Main declarations #

Naming convention #

In lemma names,

Notation #

Complete lattice and complete Boolean algebra instances #

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

Intersection of a set of sets.

Equations
source
@[simp]
theorem set.mem_sInter {α : Type u_1} {x : α} {S : set (set α)} :
x ∈ ⋂₀ S ↔ ∀ (t : set α), t ∈ S → x ∈ t
source
def set.Union {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
set β

Indexed union of a family of sets

Equations
source
def set.Inter {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
set β

Indexed intersection of a family of sets

Equations
source
@[simp]
theorem set.Sup_eq_sUnion {α : Type u_1} (S : set (set α)) :
Sup S = ⋃₀S
source
@[simp]
theorem set.Inf_eq_sInter {α : Type u_1} (S : set (set α)) :
Inf S = ⋂₀ S
source
@[simp]
theorem set.supr_eq_Union {α : Type u_1} {ι : Sort u_4} (s : ι → set α) :
supr s = set.Union s
source
@[simp]
theorem set.infi_eq_Inter {α : Type u_1} {ι : Sort u_4} (s : ι → set α) :
infi s = set.Inter s
source
@[simp]
theorem set.mem_Union {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι → set α} :
(x ∈ ⋃ (i : ι), s i) ↔ ∃ (i : ι), x ∈ s i
source
@[simp]
theorem set.mem_Inter {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι → set α} :
(x ∈ ⋂ (i : ι), s i) ↔ ∀ (i : ι), x ∈ s i
source
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
source
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
source
theorem set.mem_Union_of_mem {α : Type u_1} {ι : Sort u_4} {s : ι → set α} {a : α} (i : ι) (ha : a ∈ s i) :
a ∈ ⋃ (i : ι), s i
source
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
source
theorem set.mem_Inter_of_mem {α : Type u_1} {ι : Sort u_4} {s : ι → set α} {a : α} (h : ∀ (i : ι), a ∈ s i) :
a ∈ ⋂ (i : ι), s i
source
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
source
theorem set.mem_sUnion {α : Type u_1} {x : α} {S : set (set α)} :
x ∈ ⋃₀S ↔ ∃ (t : set α) (H : t ∈ S), x ∈ t
source
@[protected, instance]
def set.complete_boolean_algebra {α : Type u_1} :
complete_boolean_algebra (set α)
Equations
source
theorem set.monotone_image {α : Type u_1} {β : Type u_2} {f : α → β} :
monotone (set.image f)

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

source
theorem monotone.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x ∩ g x)
source
theorem antitone.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x ∩ g x)
source
theorem monotone.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x ∪ g x)
source
theorem antitone.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x ∪ g x)
source
theorem set.monotone_set_of {α : Type u_1} {β : Type u_2} [preorder α] {p : α → β → Prop} (hp : ∀ (b : β), monotone (λ (a : α), p a b)) :
monotone (λ (a : α), {b : β | p a b})
source
theorem set.antitone_set_of {α : Type u_1} {β : Type u_2} [preorder α] {p : α → β → Prop} (hp : ∀ (b : β), antitone (λ (a : α), p a b)) :
antitone (λ (a : α), {b : β | p a b})
source
theorem set.antitone_bforall {α : Type u_1} {P : α → Prop} :
antitone (λ (s : set α), ∀ (x : α), x ∈ s → P x)

Quantifying over a set is antitone in the set

source
@[protected]
theorem set.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} :
galois_connection (set.image f) (set.preimage f)
source
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
source
@[protected]
theorem set.preimage_kern_image {α : Type u_1} {β : Type u_2} {f : α → β} :
galois_connection (set.preimage f) (set.kern_image f)

Union and intersection over an indexed family of sets #

source
@[protected, instance]
def set.order_top {α : Type u_1} :
order_top (set α)
Equations
source
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) :
set.Union f₁ = set.Union f₂
source
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) :
set.Inter f₁ = set.Inter f₂
source
theorem set.Union_eq_if {α : Type u_1} {p : Prop} [decidable p] (s : set α) :
(⋃ (h : p), s) = ite p s ∅
source
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), ∅)
source
theorem set.Inter_eq_if {α : Type u_1} {p : Prop} [decidable p] (s : set α) :
(⋂ (h : p), s) = ite p s set.univ
source
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)
source
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
source
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) = ⊤) :
t.nonempty
source
theorem set.set_of_exists {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) :
{x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}
source
theorem set.set_of_forall {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) :
{x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}
source
theorem set.Union_subset {α : Type u_1} {ι : Sort u_4} {s : ι → set α} {t : set α} (h : ∀ (i : ι), s i ⊆ t) :
(⋃ (i : ι), s i) ⊆ t
source
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
source
theorem set.subset_Inter {β : Type u_2} {ι : Sort u_4} {t : set β} {s : ι → set β} (h : ∀ (i : ι), t ⊆ s i) :
t ⊆ ⋂ (i : ι), s i
source
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
source
@[simp]
theorem set.Union_subset_iff {α : Type u_1} {ι : Sort u_4} {s : ι → set α} {t : set α} :
(⋃ (i : ι), s i) ⊆ t ↔ ∀ (i : ι), s i ⊆ t
source
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
source
@[simp]
theorem set.subset_Inter_iff {α : Type u_1} {ι : Sort u_4} {s : set α} {t : ι → set α} :
(s ⊆ ⋂ (i : ι), t i) ↔ ∀ (i : ι), s ⊆ t i
source
@[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
source
theorem set.subset_Union {β : Type u_2} {ι : Sort u_4} (s : ι → set β) (i : ι) :
s i ⊆ ⋃ (i : ι), s i
source
theorem set.Inter_subset {β : Type u_2} {ι : Sort u_4} (s : ι → set β) (i : ι) :
(⋂ (i : ι), s i) ⊆ s i
source
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
source
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
source
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_Unionis convenient with apply, and has i explicit for this purpose.

source
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_subsetis convenient with apply, and has i explicit for this purpose.

source
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
source
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
source
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
source
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
source
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
source
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'
source
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
source
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'
source
theorem set.Union₂_subset_Union {α : Type u_1} {ι : Sort u_4} (κ : ι → Sort u_2) (s : ι → set α) :
(⋃ (i : ι) (j : κ i), s i) ⊆ ⋃ (i : ι), s i
source
theorem set.Inter_subset_Inter₂ {α : Type u_1} {ι : Sort u_4} (κ : ι → Sort u_2) (s : ι → set α) :
(⋂ (i : ι), s i) ⊆ ⋂ (i : ι) (j : κ i), s i
source
theorem set.Union_set_of {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) :
(⋃ (i : ι), {x : α | P i x}) = {x : α | ∃ (i : ι), P i x}
source
theorem set.Inter_set_of {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) :
(⋂ (i : ι), {x : α | P i x}) = {x : α | ∀ (i : ι), P i x}
source
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
source
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
source
theorem set.Union_const {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) :
(⋃ (i : ι), s) = s
source
theorem set.Inter_const {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) :
(⋂ (i : ι), s) = s
source
@[simp]
theorem set.compl_Union {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
(⋃ (i : ι), s i)ᶜ = ⋂ (i : ι), (s i)ᶜ
source
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)ᶜ
source
@[simp]
theorem set.compl_Inter {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
(⋂ (i : ι), s i)ᶜ = ⋃ (i : ι), (s i)ᶜ
source
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)ᶜ
source
theorem set.Union_eq_compl_Inter_compl {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
(⋃ (i : ι), s i) = (⋂ (i : ι), (s i)ᶜ)ᶜ
source
theorem set.Inter_eq_compl_Union_compl {β : Type u_2} {ι : Sort u_4} (s : ι → set β) :
(⋂ (i : ι), s i) = (⋃ (i : ι), (s i)ᶜ)ᶜ
source
theorem set.inter_Union {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι → set β) :
(s ∩ ⋃ (i : ι), t i) = ⋃ (i : ι), s ∩ t i
source
theorem set.Union_inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) ∩ s = ⋃ (i : ι), t i ∩ s
source
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
source
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
source
theorem set.union_Union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι → set β) :
(s ∪ ⋃ (i : ι), t i) = ⋃ (i : ι), s ∪ t i
source
theorem set.Union_union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) ∪ s = ⋃ (i : ι), t i ∪ s
source
theorem set.inter_Inter {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι → set β) :
(s ∩ ⋂ (i : ι), t i) = ⋂ (i : ι), s ∩ t i
source
theorem set.Inter_inter {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι → set β) :
(⋂ (i : ι), t i) ∩ s = ⋂ (i : ι), t i ∩ s
source
theorem set.union_Inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι → set β) :
(s ∪ ⋂ (i : ι), t i) = ⋂ (i : ι), s ∪ t i
source
theorem set.Union_diff {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι → set β) :
(⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s
source
theorem set.diff_Union {β : Type u_2} {ι : Sort u_4} [nonempty ι] (s : set β) (t : ι → set β) :
(s \ ⋃ (i : ι), t i) = ⋂ (i : ι), s \ t i
source
theorem set.diff_Inter {β : Type u_2} {ι : Sort u_4} (s : set β) (t : ι → set β) :
(s \ ⋂ (i : ι), t i) = ⋃ (i : ι), s \ t i
source
theorem set.directed_on_Union {α : Type u_1} {ι : Sort u_4} {r : α → α → Prop} {f : ι → set α} (hd : directed has_subset.subset f) (h : ∀ (x : ι), directed_on r (f x)) :
directed_on r (⋃ (x : ι), f x)
source
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
source
theorem set.Union_inter_of_monotone {ι : Type u_1} {α : Type u_2} [semilattice_sup ι] {s t : ι → set α} (hs : monotone s) (ht : monotone t) :
(⋃ (i : ι), s i ∩ t i) = (⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i
source
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.

source
theorem set.Union_option {α : Type u_1} {ι : Type u_2} (s : option ι → set α) :
(⋃ (o : option ι), s o) = s none ∪ ⋃ (i : ι), s (some i)
source
theorem set.Inter_option {α : Type u_1} {ι : Type u_2} (s : option ι → set α) :
(⋂ (o : option ι), s o) = s none ∩ ⋂ (i : ι), s (some i)
source
theorem set.Union_dite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [decidable_pred p] (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
source
theorem set.Union_ite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [decidable_pred p] (f g : ι → set α) :
(⋃ (i : ι), ite (p i) (f i) (g i)) = (⋃ (i : ι) (h : p i), f i) ∪ ⋃ (i : ι) (h : ¬p i), g i
source
theorem set.Inter_dite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [decidable_pred p] (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
source
theorem set.Inter_ite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [decidable_pred p] (f g : ι → set α) :
(⋂ (i : ι), ite (p i) (f i) (g i)) = (⋂ (i : ι) (h : p i), f i) ∩ ⋂ (i : ι) (h : ¬p i), g i
source
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 #

source
@[simp]
theorem set.Inter_false {α : Type u_1} {s : false → set α} :
set.Inter s = set.univ
source
@[simp]
theorem set.Union_false {α : Type u_1} {s : false → set α} :
set.Union s = ∅
source
@[simp]
theorem set.Inter_true {α : Type u_1} {s : true → set α} :
set.Inter s = s trivial
source
@[simp]
theorem set.Union_true {α : Type u_1} {s : true → set α} :
set.Union s = s trivial
source
@[simp]
theorem set.Inter_exists {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → set α} :
(⋂ (x : Exists p), f x) = ⋂ (i : ι) (h : p i), f _
source
@[simp]
theorem set.Union_exists {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → set α} :
(⋃ (x : Exists p), f x) = ⋃ (i : ι) (h : p i), f _
source
@[simp]
theorem set.Union_empty {α : Type u_1} {ι : Sort u_4} :
(⋃ (i : ι), ∅) = ∅
source
@[simp]
theorem set.Inter_univ {α : Type u_1} {ι : Sort u_4} :
(⋂ (i : ι), set.univ) = set.univ
source
@[simp]
theorem set.Union_eq_empty {α : Type u_1} {ι : Sort u_4} {s : ι → set α} :
(⋃ (i : ι), s i) = ∅ ↔ ∀ (i : ι), s i = ∅
source
@[simp]
theorem set.Inter_eq_univ {α : Type u_1} {ι : Sort u_4} {s : ι → set α} :
(⋂ (i : ι), s i) = set.univ ↔ ∀ (i : ι), s i = set.univ
source
@[simp]
theorem set.nonempty_Union {α : Type u_1} {ι : Sort u_4} {s : ι → set α} :
(⋃ (i : ι), s i).nonempty ↔ ∃ (i : ι), (s i).nonempty
source
@[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
source
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 _
source
@[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
source
@[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
source
@[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
source
@[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
source
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 _
source
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 _
source
theorem set.Union_and {α : Type u_1} {p q : Prop} (s : p ∧ q → set α) :
(⋃ (h : p ∧ q), s h) = ⋃ (hp : p) (hq : q), s _
source
theorem set.Inter_and {α : Type u_1} {p q : Prop} (s : p ∧ q → set α) :
(⋂ (h : p ∧ q), s h) = ⋂ (hp : p) (hq : q), s _
source
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'
source
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'
source
@[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 _
source
@[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 _
source
@[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 _
source
@[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 _
source
@[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 _
source
@[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 #

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

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

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

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

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 _
source
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 _
source
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⟩
source
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⟩
source
theorem set.bInter_empty {α : Type u_1} {β : Type u_2} (u : α → set β) :
(⋂ (x : α) (H : x ∈ ∅), u x) = set.univ
source
theorem set.bInter_univ {α : Type u_1} {β : Type u_2} (u : α → set β) :
(⋂ (x : α) (H : x ∈ set.univ), u x) = ⋂ (x : α), u x
source
@[simp]
theorem set.bUnion_self {α : Type u_1} (s : set α) :
(⋃ (x : α) (H : x ∈ s), s) = s
source
@[simp]
theorem set.Union_nonempty_self {α : Type u_1} (s : set α) :
(⋃ (h : s.nonempty), s) = s
source
theorem set.bInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋂ (x : α) (H : x ∈ {a}), s x) = s a
source
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
source
theorem set.bInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : set α) (t : α → set β) :
(⋂ (x : α) (H : x ∈ insert a s), t x) = t a ∩ ⋂ (x : α) (H : x ∈ s), t x
source
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
source
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
source
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
source
theorem set.bUnion_empty {α : Type u_1} {β : Type u_2} (s : α → set β) :
(⋃ (x : α) (H : x ∈ ∅), s x) = ∅
source
theorem set.bUnion_univ {α : Type u_1} {β : Type u_2} (s : α → set β) :
(⋃ (x : α) (H : x ∈ set.univ), s x) = ⋃ (x : α), s x
source
theorem set.bUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → set β) :
(⋃ (x : α) (H : x ∈ {a}), s x) = s a
source
@[simp]
theorem set.bUnion_of_singleton {α : Type u_1} (s : set α) :
(⋃ (x : α) (H : x ∈ s), {x}) = s
source
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
source
@[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⟩
source
@[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⟩
source
theorem set.bUnion_insert {α : Type u_1} {β : Type u_2} (a : α) (s : set α) (t : α → set β) :
(⋃ (x : α) (H : x ∈ insert a s), t x) = t a ∪ ⋃ (x : α) (H : x ∈ s), t x
source
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
source
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
source
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
source
theorem set.mem_sUnion_of_mem {α : Type u_1} {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
x ∈ ⋃₀S
source
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
source
theorem set.sInter_subset_of_mem {α : Type u_1} {S : set (set α)} {t : set α} (tS : t ∈ S) :
⋂₀ S ⊆ t
source
theorem set.subset_sUnion_of_mem {α : Type u_1} {S : set (set α)} {t : set α} (tS : t ∈ S) :
t ⊆ ⋃₀S
source
theorem set.subset_sUnion_of_subset {α : Type u_1} {s : set α} (t : set (set α)) (u : set α) (h₁ : s ⊆ u) (h₂ : u ∈ t) :
s ⊆ ⋃₀t
source
theorem set.sUnion_subset {α : Type u_1} {S : set (set α)} {t : set α} (h : ∀ (t' : set α), t' ∈ S → t' ⊆ t) :
⋃₀S ⊆ t
source
@[simp]
theorem set.sUnion_subset_iff {α : Type u_1} {s : set (set α)} {t : set α} :
⋃₀s ⊆ t ↔ ∀ (t' : set α), t' ∈ s → t' ⊆ t
source
theorem set.subset_sInter {α : Type u_1} {S : set (set α)} {t : set α} (h : ∀ (t' : set α), t' ∈ S → t ⊆ t') :
t ⊆ ⋂₀ S
source
@[simp]
theorem set.subset_sInter_iff {α : Type u_1} {S : set (set α)} {t : set α} :
t ⊆ ⋂₀ S ↔ ∀ (t' : set α), t' ∈ S → t ⊆ t'
source
theorem set.sUnion_subset_sUnion {α : Type u_1} {S T : set (set α)} (h : S ⊆ T) :
⋃₀S ⊆ ⋃₀T
source
theorem set.sInter_subset_sInter {α : Type u_1} {S T : set (set α)} (h : S ⊆ T) :
⋂₀ T ⊆ ⋂₀ S
source
@[simp]
theorem set.sUnion_empty {α : Type u_1} :
⋃₀∅ = ∅
source
@[simp]
theorem set.sInter_empty {α : Type u_1} :
⋂₀ ∅ = set.univ
source
@[simp]
theorem set.sUnion_singleton {α : Type u_1} (s : set α) :
⋃₀{s} = s
source
@[simp]
theorem set.sInter_singleton {α : Type u_1} (s : set α) :
⋂₀ {s} = s
source
@[simp]
theorem set.sUnion_eq_empty {α : Type u_1} {S : set (set α)} :
⋃₀S = ∅ ↔ ∀ (s : set α), s ∈ S → s = ∅
source
@[simp]
theorem set.sInter_eq_univ {α : Type u_1} {S : set (set α)} :
⋂₀ S = set.univ ↔ ∀ (s : set α), s ∈ S → s = set.univ
source
@[simp]
theorem set.nonempty_sUnion {α : Type u_1} {S : set (set α)} :
(⋃₀S).nonempty ↔ ∃ (s : set α) (H : s ∈ S), s.nonempty
source
theorem set.nonempty.of_sUnion {α : Type u_1} {s : set (set α)} (h : (⋃₀s).nonempty) :
s.nonempty
source
theorem set.nonempty.of_sUnion_eq_univ {α : Type u_1} [nonempty α] {s : set (set α)} (h : ⋃₀s = set.univ) :
s.nonempty
source
theorem set.sUnion_union {α : Type u_1} (S T : set (set α)) :
⋃₀(S ∪ T) = ⋃₀S ∪ ⋃₀T
source
theorem set.sInter_union {α : Type u_1} (S T : set (set α)) :
⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T
source
@[simp]
theorem set.sUnion_insert {α : Type u_1} (s : set α) (T : set (set α)) :
⋃₀insert s T = s ∪ ⋃₀T
source
@[simp]
theorem set.sInter_insert {α : Type u_1} (s : set α) (T : set (set α)) :
⋂₀ insert s T = s ∩ ⋂₀ T
source
theorem set.sUnion_pair {α : Type u_1} (s t : set α) :
⋃₀{s, t} = s ∪ t
source
theorem set.sInter_pair {α : Type u_1} (s t : set α) :
⋂₀ {s, t} = s ∩ t
source
@[simp]
theorem set.sUnion_image {α : Type u_1} {β : Type u_2} (f : α → set β) (s : set α) :
⋃₀(f '' s) = ⋃ (x : α) (H : x ∈ s), f x
source
@[simp]
theorem set.sInter_image {α : Type u_1} {β : Type u_2} (f : α → set β) (s : set α) :
⋂₀ (f '' s) = ⋂ (x : α) (H : x ∈ s), f x
source
@[simp]
theorem set.sUnion_range {β : Type u_2} {ι : Sort u_4} (f : ι → set β) :
⋃₀set.range f = ⋃ (x : ι), f x
source
@[simp]
theorem set.sInter_range {β : Type u_2} {ι : Sort u_4} (f : ι → set β) :
⋂₀ set.range f = ⋂ (x : ι), f x
source
theorem set.Union_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {f : ι → set α} :
(⋃ (i : ι), f i) = set.univ ↔ ∀ (x : α), ∃ (i : ι), x ∈ f i
source
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
source
theorem set.sUnion_eq_univ_iff {α : Type u_1} {c : set (set α)} :
⋃₀c = set.univ ↔ ∀ (a : α), ∃ (b : set α) (H : b ∈ c), a ∈ b
source
theorem set.Inter_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι → set α} :
(⋂ (i : ι), f i) = ∅ ↔ ∀ (x : α), ∃ (i : ι), x ∉ f i
source
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
source
theorem set.sInter_eq_empty_iff {α : Type u_1} {c : set (set α)} :
⋂₀ c = ∅ ↔ ∀ (a : α), ∃ (b : set α) (H : b ∈ c), a ∉ b
source
@[simp]
theorem set.nonempty_Inter {α : Type u_1} {ι : Sort u_4} {f : ι → set α} :
(⋂ (i : ι), f i).nonempty ↔ ∃ (x : α), ∀ (i : ι), x ∈ f i
source
@[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
source
@[simp]
theorem set.nonempty_sInter {α : Type u_1} {c : set (set α)} :
(⋂₀ c).nonempty ↔ ∃ (a : α), ∀ (b : set α), b ∈ c → a ∈ b
source
theorem set.compl_sUnion {α : Type u_1} (S : set (set α)) :
(⋃₀S)ᶜ = ⋂₀ (compl '' S)
source
theorem set.sUnion_eq_compl_sInter_compl {α : Type u_1} (S : set (set α)) :
⋃₀S = (⋂₀ (compl '' S))ᶜ
source
theorem set.compl_sInter {α : Type u_1} (S : set (set α)) :
(⋂₀ S)ᶜ = ⋃₀(compl '' S)
source
theorem set.sInter_eq_compl_sUnion_compl {α : Type u_1} (S : set (set α)) :
⋂₀ S = (⋃₀(compl '' S))ᶜ
source
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 = ∅
source
theorem set.range_sigma_eq_Union_range {α : Type u_1} {β : Type u_2} {γ : α → Type u_3} (f : sigma γ → β) :
set.range f = ⋃ (a : α), set.range (λ (b : γ a), f ⟨a, b⟩)
source
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))
source
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
source
theorem set.sigma.univ {α : Type u_1} (X : α → Type u_2) :
set.univ = ⋃ (a : α), set.range (sigma.mk a)
source
theorem set.sUnion_mono {α : Type u_1} {s t : set (set α)} (h : s ⊆ t) :
⋃₀s ⊆ ⋃₀t
source
theorem set.Union_subset_Union_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : set α} (h : ι → ι₂) :
(⋃ (i : ι), s) ⊆ ⋃ (j : ι₂), s
source
@[simp]
theorem set.Union_singleton_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) :
(⋃ (x : α), {f x}) = set.range f
source
theorem set.Union_of_singleton (α : Type u_1) :
(⋃ (x : α), {x}) = set.univ
source
theorem set.Union_of_singleton_coe {α : Type u_1} (s : set α) :
(⋃ (i : ↥s), {↑i}) = s
source
theorem set.sUnion_eq_bUnion {α : Type u_1} {s : set (set α)} :
⋃₀s = ⋃ (i : set α) (h : i ∈ s), i
source
theorem set.sInter_eq_bInter {α : Type u_1} {s : set (set α)} :
⋂₀ s = ⋂ (i : set α) (h : i ∈ s), i
source
theorem set.sUnion_eq_Union {α : Type u_1} {s : set (set α)} :
⋃₀s = ⋃ (i : ↥s), ↑i
source
theorem set.sInter_eq_Inter {α : Type u_1} {s : set (set α)} :
⋂₀ s = ⋂ (i : ↥s), ↑i
source
theorem set.union_eq_Union {α : Type u_1} {s₁ s₂ : set α} :
s₁ ∪ s₂ = ⋃ (b : bool), cond b s₁ s₂
source
theorem set.inter_eq_Inter {α : Type u_1} {s₁ s₂ : set α} :
s₁ ∩ s₂ = ⋂ (b : bool), cond b s₁ s₂
source
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
source
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
source
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
source
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
source
theorem set.sUnion_Union {α : Type u_1} {ι : Sort u_4} (s : ι → set (set α)) :
(⋃₀⋃ (i : ι), s i) = ⋃ (i : ι), ⋃₀s i
source
theorem set.sInter_Union {α : Type u_1} {ι : Sort u_4} (s : ι → set (set α)) :
(⋂₀ ⋃ (i : ι), s i) = ⋂ (i : ι), ⋂₀ s i
source
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
source
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
source
theorem set.union_distrib_Inter_left {α : Type u_1} {ι : Sort u_4} (s : ι → set α) (t : set α) :
(t ∪ ⋂ (i : ι), s i) = ⋂ (i : ι), t ∪ s i
source
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
source
theorem set.union_distrib_Inter_right {α : Type u_1} {ι : Sort u_4} (s : ι → set α) (t : set α) :
(⋂ (i : ι), s i) ∪ t = ⋂ (i : ι), s i ∪ t
source
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 #

source
theorem set.maps_to_sUnion {α : Type u_1} {β : Type u_2} {S : set (set α)} {t : set β} {f : α → β} (H : ∀ (s : set α), s ∈ S → set.maps_to f s t) :
set.maps_to f (⋃₀S) t
source
theorem set.maps_to_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} {t : set β} {f : α → β} (H : ∀ (i : ι), set.maps_to f (s i) t) :
set.maps_to f (⋃ (i : ι), s i) t
source
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), set.maps_to f (s i j) t) :
set.maps_to f (⋃ (i : ι) (j : κ i), s i j) t
source
theorem set.maps_to_Union_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.maps_to f (s i) (t i)) :
set.maps_to f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
source
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), set.maps_to f (s i j) (t i j)) :
set.maps_to f (⋃ (i : ι) (j : κ i), s i j) (⋃ (i : ι) (j : κ i), t i j)
source
theorem set.maps_to_sInter {α : Type u_1} {β : Type u_2} {s : set α} {T : set (set β)} {f : α → β} (H : ∀ (t : set β), t ∈ T → set.maps_to f s t) :
set.maps_to f s (⋂₀ T)
source
theorem set.maps_to_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.maps_to f s (t i)) :
set.maps_to f s (⋂ (i : ι), t i)
source
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), set.maps_to f s (t i j)) :
set.maps_to f s (⋂ (i : ι) (j : κ i), t i j)
source
theorem set.maps_to_Inter_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.maps_to f (s i) (t i)) :
set.maps_to f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
source
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), set.maps_to f (s i j) (t i j)) :
set.maps_to f (⋂ (i : ι) (j : κ i), s i j) (⋂ (i : ι) (j : κ i), t i j)
source
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
source
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
source
theorem set.image_sInter_subset {α : Type u_1} {β : Type u_2} (S : set (set α)) (f : α → β) :
f '' ⋂₀ S ⊆ ⋂ (s : set α) (H : s ∈ S), f '' s

inj_on #

source
theorem set.inj_on.image_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s t u : set α} (hf : set.inj_on f u) (hs : s ⊆ u) (ht : t ⊆ u) :
f '' (s ∩ t) = f '' s ∩ f '' t
source
theorem set.inj_on.image_Inter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {s : ι → set α} {f : α → β} (h : set.inj_on f (⋃ (i : ι), s i)) :
(f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
source
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 : 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
source
theorem set.inj_on_Union_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} (hs : directed has_subset.subset s) {f : α → β} (hf : ∀ (i : ι), set.inj_on f (s i)) :
set.inj_on f (⋃ (i : ι), s i)

surj_on #

source
theorem set.surj_on_sUnion {α : Type u_1} {β : Type u_2} {s : set α} {T : set (set β)} {f : α → β} (H : ∀ (t : set β), t ∈ T → set.surj_on f s t) :
set.surj_on f s (⋃₀T)
source
theorem set.surj_on_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.surj_on f s (t i)) :
set.surj_on f s (⋃ (i : ι), t i)
source
theorem set.surj_on_Union_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.surj_on f (s i) (t i)) :
set.surj_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
source
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), set.surj_on f s (t i j)) :
set.surj_on f s (⋃ (i : ι) (j : κ i), t i j)
source
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), set.surj_on f (s i j) (t i j)) :
set.surj_on f (⋃ (i : ι) (j : κ i), s i j) (⋃ (i : ι) (j : κ i), t i j)
source
theorem set.surj_on_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι → set α} {t : set β} {f : α → β} (H : ∀ (i : ι), set.surj_on f (s i) t) (Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.surj_on f (⋂ (i : ι), s i) t
source
theorem set.surj_on_Inter_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.surj_on f (s i) (t i)) (Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.surj_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

bij_on #

source
theorem set.bij_on_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.bij_on f (s i) (t i)) (Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
source
theorem set.bij_on_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : nonempty ι] {s : ι → set α} {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.bij_on f (s i) (t i)) (Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
source
theorem set.bij_on_Union_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → set α} (hs : directed has_subset.subset s) {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.bij_on f (s i) (t i)) :
set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
source
theorem set.bij_on_Inter_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [nonempty ι] {s : ι → set α} (hs : directed has_subset.subset s) {t : ι → set β} {f : α → β} (H : ∀ (i : ι), set.bij_on f (s i) (t i)) :
set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

image, preimage #

source
theorem set.image_Union {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → set α} :
(f '' ⋃ (i : ι), s i) = ⋃ (i : ι), f '' s i
source
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
source
theorem set.univ_subtype {α : Type u_1} {p : α → Prop} :
set.univ = ⋃ (x : α) (h : p x), {⟨x, h⟩}
source
theorem set.range_eq_Union {α : Type u_1} {ι : Sort u_2} (f : ι → α) :
set.range f = ⋃ (i : ι), {f i}
source
theorem set.image_eq_Union {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
f '' s = ⋃ (i : α) (H : i ∈ s), {f i}
source
theorem set.bUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → set β} :
(⋃ (x : α) (H : x ∈ set.range f), g x) = ⋃ (y : ι), g (f y)
source
@[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)
source
theorem set.bInter_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → set β} :
(⋂ (x : α) (H : x ∈ set.range f), g x) = ⋂ (y : ι), g (f y)
source
@[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)
source
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)
source
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)
source
theorem set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : α → β} :
monotone (set.preimage f)
source
@[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
source
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
source
@[simp]
theorem set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : set (set β)} :
f ⁻¹' ⋃₀s = ⋃ (t : set β) (H : t ∈ s), f ⁻¹' t
source
theorem set.preimage_Inter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → set β} :
(f ⁻¹' ⋂ (i : ι), s i) = ⋂ (i : ι), f ⁻¹' s i
source
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
source
@[simp]
theorem set.preimage_sInter {α : Type u_1} {β : Type u_2} {f : α → β} {s : set (set β)} :
f ⁻¹' ⋂₀ s = ⋂ (t : set β) (H : t ∈ s), f ⁻¹' t
source
@[simp]
theorem set.bUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
(⋃ (y : β) (H : y ∈ s), f ⁻¹' {y}) = f ⁻¹' s
source
theorem set.bUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) :
(⋃ (y : β) (H : y ∈ set.range f), f ⁻¹' {y}) = set.univ
source
theorem set.monotone_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] {f : α → set β} {g : α → set γ} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : α), f x ×ˢ g x)
source
theorem monotone.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] {f : α → set β} {g : α → set γ} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : α), f x ×ˢ g x)

Alias of monotone_prod.

source
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
source
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
source
theorem set.prod_sUnion {α : Type u_1} {β : Type u_2} {s : set α} {C : set (set β)} :
s ×ˢ ⋃₀C = ⋃₀((λ (t : set β), s ×ˢ t) '' C)
source
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
source
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
source
theorem set.sUnion_prod_const {α : Type u_1} {β : Type u_2} {C : set (set α)} {t : set β} :
⋃₀C ×ˢ t = ⋃₀((λ (s : set α), s ×ˢ t) '' C)
source
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
source
theorem set.Union_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [semilattice_sup α] {s : α → set β} {t : α → set γ} (hs : monotone s) (ht : monotone t) :
(⋃ (x : α), s x ×ˢ t x) = (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
source
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) = set.image2 f s t
source
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) = set.image2 f s t
source
theorem set.image2_Union_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → set α) (t : set β) :
set.image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), set.image2 f (s i) t
source
theorem set.image2_Union_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : set α) (t : ι → set β) :
set.image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), set.image2 f s (t i)
source
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 β) :
set.image2 f (⋃ (i : ι) (j : κ i), s i j) t = ⋃ (i : ι) (j : κ i), set.image2 f (s i j) t
source
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 β) :
set.image2 f s (⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), set.image2 f s (t i j)
source
theorem set.image2_Inter_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → set α) (t : set β) :
set.image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), set.image2 f (s i) t
source
theorem set.image2_Inter_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : set α) (t : ι → set β) :
set.image2 f s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), set.image2 f s (t i)
source
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 β) :
set.image2 f (⋂ (i : ι) (j : κ i), s i j) t ⊆ ⋂ (i : ι) (j : κ i), set.image2 f (s i j) t
source
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 β) :
set.image2 f s (⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), set.image2 f s (t i j)
source
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
  • s.seq t = {b : β | ∃ (f : α → β) (H : f ∈ s) (a : α) (H : a ∈ t), f a = b}
source
theorem set.seq_def {α : Type u_1} {β : Type u_2} {s : set (α → β)} {t : set α} :
s.seq t = ⋃ (f : α → β) (H : f ∈ s), f '' t
source
@[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
source
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
source
theorem set.seq_mono {α : Type u_1} {β : Type u_2} {s₀ s₁ : set (α → β)} {t₀ t₁ : set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) :
s₀.seq t₀ ⊆ s₁.seq t₁
source
theorem set.singleton_seq {α : Type u_1} {β : Type u_2} {f : α → β} {t : set α} :
{f}.seq t = f '' t
source
theorem set.seq_singleton {α : Type u_1} {β : Type u_2} {s : set (α → β)} {a : α} :
s.seq {a} = (λ (f : α → β), f a) '' s
source
theorem set.seq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set (β → γ)} {t : set (α → β)} {u : set α} :
s.seq (t.seq u) = ((function.comp '' s).seq t).seq u
source
theorem set.image_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {s : set (α → β)} {t : set α} :
f '' s.seq t = (function.comp f '' s).seq t
source
theorem set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s ×ˢ t = (prod.mk '' s).seq t
source
theorem set.prod_image_seq_comm {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
(prod.mk '' s).seq t = ((λ (b : β) (a : α), (a, b)) '' t).seq s
source
theorem set.image2_eq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : set α) (t : set β) :
set.image2 f s t = (f '' s).seq t
source
theorem set.pi_def {α : Type u_1} {π : α → Type u_11} (i : set α) (s : Π (a : α), set (π a)) :
i.pi s = ⋂ (a : α) (H : a ∈ i), function.eval a ⁻¹' s a
source
theorem set.univ_pi_eq_Inter {α : Type u_1} {π : α → Type u_11} (t : Π (i : α), set (π i)) :
set.univ.pi t = ⋂ (i : α), function.eval i ⁻¹' t i
source
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), function.eval a ⁻¹' (s a \ t a)
source
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)
source
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
source
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.

source
theorem disjoint.union_left {α : Type u_1} {s t u : set α} (hs : disjoint s u) (ht : disjoint t u) :
disjoint (s ∪ t) u
source
theorem disjoint.union_right {α : Type u_1} {s t u : set α} (ht : disjoint s t) (hu : disjoint s u) :
disjoint s (t ∪ u)
source
theorem disjoint.inter_left {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint (s ∩ u) t
source
theorem disjoint.inter_left' {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint (u ∩ s) t
source
theorem disjoint.inter_right {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint s (t ∩ u)
source
theorem disjoint.inter_right' {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint s (u ∩ t)
source
theorem disjoint.subset_left_of_subset_union {α : Type u_1} {s t u : set α} (h : s ⊆ t ∪ u) (hac : disjoint s u) :
s ⊆ t
source
theorem disjoint.subset_right_of_subset_union {α : Type u_1} {s t u : set α} (h : s ⊆ t ∪ u) (hab : disjoint s t) :
s ⊆ u
source
theorem disjoint.preimage {α : Type u_1} {β : Type u_2} (f : α → β) {s t : set β} (h : disjoint s t) :
disjoint (f ⁻¹' s) (f ⁻¹' t)
source
@[protected]
theorem set.disjoint_iff {α : Type u_1} {s t : set α} :
disjoint s t ↔ s ∩ t ⊆ ∅
source
theorem set.disjoint_iff_inter_eq_empty {α : Type u_1} {s t : set α} :
disjoint s t ↔ s ∩ t = ∅
source
theorem set.not_disjoint_iff {α : Type u_1} {s t : set α} :
¬disjoint s t ↔ ∃ (x : α), x ∈ s ∧ x ∈ t
source
theorem set.not_disjoint_iff_nonempty_inter {α : Type u_1} {s t : set α} :
¬disjoint s t ↔ (s ∩ t).nonempty
source
theorem set.nonempty.not_disjoint {α : Type u_1} {s t : set α} :
(s ∩ t).nonempty → ¬disjoint s t

Alias of not_disjoint_iff_nonempty_inter.

source
theorem set.disjoint_or_nonempty_inter {α : Type u_1} (s t : set α) :
disjoint s t ∨ (s ∩ t).nonempty
source
theorem set.disjoint_left {α : Type u_1} {s t : set α} :
disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t
source
theorem set.disjoint_right {α : Type u_1} {s t : set α} :
disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s
source
theorem set.disjoint_iff_forall_ne {α : Type u_1} {s t : set α} :
disjoint s t ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x ≠ y
source
theorem disjoint.ne_of_mem {α : Type u_1} {s t : set α} (h : disjoint s t) {x y : α} (hx : x ∈ s) (hy : y ∈ t) :
x ≠ y
source
theorem set.disjoint_of_subset_left {α : Type u_1} {s t u : set α} (h : s ⊆ u) (d : disjoint u t) :
disjoint s t
source
theorem set.disjoint_of_subset_right {α : Type u_1} {s t u : set α} (h : t ⊆ u) (d : disjoint s u) :
disjoint s t
source
theorem set.disjoint_of_subset {α : Type u_1} {s t u v : set α} (h1 : s ⊆ u) (h2 : t ⊆ v) (d : disjoint u v) :
disjoint s t
source
@[simp]
theorem set.disjoint_union_left {α : Type u_1} {s t u : set α} :
disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u
source
@[simp]
theorem set.disjoint_union_right {α : Type u_1} {s t u : set α} :
disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u
source
@[simp]
theorem set.disjoint_Union_left {α : Type u_1} {t : set α} {ι : Sort u_2} {s : ι → set α} :
disjoint (⋃ (i : ι), s i) t ↔ ∀ (i : ι), disjoint (s i) t
source
@[simp]
theorem set.disjoint_Union_right {α : Type u_1} {t : set α} {ι : Sort u_2} {s : ι → set α} :
disjoint t (⋃ (i : ι), s i) ↔ ∀ (i : ι), disjoint t (s i)
source
theorem set.disjoint_diff {α : Type u_1} {a b : set α} :
disjoint a (b \ a)
source
@[simp]
theorem set.disjoint_empty {α : Type u_1} (s : set α) :
disjoint s ∅
source
@[simp]
theorem set.empty_disjoint {α : Type u_1} (s : set α) :
disjoint ∅ s
source
@[simp]
theorem set.univ_disjoint {α : Type u_1} {s : set α} :
disjoint set.univ s ↔ s = ∅
source
@[simp]
theorem set.disjoint_univ {α : Type u_1} {s : set α} :
disjoint s set.univ ↔ s = ∅
source
@[simp]
theorem set.disjoint_singleton_left {α : Type u_1} {a : α} {s : set α} :
disjoint {a} s ↔ a ∉ s
source
@[simp]
theorem set.disjoint_singleton_right {α : Type u_1} {a : α} {s : set α} :
disjoint s {a} ↔ a ∉ s
source
@[simp]
theorem set.disjoint_singleton {α : Type u_1} {a b : α} :
disjoint {a} {b} ↔ a ≠ b
source
theorem set.disjoint_image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α} {g : γ → α} {s : set β} {t : set γ} (h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c) :
disjoint (f '' s) (g '' t)
source
theorem set.disjoint_image_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {s t : set α} (hd : disjoint s t) :
disjoint (f '' s) (f '' t)
source
theorem set.disjoint_preimage {α : Type u_1} {β : Type u_2} {s t : set β} (hd : disjoint s t) (f : α → β) :
disjoint (f ⁻¹' s) (f ⁻¹' t)
source
theorem set.preimage_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} (h : disjoint s (set.range f)) :
f ⁻¹' s = ∅
source
theorem set.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :
disjoint s (set.range f) ↔ f ⁻¹' s = ∅
source
theorem set.disjoint_iff_subset_compl_right {α : Type u_1} {s t : set α} :
disjoint s t ↔ s ⊆ tᶜ
source
theorem set.disjoint_iff_subset_compl_left {α : Type u_1} {s t : set α} :
disjoint s t ↔ t ⊆ sᶜ
source
theorem disjoint.image {α : Type u_1} {β : Type u_2} {s t u : set α} {f : α → β} (h : disjoint s t) (hf : set.inj_on f u) (hs : s ⊆ u) (ht : t ⊆ u) :
disjoint (f '' s) (f '' t)

Intervals #

source
theorem set.Ici_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (f : ι → α) :
set.Ici (⨆ (i : ι), f i) = ⋂ (i : ι), set.Ici (f i)
source
theorem set.Iic_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (f : ι → α) :
set.Iic (⨅ (i : ι), f i) = ⋂ (i : ι), set.Iic (f i)
source
theorem set.Ici_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} [complete_lattice α] (f : Π (i : ι), κ i → α) :
set.Ici (⨆ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), set.Ici (f i j)
source
theorem set.Iic_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} [complete_lattice α] (f : Π (i : ι), κ i → α) :
set.Iic (⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), set.Iic (f i j)
source
theorem set.Ici_Sup {α : Type u_1} [complete_lattice α] (s : set α) :
set.Ici (Sup s) = ⋂ (a : α) (H : a ∈ s), set.Ici a
source
theorem set.Iic_Inf {α : Type u_1} [complete_lattice α] (s : set α) :
set.Iic (Inf s) = ⋂ (a : α) (H : a ∈ s), set.Iic a
source
theorem set.subset_diff {α : Type u_1} {s t u : set α} :
s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u
source
theorem set.bUnion_diff_bUnion_subset {α : Type u_1} {β : Type u_2} (t : α → set β) (s₁ s₂ : set α) :
((⋃ (x : α) (H : x ∈ s₁), t x) \ ⋃ (x : α) (H : x ∈ s₂), t x) ⊆ ⋃ (x : α) (H : x ∈ s₁ \ s₂), t x
source
def set.sigma_to_Union {α : Type u_1} {β : Type u_2} (t : α → set β) (x : Σ (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
source
theorem set.sigma_to_Union_surjective {α : Type u_1} {β : Type u_2} (t : α → set β) :
function.surjective (set.sigma_to_Union t)
source
theorem set.sigma_to_Union_injective {α : Type u_1} {β : Type u_2} (t : α → set β) (h : ∀ (i j : α), i ≠ j → disjoint (t i) (t j)) :
function.injective (set.sigma_to_Union t)
source
theorem set.sigma_to_Union_bijective {α : Type u_1} {β : Type u_2} (t : α → set β) (h : ∀ (i j : α), i ≠ j → disjoint (t i) (t j)) :
function.bijective (set.sigma_to_Union t)
source
noncomputable def set.Union_eq_sigma_of_disjoint {α : Type u_1} {β : Type u_2} {t : α → set β} (h : ∀ (i j : α), i ≠ j → disjoint (t i) (t j)) :
(↥⋃ (i : α), t i) ≃ Σ (i : α), ↥(t i)

Equivalence between a disjoint union and a dependent sum.

Equations