mathlib docs: data.set.lattice

source

@[instance]

def set.lattice_set {α : Type u} :

complete_lattice (set α)

Equations

set.lattice_set = {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 := _, top := boolean_algebra.top set.boolean_algebra, le_top := _, bot := boolean_algebra.bot set.boolean_algebra, bot_le := _, Sup := λ (s : set (set α)), {a : α | ∃ (t : set α) (H : t ∈ s), a ∈ t}, Inf := λ (s : set (set α)), {a : α | ∀ (t : set α), t ∈ s → a ∈ t}, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

source

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

monotone (set.image f)

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

source

theorem set.monotone_inter {α : Type u} {β : Type v} [preorder β] {f g : β → set α} :

monotone f → monotone g → monotone (λ (x : β), f x ∩ g x)

source

theorem set.monotone_union {α : Type u} {β : Type v} [preorder β] {f g : β → set α} :

monotone f → monotone g → monotone (λ (x : β), f x ∪ g x)

source

theorem set.monotone_set_of {α : Type u} {β : Type v} [preorder α] {p : α → β → Prop} :

(∀ (b : β), monotone (λ (a : α), p a b)) → monotone (λ (a : α), {b : β | p a b})

source

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

galois_connection (set.image f) (set.preimage f)

source

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

(α → β) → set α → set β

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

Equations

set.kern_image f s = {y : β | ∀ ⦃x : α⦄, f x = y → x ∈ s}

source

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

galois_connection (set.preimage f) (set.kern_image f)

source

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

(ι → set β) → set β

Indexed union of a family of sets

Equations

set.Union s = supr s

source

def set.Inter {β : Type v} {ι : Sort x} :

(ι → set β) → set β

Indexed intersection of a family of sets

Equations

set.Inter s = infi s

source

@[simp]

theorem set.mem_Union {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :

x ∈ set.Union s ↔ ∃ (i : ι), x ∈ s i

source

theorem set.set_of_exists {β : Type v} {ι : Sort x} (p : ι → β → Prop) :

{x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}

source

@[simp]

theorem set.mem_Inter {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :

x ∈ set.Inter s ↔ ∀ (i : ι), x ∈ s i

source

theorem set.set_of_forall {β : Type v} {ι : Sort x} (p : ι → β → Prop) :

{x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}

source

theorem set.Union_subset {β : Type v} {ι : Sort x} {s : ι → set β} {t : set β} :

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

source

theorem set.Union_subset_iff {β : Type v} {ι : Sort x} {s : ι → set β} {t : set β} :

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

source

theorem set.mem_Inter_of_mem {β : Type v} {ι : Sort x} {x : β} {s : ι → set β} :

(∀ (i : ι), x ∈ s i) → (x ∈ ⋂ (i : ι), s i)

source

theorem set.subset_Inter {β : Type v} {ι : Sort x} {t : set β} {s : ι → set β} :

(∀ (i : ι), t ⊆ s i) → (t ⊆ ⋂ (i : ι), s i)

source

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

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

source

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

A ⊆ s i → (A ⊆ ⋃ (i : ι), s i)

source

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

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

source

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

s i ⊆ t → (⋂ (i : ι), s i) ⊆ t

source

theorem set.Inter_subset_Inter {α : Type u} {ι : Sort x} {s t : ι → set α} :

(∀ (i : ι), s i ⊆ t i) → ((⋂ (i : ι), s i) ⊆ ⋂ (i : ι), t i)

source

theorem set.Inter_subset_Inter2 {α : Type u} {ι : Sort x} {ι' : Sort y} {s : ι → set α} {t : ι' → set α} :

(∀ (j : ι'), ∃ (i : ι), s i ⊆ t j) → ((⋂ (i : ι), s i) ⊆ ⋂ (j : ι'), t j)

source

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

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

source

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

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

source

@[simp]

theorem set.compl_Union {β : Type v} {ι : Sort x} (s : ι → set β) :

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

source

theorem set.compl_Inter {β : Type v} {ι : Sort x} (s : ι → set β) :

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

source

theorem set.Union_eq_comp_Inter_comp {β : Type v} {ι : Sort x} (s : ι → set β) :

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

source

theorem set.Inter_eq_comp_Union_comp {β : Type v} {ι : Sort x} (s : ι → set β) :

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

source

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

(s ∩ ⋃ (i : ι), t i) = ⋃ (i : ι), s ∩ t i

source

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

(⋃ (i : ι), t i) ∩ s = ⋃ (i : ι), t i ∩ s

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem set.Union_diff {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :

(⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s

source

theorem set.diff_Union {β : Type v} {ι : Sort x} [nonempty ι] (s : set β) (t : ι → set β) :

(s \ ⋃ (i : ι), t i) = ⋂ (i : ι), s \ t i

source

theorem set.diff_Inter {β : Type v} {ι : Sort x} (s : set β) (t : ι → set β) :

(s \ ⋂ (i : ι), t i) = ⋃ (i : ι), s \ t i

source

theorem set.directed_on_Union {α : Type u} {r : α → α → Prop} {ι : Sort v} {f : ι → set α} :

directed has_subset.subset f → (∀ (x : ι), directed_on r (f x)) → directed_on r (⋃ (x : ι), f x)

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 : β} :

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

source

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

(∀ (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 β} :

(∀ (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 β} :

(∀ (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 : α} :

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 : α} :

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 β} :

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 β} :

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 β} :

(∀ (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 β} :

(∀ (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 β} :

(∀ (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 β} :

s ⊆ s' → (∀ (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 β} :

(∀ (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 β} :

(∀ (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 ∈ has_insert.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 ∈ has_insert.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} :

set (set α) → set α

Intersection of a set of sets.

Equations

⋂₀S = has_Inf.Inf S

source

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

x ∈ t → 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 α)} :

x ∉ ⋃₀S → 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 α} :

t ∈ S → ⋂₀S ⊆ t

source

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

t ∈ S → t ⊆ ⋃₀S

source

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

s ⊆ u → u ∈ t → s ⊆ ⋃₀t

source

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

(∀ (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 α} :

(∀ (t' : set α), t' ∈ S → t ⊆ t') → t ⊆ ⋂₀S

source

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

S ⊆ T → ⋃₀S ⊆ ⋃₀T

source

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

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 α)) :

⋃₀has_insert.insert s T = s ∪ ⋃₀T

source

@[simp]

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

⋂₀has_insert.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)ᶜ = ⋂₀(has_compl.compl '' S)

source

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

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

source

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

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

source

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

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

source

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

t ∈ S → 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 α)} :

s ⊆ t → ⋃₀s ⊆ ⋃₀t

source

theorem set.Union_subset_Union {α : Type u} {ι : Sort x} {s t : ι → set α} :

(∀ (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 α} :

(∀ (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 α} :

(ι → ι₂) → ((⋃ (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 := has_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 α)} :

(∀ (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 α)} :

(∀ (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} :

(∀ (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)} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

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 : α → β} :

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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (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 : α → β} :

(∀ (i : ι), set.surj_on f (s i) t) → 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 : α → β} :

(∀ (i : ι), set.surj_on f (s i) (t i)) → set.inj_on f (⋃ (i : ι), s i) → set.surj_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

source

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

(∀ (i : ι), set.bij_on f (s i) (t i)) → set.inj_on f (⋃ (i : ι), s i) → set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

source

theorem set.bij_on_Inter {α : Type u} {β : Type v} {ι : Sort x} [hi : nonempty ι] {s : ι → set α} {t : ι → set β} {f : α → β} :

(∀ (i : ι), set.bij_on f (s i) (t i)) → set.inj_on f (⋃ (i : ι), s i) → set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

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 : α → β} :

(∀ (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 : α → β} :

(∀ (i : ι), set.bij_on f (s i) (t i)) → set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

source

@[simp]