mathlib docs: data.set.lattice

theorem set.directed_on_Union {α : Type u} {r : α → α → Prop} {ι : Sort v} {f : ι → set α} (hd : directed has_subset.subset f) (h : ∀ (x : ι), directed_on r (f x)) :

directed_on r (⋃ (x : ι), f x)

source

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

source

theorem set.mem_bInter_iff {α : Type u} {β : Type v} {s : set α} {t : α → set β} {y : β} :

(y ∈ ⋂ (x : α) (H : x ∈ s), t x) ↔ ∀ (x : α), x ∈ s → y ∈ t x

source

theorem set.mem_bUnion {α : Type u} {β : Type v} {s : set α} {t : α → set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) :

y ∈ ⋃ (x : α) (H : x ∈ s), t x

source

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

y ∈ ⋂ (x : α) (H : x ∈ s), t x

source

theorem set.bUnion_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {u : α → set β} (h : ∀ (x : α), x ∈ s → u x ⊆ t) :

(⋃ (x : α) (H : x ∈ s), u x) ⊆ t

source

theorem set.subset_bInter {α : Type u} {β : Type v} {s : set α} {t : set β} {u : α → set β} (h : ∀ (x : α), x ∈ s → t ⊆ u x) :

t ⊆ ⋂ (x : α) (H : x ∈ s), u x

source

theorem set.subset_bUnion_of_mem {α : Type u} {β : Type v} {s : set α} {u : α → set β} {x : α} (xs : x ∈ s) :

u x ⊆ ⋃ (x : α) (H : x ∈ s), u x

source

theorem set.bInter_subset_of_mem {α : Type u} {β : Type v} {s : set α} {t : α → set β} {x : α} (xs : x ∈ s) :

(⋂ (x : α) (H : x ∈ s), t x) ⊆ t x

source

theorem set.bUnion_subset_bUnion_left {α : Type u} {β : Type v} {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} {β : Type v} {s s' : set α} {t : α → set β} (h : s' ⊆ s) :

(⋂ (x : α) (H : x ∈ s), t x) ⊆ ⋂ (x : α) (H : x ∈ s'), t x

source

theorem set.bUnion_subset_bUnion_right {α : Type u} {β : Type v} {s : set α} {t1 t2 : α → set β} (h : ∀ (x : α), x ∈ s → t1 x ⊆ t2 x) :

(⋃ (x : α) (H : x ∈ s), t1 x) ⊆ ⋃ (x : α) (H : x ∈ s), t2 x

source

theorem set.bInter_subset_bInter_right {α : Type u} {β : Type v} {s : set α} {t1 t2 : α → set β} (h : ∀ (x : α), x ∈ s → t1 x ⊆ t2 x) :

(⋂ (x : α) (H : x ∈ s), t1 x) ⊆ ⋂ (x : α) (H : x ∈ s), t2 x

source

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

(⋃ (x : α) (H : x ∈ s), t x) ⊆ ⋃ (y : γ) (H : y ∈ s'), t' y

source

theorem set.bInter_mono' {α : Type u} {β : Type v} {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} {β : Type v} {s : set α} {t t' : α → set β} (h : ∀ (x : α), x ∈ s → t x ⊆ t' x) :

(⋂ (x : α) (H : x ∈ s), t x) ⊆ ⋂ (x : α) (H : x ∈ s), t' x

source

theorem set.bUnion_mono {α : Type u} {β : Type v} {s : set α} {t t' : α → set β} (h : ∀ (x : α), x ∈ s → t x ⊆ t' x) :

(⋃ (x : α) (H : x ∈ s), t x) ⊆ ⋃ (x : α) (H : x ∈ s), t' x

source

theorem set.bUnion_eq_Union {α : Type u} {β : Type v} (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} {β : Type v} (s : set α) (t : Π (x : α), x ∈ s → set β) :

(⋂ (x : α) (H : x ∈ s), t x H) = ⋂ (x : ↥s), t ↑x _

source

theorem set.bInter_empty {α : Type u} {β : Type v} (u : α → set β) :

(⋂ (x : α) (H : x ∈ ∅), u x) = set.univ

source

theorem set.bInter_univ {α : Type u} {β : Type v} (u : α → set β) :

(⋂ (x : α) (H : x ∈ set.univ), u x) = ⋂ (x : α), u x

source

@[simp]

theorem set.bInter_singleton {α : Type u} {β : Type v} (a : α) (s : α → set β) :

(⋂ (x : α) (H : x ∈ {a}), s x) = s a

source

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

source

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

source

theorem set.bInter_pair {α : Type u} {β : Type v} (a b : α) (s : α → set β) :

(⋂ (x : α) (H : x ∈ {a, b}), s x) = s a ∩ s b

source

theorem set.bUnion_empty {α : Type u} {β : Type v} (s : α → set β) :

(⋃ (x : α) (H : x ∈ ∅), s x) = ∅

source

theorem set.bUnion_univ {α : Type u} {β : Type v} (s : α → set β) :

(⋃ (x : α) (H : x ∈ set.univ), s x) = ⋃ (x : α), s x

source

@[simp]

theorem set.bUnion_singleton {α : Type u} {β : Type v} (a : α) (s : α → set β) :

(⋃ (x : α) (H : x ∈ {a}), s x) = s a

source

@[simp]

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

(⋃ (x : α) (H : x ∈ s), {x}) = s

source

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

source

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

source

theorem set.bUnion_pair {α : Type u} {β : Type v} (a b : α) (s : α → set β) :

(⋃ (x : α) (H : x ∈ {a, b}), s x) = s a ∪ s b

source

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

source

theorem set.compl_bInter {α : Type u} {β : Type v} (s : set α) (t : α → set β) :

(⋂ (i : α) (H : i ∈ s), t i)ᶜ = ⋃ (i : α) (H : i ∈ s), (t i)ᶜ

source

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

source

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

source

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

set α

Intersection of a set of sets.

Equations

⋂₀S = Inf S

source

theorem set.mem_sUnion_of_mem {α : Type u} {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :

x ∈ ⋃₀S

source

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

x ∈ ⋃₀S ↔ ∃ (t : set α) (H : t ∈ S), x ∈ t

source

theorem set.not_mem_of_not_mem_sUnion {α : Type u} {x : α} {t : set α} {S : set (set α)} (hx : x ∉ ⋃₀S) (ht : t ∈ S) :

x ∉ t

source

@[simp]

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

x ∈ ⋂₀S ↔ ∀ (t : set α), t ∈ S → x ∈ t

source

theorem set.sInter_subset_of_mem {α : Type u} {S : set (set α)} {t : set α} (tS : t ∈ S) :

⋂₀S ⊆ t

source

theorem set.subset_sUnion_of_mem {α : Type u} {S : set (set α)} {t : set α} (tS : t ∈ S) :

t ⊆ ⋃₀S

source

theorem set.subset_sUnion_of_subset {α : Type u} {s : set α} (t : set (set α)) (u : set α) (h₁ : s ⊆ u) (h₂ : u ∈ t) :

s ⊆ ⋃₀t

source

theorem set.sUnion_subset {α : Type u} {S : set (set α)} {t : set α} (h : ∀ (t' : set α), t' ∈ S → t' ⊆ t) :

⋃₀S ⊆ t

source

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

⋃₀s ⊆ t ↔ ∀ (t' : set α), t' ∈ s → t' ⊆ t

source

theorem set.subset_sInter {α : Type u} {S : set (set α)} {t : set α} (h : ∀ (t' : set α), t' ∈ S → t ⊆ t') :

t ⊆ ⋂₀S

source

theorem set.sUnion_subset_sUnion {α : Type u} {S T : set (set α)} (h : S ⊆ T) :

⋃₀S ⊆ ⋃₀T

source

theorem set.sInter_subset_sInter {α : Type u} {S T : set (set α)} (h : S ⊆ T) :

⋂₀T ⊆ ⋂₀S

source

@[simp]

theorem set.sUnion_empty {α : Type u} :

⋃₀ ∅ = ∅

source

@[simp]

theorem set.sInter_empty {α : Type u} :

⋂₀ ∅ = set.univ

source

@[simp]

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

⋃₀{s} = s

source

@[simp]

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

⋂₀{s} = s

source

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

⋃₀(S ∪ T) = ⋃₀S ∪ ⋃₀T

source

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

⋂₀(S ∪ T) = ⋂₀S ∩ ⋂₀T

source

theorem set.sInter_Union {α : Type u} {ι : Sort x} (s : ι → set (set α)) :

(⋂₀⋃ (i : ι), s i) = ⋂ (i : ι), ⋂₀s i

source

@[simp]

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

⋃₀insert s T = s ∪ ⋃₀T

source

@[simp]

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

⋂₀insert s T = s ∩ ⋂₀T

source

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

⋃₀{s, t} = s ∪ t

source

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

⋂₀{s, t} = s ∩ t

source

@[simp]

theorem set.sUnion_image {α : Type u} {β : Type v} (f : α → set β) (s : set α) :

⋃₀(f '' s) = ⋃ (x : α) (H : x ∈ s), f x

source

@[simp]

theorem set.sInter_image {α : Type u} {β : Type v} (f : α → set β) (s : set α) :

⋂₀(f '' s) = ⋂ (x : α) (H : x ∈ s), f x

source

@[simp]

theorem set.sUnion_range {β : Type v} {ι : Sort x} (f : ι → set β) :

⋃₀set.range f = ⋃ (x : ι), f x

source

@[simp]

theorem set.sInter_range {β : Type v} {ι : Sort x} (f : ι → set β) :

⋂₀set.range f = ⋂ (x : ι), f x

source

theorem set.sUnion_eq_univ_iff {α : Type u} {c : set (set α)} :

⋃₀c = set.univ ↔ ∀ (a : α), ∃ (b : set α) (H : b ∈ c), a ∈ b

source

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

(⋃₀S)ᶜ = ⋂₀(compl '' S)

source

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

⋃₀S = (⋂₀(compl '' S))ᶜ

source

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

(⋂₀S)ᶜ = ⋃₀(compl '' S)

source

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

⋂₀S = (⋃₀(compl '' S))ᶜ

source

theorem set.inter_empty_of_inter_sUnion_empty {α : Type u} {s t : set α} {S : set (set α)} (hs : t ∈ S) (h : s ∩ ⋃₀S = ∅) :

s ∩ t = ∅

source

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

source

theorem set.Union_eq_range_sigma {α : Type u} {β : Type v} (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.sUnion_mono {α : Type u} {s t : set (set α)} (h : s ⊆ t) :

⋃₀s ⊆ ⋃₀t

source

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

(⋃ (i : ι), s i) ⊆ ⋃ (i : ι), t i

source

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

(⋃ (i : ι), s i) ⊆ ⋃ (i : ι₂), t i

source

theorem set.Union_subset_Union_const {α : Type u} {ι ι₂ : Sort x} {s : set α} (h : ι → ι₂) :

(⋃ (i : ι), s) ⊆ ⋃ (j : ι₂), s

source

@[simp]

theorem set.Union_of_singleton (α : Type u) :

(⋃ (x : α), {x}) = set.univ

source

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

(⋃ (x : α) (H : x ∈ s), t x) ⊆ ⋃ (x : α), t x

source

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

⋃₀s = ⋃ (i : set α) (h : i ∈ s), i

source

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

⋂₀s = ⋂ (i : set α) (h : i ∈ s), i

source

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

⋃₀s = ⋃ (i : ↥s), ↑i

source

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

⋂₀s = ⋂ (i : ↥s), ↑i

source

theorem set.union_eq_Union {α : Type u} {s₁ s₂ : set α} :

s₁ ∪ s₂ = ⋃ (b : bool), cond b s₁ s₂

source

theorem set.inter_eq_Inter {α : Type u} {s₁ s₂ : set α} :

s₁ ∩ s₂ = ⋂ (b : bool), cond b s₁ s₂

source

@[instance]

def set.complete_boolean_algebra {α : Type u} :

complete_boolean_algebra (set α)

Equations

set.complete_boolean_algebra = {sup := boolean_algebra.sup set.boolean_algebra, le := boolean_algebra.le set.boolean_algebra, lt := boolean_algebra.lt set.boolean_algebra, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := boolean_algebra.inf set.boolean_algebra, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := boolean_algebra.top set.boolean_algebra, le_top := _, bot := boolean_algebra.bot set.boolean_algebra, bot_le := _, compl := compl (boolean_algebra.to_has_compl (set α)), sdiff := has_sdiff.sdiff set.has_sdiff, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _, Sup := complete_lattice.Sup set.lattice_set, Inf := complete_lattice.Inf set.lattice_set, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, infi_sup_le_sup_Inf := _, inf_Sup_le_supr_inf := _}

source

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

source

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

source

theorem set.sInter_bUnion {α : Type u} {S : set (set α)} {T : Π (s : set α), s ∈ S → set (set α)} (hT : ∀ (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.

source

theorem set.sUnion_bUnion {α : Type u} {S : set (set α)} {T : Π (s : set α), s ∈ S → set (set α)} (hT : ∀ (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.

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} {β : Type u_3} (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_right {α : Type u} {ι : Type u_1} (s : ι → set α) (t : set α) :

(⋂ (i : ι), s i) ∪ t = ⋂ (i : ι), s i ∪ t

source

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

(t ∪ ⋂ (i : ι), s i) = ⋂ (i : ι), t ∪ s i

source

theorem set.maps_to_sUnion {α : Type u} {β : Type v} {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} {β : Type v} {ι : Sort x} {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_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p i → set α} {t : set β} {f : α → β} (H : ∀ (i : ι) (hi : p i), set.maps_to f (s i hi) t) :

set.maps_to f (⋃ (i : ι) (hi : p i), s i hi) t

source

theorem set.maps_to_Union_Union {α : Type u} {β : Type v} {ι : Sort x} {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_bUnion_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p i → set α} {t : Π (i : ι), p i → set β} {f : α → β} (H : ∀ (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)

source

theorem set.maps_to_sInter {α : Type u} {β : Type v} {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} {β : Type v} {ι : Sort x} {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_bInter {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : set α} {t : Π (i : ι), p i → set β} {f : α → β} (H : ∀ (i : ι) (hi : p i), set.maps_to f s (t i hi)) :

set.maps_to f s (⋂ (i : ι) (hi : p i), t i hi)

source

theorem set.maps_to_Inter_Inter {α : Type u} {β : Type v} {ι : Sort x} {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_bInter_bInter {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p i → set α} {t : Π (i : ι), p i → set β} {f : α → β} (H : ∀ (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)

source

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

(f '' ⋂ (i : ι), s i) ⊆ ⋂ (i : ι), f '' s i

source

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

(f '' ⋂ (i : ι) (hi : p i), s i hi) ⊆ ⋂ (i : ι) (hi : p i), f '' s i hi

source

theorem set.image_sInter_subset {α : Type u} {β : Type v} (S : set (set α)) (f : α → β) :

f '' ⋂₀S ⊆ ⋂ (s : set α) (H : s ∈ S), f '' s

source

theorem set.inj_on.image_Inter_eq {α : Type u} {β : Type v} {ι : Sort x} [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} {β : Type v} {ι : Sort x} {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} {β : Type v} {ι : Sort x} {s : ι → set α} (hs : directed has_subset.subset s) {f : α → β} (hf : ∀ (i : ι), set.inj_on f (s i)) :

set.inj_on f (⋃ (i : ι), s i)

source

theorem set.surj_on_sUnion {α : Type u} {β : Type v} {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} {β : Type v} {ι : Sort x} {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} {β : Type v} {ι : Sort x} {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_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : set α} {t : Π (i : ι), p i → set β} {f : α → β} (H : ∀ (i : ι) (hi : p i), set.surj_on f s (t i hi)) :

set.surj_on f s (⋃ (i : ι) (hi : p i), t i hi)

source

theorem set.surj_on_bUnion_bUnion {α : Type u} {β : Type v} {ι : Sort x} {p : ι → Prop} {s : Π (i : ι), p i → set α} {t : Π (i : ι), p i → set β} {f : α → β} (H : ∀ (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)

source

theorem set.surj_on_Inter {α : Type u} {β : Type v} {ι : Sort x} [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} {β : Type v} {ι : Sort x} [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)

source

theorem set.bij_on_Union {α : Type u} {β : Type v} {ι : Sort x} {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} {β : Type v} {ι : Sort x} [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} {β : Type v} {ι : Sort x} {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} {β : Type v} {ι : Sort x} [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)

source

@[simp]

theorem set.Inter_pos {α : Type u} {p : Prop} {μ : p → set α} (hp : p) :

(⋂ (h : p), μ h) = μ hp

source

@[simp]

theorem set.Inter_neg {α : Type u} {p : Prop} {μ : p → set α} (hp : ¬p) :

(⋂ (h : p), μ h) = set.univ

source

@[simp]

theorem set.Union_pos {α : Type u} {p : Prop} {μ : p → set α} (hp : p) :

(⋃ (h : p), μ h) = μ hp

source

@[simp]

theorem set.Union_neg {α : Type u} {p : Prop} {μ : p → set α} (hp : ¬p) :

(⋃ (h : p), μ h) = ∅

source

@[simp]

theorem set.Union_empty {α : Type u} {ι : Sort u_1} :

(⋃ (i : ι), ∅) = ∅

source

@[simp]

theorem set.Inter_univ {α : Type u} {ι : Sort u_1} :

(⋂ (i : ι), set.univ) = set.univ

source

theorem set.image_Union {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {s : ι → set α} :

(f '' ⋃ (i : ι), s i) = ⋃ (i : ι), f '' s i

source

theorem set.univ_subtype {α : Type u} {p : α → Prop} :

set.univ = ⋃ (x : α) (h : p x), {⟨x, h⟩}

source

theorem set.range_eq_Union {α : Type u} {ι : Sort u_1} (f : ι → α) :

set.range f = ⋃ (i : ι), {f i}

source

theorem set.image_eq_Union {α : Type u} {β : Type v} (f : α → β) (s : set α) :

f '' s = ⋃ (i : α) (H : i ∈ s), {f i}

source

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

source

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

source

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

source

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

source

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

source

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

source

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

monotone (set.preimage f)

source

@[simp]

theorem set.preimage_Union {α : Type u} {β : Type v} {ι : Sort w} {f : α → β} {s : ι → set β} :

(f ⁻¹' ⋃ (i : ι), s i) = ⋃ (i : ι), f ⁻¹' s i

source

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

source

@[simp]

theorem set.preimage_sUnion {α : Type u} {β : Type v} {f : α → β} {s : set (set β)} :

f ⁻¹' ⋃₀s = ⋃ (t : set β) (H : t ∈ s), f ⁻¹' t

source

theorem set.preimage_Inter {α : Type u} {β : Type v} {ι : Sort u_1} {s : ι → set β} {f : α → β} :

(f ⁻¹' ⋂ (i : ι), s i) = ⋂ (i : ι), f ⁻¹' s i

source

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

source

@[simp]

theorem set.bUnion_preimage_singleton {α : Type u} {β : Type v} (f : α → β) (s : set β) :

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

source

theorem set.bUnion_range_preimage_singleton {α : Type u} {β : Type v} (f : α → β) :

(⋃ (y : β) (H : y ∈ set.range f), f ⁻¹' {y}) = set.univ

source

theorem set.monotone_prod {α : Type u} {β : Type v} {γ : Type w} [preorder α] {f : α → set β} {g : α → set γ} (hf : monotone f) (hg : monotone g) :

monotone (λ (x : α), (f x).prod (g x))

source

theorem set.Union_prod_of_monotone {α : Type u} {β : Type v} {γ : Type w} [semilattice_sup α] {s : α → set β} {t : α → set γ} (hs : monotone s) (ht : monotone t) :

(⋃ (x : α), (s x).prod (t x)) = (⋃ (x : α), s x).prod (⋃ (x : α), t x)

source

def set.seq {α : Type u} {β : Type v} (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} {β : Type v} {s : set (α → β)} {t : set α} :

s.seq t = ⋃ (f : α → β) (H : f ∈ s), f '' t

source

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

source

theorem set.seq_subset {α : Type u} {β : Type v} {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} {β : Type v} {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} {β : Type v} {f : α → β} {t : set α} :

{f}.seq t = f '' t

source

theorem set.seq_singleton {α : Type u} {β : Type v} {s : set (α → β)} {a : α} :

s.seq {a} = (λ (f : α → β), f a) '' s

source

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

source

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

source

theorem set.prod_eq_seq {α : Type u} {β : Type v} {s : set α} {t : set β} :

s.prod t = (prod.mk '' s).seq t

source

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

source

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

source

@[instance]

def set.monad :

monad set

Equations

set.monad = monad.mk

source

@[simp]

theorem set.bind_def {α' β' : Type u} {s : set α'} {f : α' → set β'} :

s >>= f = ⋃ (i : α') (H : i ∈ s), f i

source

@[simp]

theorem set.fmap_eq_image {α' β' : Type u} {s : set α'} (f : α' → β') :

f <$> s = f '' s

source

@[simp]

theorem set.seq_eq_set_seq {α β : Type u_1} (s : set (α → β)) (t : set α) :

s <*> t = s.seq t

source

@[simp]

theorem set.pure_def {α : Type u} (a : α) :

pure a = {a}

source

@[instance]

def set.is_lawful_monad :

is_lawful_monad set

source

@[instance]

def set.is_comm_applicative :

is_comm_applicative set

source

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

source

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

disjoint (s ∪ t) u

source

theorem disjoint.union_right {α : Type u} {s t u : set α} (ht : disjoint s t) (hu : disjoint s u) :

disjoint s (t ∪ 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

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

disjoint s t ↔ s ∩ t ⊆ ∅

source

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

disjoint s t ↔ s ∩ t = ∅

source

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

¬disjoint s t ↔ ∃ (x : α), x ∈ s ∧ x ∈ t

source

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

disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t

source

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

disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s

source

theorem set.disjoint_of_subset_left {α : Type u} {s t u : set α} (h : s ⊆ u) (d : disjoint u t) :

disjoint s t

source

theorem set.disjoint_of_subset_right {α : Type u} {s t u : set α} (h : t ⊆ u) (d : disjoint s u) :

disjoint s t

source

theorem set.disjoint_of_subset {α : Type u} {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} {s t u : set α} :

disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u

source

@[simp]

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

disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u

source

theorem set.disjoint_diff {α : Type u} {a b : set α} :

disjoint a (b \ a)

source

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

disjoint sᶜ s

source

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

disjoint s sᶜ

source

@[simp]

theorem set.univ_disjoint {α : Type u} {s : set α} :

disjoint set.univ s ↔ s = ∅

source

@[simp]

theorem set.disjoint_univ {α : Type u} {s : set α} :

disjoint s set.univ ↔ s = ∅

source

@[simp]

theorem set.disjoint_singleton_left {α : Type u} {a : α} {s : set α} :

disjoint {a} s ↔ a ∉ s

source

@[simp]

theorem set.disjoint_singleton_right {α : Type u} {a : α} {s : set α} :

disjoint s {a} ↔ a ∉ s

source

theorem set.disjoint_image_image {α : Type u} {β : Type v} {γ : Type w} {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.pairwise_on_disjoint_fiber {α : Type u} {β : Type v} (f : α → β) (s : set β) :

s.pairwise_on (disjoint on λ (y : β), f ⁻¹' {y})

source

theorem set.preimage_eq_empty {α : Type u} {β : Type v} {f : α → β} {s : set β} (h : disjoint s (set.range f)) :

f ⁻¹' s = ∅

source

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

disjoint s (set.range f) ↔ f ⁻¹' s = ∅

source

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

Prop

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

Equations

s.pairwise_disjoint = s.pairwise_on disjoint

source

theorem set.pairwise_disjoint.subset {α : Type u} {s t : set (set α)} (h : s ⊆ t) (ht : t.pairwise_disjoint) :

s.pairwise_disjoint

source

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

(set.range f).pairwise_disjoint

source

theorem set.pairwise_disjoint.elim {α : Type u} {s : set (set α)} (h : s.pairwise_disjoint) {x y : set α} (hx : x ∈ s) (hy : y ∈ s) (z : α) (hzx : z ∈ x) (hzy : z ∈ y) :

x = y

source

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

s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u

source

def set.sigma_to_Union {α : Type u} {β : Type v} (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

set.sigma_to_Union t x = ⟨↑(x.snd), _⟩

source

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

function.surjective (set.sigma_to_Union t)

source

theorem set.sigma_to_Union_injective {α : Type u} {β : Type v} (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} {β : Type v} (t : α → set β) (h : ∀ (i j : α), i ≠ j → disjoint (t i) (t j)) :

function.bijective (set.sigma_to_Union t)

source

def set.Union_eq_sigma_of_disjoint {α : Type u} {β : Type v} {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

set.Union_eq_sigma_of_disjoint h = (equiv.of_bijective (set.sigma_to_Union t) _).symm

source

def set.bUnion_eq_sigma_of_disjoint {α : Type u} {β : Type v} {s : set α} {t : α → set β} (h : 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

set.bUnion_eq_sigma_of_disjoint h = (equiv.set_congr set.bUnion_eq_sigma_of_disjoint._proof_1).trans (set.Union_eq_sigma_of_disjoint _)

mathlib documentation

`maps_to`

`inj_on`

`surj_on`

`bij_on`