import order.complete_boolean_algebra

import order.directed

import order.galois_connection

open function tactic set

universes u

variables {α β γ : Type*} {ι ι' ι₂ : Sort*} {κ κ₁ κ₂ : ι → Sort*} {κ' : ι' → Sort*}

namespace set

instance : has_Inf (set α) := ⟨λ s, {a | ∀ t ∈ s, a ∈ t}⟩

instance : has_Sup (set α) := ⟨λ s, {a | ∃ t ∈ s, a ∈ t}⟩

def sInter (S : set (set α)) : set α := Inf S

def sUnion (S : set (set α)) : set α := Sup S

prefix `⋂₀ `:110 := sInter

prefix `⋃₀ `:110 := sUnion

@[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl

@[simp] theorem mem_sUnion {x : α} {S : set (set α)} : x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t := iff.rfl

def Union (s : ι → set β) : set β := supr s

def Inter (s : ι → set β) : set β := infi s

notation `⋃` binders `, ` r:(scoped f, Union f) := r

notation `⋂` binders `, ` r:(scoped f, Inter f) := r

@[simp] lemma Sup_eq_sUnion (S : set (set α)) : Sup S = ⋃₀ S := rfl

@[simp] lemma Inf_eq_sInter (S : set (set α)) : Inf S = ⋂₀ S := rfl

@[simp] lemma supr_eq_Union (s : ι → set α) : supr s = Union s := rfl

@[simp] lemma infi_eq_Inter (s : ι → set α) : infi s = Inter s := rfl

@[simp] lemma mem_Union {x : α} {s : ι → set α} : x ∈ (⋃ i, s i) ↔ ∃ i, x ∈ s i :=

⟨λ ⟨t, ⟨⟨a, (t_eq : s a = t)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq.symm ▸ h⟩,

λ ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩

@[simp] lemma mem_Inter {x : α} {s : ι → set α} : x ∈ (⋂ i, s i) ↔ ∀ i, x ∈ s i :=

⟨λ (h : ∀ a ∈ {a : set α | ∃ i, s i = a}, x ∈ a) a, h (s a) ⟨a, rfl⟩,

λ h t ⟨a, (eq : s a = t)⟩, eq ▸ h a⟩

lemma mem_Union₂ {x : γ} {s : Π i, κ i → set γ} : x ∈ (⋃ i j, s i j) ↔ ∃ i j, x ∈ s i j :=

by simp_rw mem_Union

lemma mem_Inter₂ {x : γ} {s : Π i, κ i → set γ} : x ∈ (⋂ i j, s i j) ↔ ∀ i j, x ∈ s i j :=

by simp_rw mem_Inter

lemma mem_Union_of_mem {s : ι → set α} {a : α} (i : ι) (ha : a ∈ s i) : a ∈ ⋃ i, s i :=

mem_Union.2 ⟨i, ha⟩

lemma mem_Union₂_of_mem {s : Π i, κ i → set α} {a : α} {i : ι} (j : κ i) (ha : a ∈ s i j) :

a ∈ ⋃ i j, s i j :=

mem_Union₂.2 ⟨i, j, ha⟩

lemma mem_Inter_of_mem {s : ι → set α} {a : α} (h : ∀ i, a ∈ s i) : a ∈ ⋂ i, s i := mem_Inter.2 h

lemma mem_Inter₂_of_mem {s : Π i, κ i → set α} {a : α} (h : ∀ i j, a ∈ s i j) : a ∈ ⋂ i j, s i j :=

mem_Inter₂.2 h

instance : complete_boolean_algebra (set α) :=

{ Sup := Sup,

Inf := Inf,

le_Sup := λ s t t_in a a_in, ⟨t, ⟨t_in, a_in⟩⟩,

Sup_le := λ s t h a ⟨t', ⟨t'_in, a_in⟩⟩, h t' t'_in a_in,

le_Inf := λ s t h a a_in t' t'_in, h t' t'_in a_in,

Inf_le := λ s t t_in a h, h _ t_in,

infi_sup_le_sup_Inf := λ s S x, iff.mp $ by simp [forall_or_distrib_left],

inf_Sup_le_supr_inf := λ s S x, iff.mp $ by simp [exists_and_distrib_left],

.. set.boolean_algebra }

section galois_connection

variables {f : α → β}

protected lemma image_preimage : galois_connection (image f) (preimage f) :=

λ a b, image_subset_iff

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

protected lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=

λ a b,

⟨ λ h x hx y hy, have f y ∈ a, from hy.symm ▸ hx, h this,

λ h x (hx : f x ∈ a), h hx rfl⟩

end galois_connection

instance : order_top (set α) :=

{ top := univ,

le_top := by simp }

@[congr] theorem Union_congr_Prop {p q : Prop} {f₁ : p → set α} {f₂ : q → set α}

(pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : Union f₁ = Union f₂ :=

supr_congr_Prop pq f

@[congr] theorem Inter_congr_Prop {p q : Prop} {f₁ : p → set α} {f₂ : q → set α}

(pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : Inter f₁ = Inter f₂ :=

infi_congr_Prop pq f

lemma Union_plift_up (f : plift ι → set α) : (⋃ i, f (plift.up i)) = ⋃ i, f i := supr_plift_up _

lemma Union_plift_down (f : ι → set α) : (⋃ i, f (plift.down i)) = ⋃ i, f i := supr_plift_down _

lemma Inter_plift_up (f : plift ι → set α) : (⋂ i, f (plift.up i)) = ⋂ i, f i := infi_plift_up _

lemma Inter_plift_down (f : ι → set α) : (⋂ i, f (plift.down i)) = ⋂ i, f i := infi_plift_down _

lemma Union_eq_if {p : Prop} [decidable p] (s : set α) :

(⋃ h : p, s) = if p then s else ∅ :=

supr_eq_if _

lemma Union_eq_dif {p : Prop} [decidable p] (s : p → set α) :

(⋃ (h : p), s h) = if h : p then s h else ∅ :=

supr_eq_dif _

lemma Inter_eq_if {p : Prop} [decidable p] (s : set α) :

(⋂ h : p, s) = if p then s else univ :=

infi_eq_if _

lemma Infi_eq_dif {p : Prop} [decidable p] (s : p → set α) :

(⋂ (h : p), s h) = if h : p then s h else univ :=

infi_eq_dif _

lemma exists_set_mem_of_union_eq_top {ι : Type*} (t : set ι) (s : ι → set β)

(w : (⋃ i ∈ t, s i) = ⊤) (x : β) :

∃ (i ∈ t), x ∈ s i :=

have p : x ∈ ⊤ := set.mem_univ x,

simpa only [←w, set.mem_Union] using p,

lemma nonempty_of_union_eq_top_of_nonempty

{ι : Type*} (t : set ι) (s : ι → set α) (H : nonempty α) (w : (⋃ i ∈ t, s i) = ⊤) :

t.nonempty :=

obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some,

exact ⟨x, m⟩,

theorem set_of_exists (p : ι → β → Prop) : {x | ∃ i, p i x} = ⋃ i, {x | p i x} :=

ext $ λ i, mem_Union.symm

theorem set_of_forall (p : ι → β → Prop) : {x | ∀ i, p i x} = ⋂ i, {x | p i x} :=

ext $ λ i, mem_Inter.symm

lemma Union_subset {s : ι → set α} {t : set α} (h : ∀ i, s i ⊆ t) : (⋃ i, s i) ⊆ t :=

@supr_le (set α) _ _ _ _ h

lemma Union₂_subset {s : Π i, κ i → set α} {t : set α} (h : ∀ i j, s i j ⊆ t) :

(⋃ i j, s i j) ⊆ t :=

Union_subset $ λ x, Union_subset (h x)

theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=

@le_infi (set β) _ _ _ _ h

lemma subset_Inter₂ {s : set α} {t : Π i, κ i → set α} (h : ∀ i j, s ⊆ t i j) : s ⊆ ⋂ i j, t i j :=

subset_Inter $ λ x, subset_Inter $ h x

@[simp] lemma Union_subset_iff {s : ι → set α} {t : set α} : (⋃ i, s i) ⊆ t ↔ ∀ i, s i ⊆ t :=

⟨λ h i, subset.trans (le_supr s _) h, Union_subset⟩

lemma Union₂_subset_iff {s : Π i, κ i → set α} {t : set α} :

(⋃ i j, s i j) ⊆ t ↔ ∀ i j, s i j ⊆ t :=

by simp_rw Union_subset_iff

@[simp] lemma subset_Inter_iff {s : set α} {t : ι → set α} : s ⊆ (⋂ i, t i) ↔ ∀ i, s ⊆ t i :=

@le_infi_iff (set α) _ _ _ _

@[simp] lemma subset_Inter₂_iff {s : set α} {t : Π i, κ i → set α} :

s ⊆ (⋂ i j, t i j) ↔ ∀ i j, s ⊆ t i j :=

by simp_rw subset_Inter_iff

lemma subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ ⋃ i, s i := le_supr

lemma Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le

lemma subset_Union₂ {s : Π i, κ i → set α} (i : ι) (j : κ i) : s i j ⊆ ⋃ i j, s i j :=

@le_supr₂ (set α) _ _ _ _ i j

lemma Inter₂_subset {s : Π i, κ i → set α} (i : ι) (j : κ i) : (⋂ i j, s i j) ⊆ s i j :=

@infi₂_le (set α) _ _ _ _ i j

lemma subset_Union_of_subset {s : set α} {t : ι → set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i :=

@le_supr_of_le (set α) _ _ _ _ i h

lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι) (h : s i ⊆ t) : (⋂ i, s i) ⊆ t :=

@infi_le_of_le (set α) _ _ _ _ i h

lemma subset_Union₂_of_subset {s : set α} {t : Π i, κ i → set α} (i : ι) (j : κ i) (h : s ⊆ t i j) :

s ⊆ ⋃ i j, t i j :=

@le_supr₂_of_le (set α) _ _ _ _ _ i j h

lemma Inter₂_subset_of_subset {s : Π i, κ i → set α} {t : set α} (i : ι) (j : κ i) (h : s i j ⊆ t) :

(⋂ i j, s i j) ⊆ t :=

@infi₂_le_of_le (set α) _ _ _ _ _ i j h

lemma Union_mono {s t : ι → set α} (h : ∀ i, s i ⊆ t i) : (⋃ i, s i) ⊆ ⋃ i, t i :=

@supr_mono (set α) _ _ s t h

lemma Union₂_mono {s t : Π i, κ i → set α} (h : ∀ i j, s i j ⊆ t i j) :

(⋃ i j, s i j) ⊆ ⋃ i j, t i j :=

@supr₂_mono (set α) _ _ _ s t h

lemma Inter_mono {s t : ι → set α} (h : ∀ i, s i ⊆ t i) : (⋂ i, s i) ⊆ ⋂ i, t i :=

@infi_mono (set α) _ _ s t h

lemma Inter₂_mono {s t : Π i, κ i → set α} (h : ∀ i j, s i j ⊆ t i j) :

(⋂ i j, s i j) ⊆ ⋂ i j, t i j :=

@infi₂_mono (set α) _ _ _ s t h

lemma Union_mono' {s : ι → set α} {t : ι₂ → set α} (h : ∀ i, ∃ j, s i ⊆ t j) :

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

@supr_mono' (set α) _ _ _ s t h

lemma Union₂_mono' {s : Π i, κ i → set α} {t : Π i', κ' i' → set α}

(h : ∀ i j, ∃ i' j', s i j ⊆ t i' j') :

(⋃ i j, s i j) ⊆ ⋃ i' j', t i' j' :=

@supr₂_mono' (set α) _ _ _ _ _ s t h

lemma Inter_mono' {s : ι → set α} {t : ι' → set α} (h : ∀ j, ∃ i, s i ⊆ t j) :

(⋂ i, s i) ⊆ (⋂ j, t j) :=

set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi

lemma Inter₂_mono' {s : Π i, κ i → set α} {t : Π i', κ' i' → set α}

(h : ∀ i' j', ∃ i j, s i j ⊆ t i' j') :

(⋂ i j, s i j) ⊆ ⋂ i' j', t i' j' :=

subset_Inter₂_iff.2 $ λ i' j', let ⟨i, j, hst⟩ := h i' j' in (Inter₂_subset _ _).trans hst

lemma Union₂_subset_Union (κ : ι → Sort*) (s : ι → set α) : (⋃ i (j : κ i), s i) ⊆ ⋃ i, s i :=

Union_mono $ λ i, Union_subset $ λ h, subset.rfl

lemma Inter_subset_Inter₂ (κ : ι → Sort*) (s : ι → set α) : (⋂ i, s i) ⊆ ⋂ i (j : κ i), s i :=

Inter_mono $ λ i, subset_Inter $ λ h, subset.rfl

lemma Union_set_of (P : ι → α → Prop) : (⋃ i, {x : α | P i x}) = {x : α | ∃ i, P i x} :=

by { ext, exact mem_Union }

lemma Inter_set_of (P : ι → α → Prop) : (⋂ i, {x : α | P i x}) = {x : α | ∀ i, P i x} :=

by { ext, exact mem_Inter }

lemma Union_congr_of_surjective {f : ι → set α} {g : ι₂ → set α} (h : ι → ι₂)

(h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⋃ x, f x) = ⋃ y, g y :=

h1.supr_congr h h2

lemma Inter_congr_of_surjective {f : ι → set α} {g : ι₂ → set α} (h : ι → ι₂)

(h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⋂ x, f x) = ⋂ y, g y :=

h1.infi_congr h h2

lemma Union_congr {s t : ι → set α} (h : ∀ i, s i = t i) : (⋃ i, s i) = ⋃ i, t i := supr_congr h

lemma Inter_congr {s t : ι → set α} (h : ∀ i, s i = t i) : (⋂ i, s i) = ⋂ i, t i := infi_congr h

lemma Union₂_congr {s t : Π i, κ i → set α} (h : ∀ i j, s i j = t i j) :

(⋃ i j, s i j) = ⋃ i j, t i j :=

Union_congr $ λ i, Union_congr $ h i

lemma Inter₂_congr {s t : Π i, κ i → set α} (h : ∀ i j, s i j = t i j) :

(⋂ i j, s i j) = ⋂ i j, t i j :=

Inter_congr $ λ i, Inter_congr $ h i

section nonempty

variables [nonempty ι] {f : ι → set α} {s : set α}

lemma Union_const (s : set β) : (⋃ i : ι, s) = s := supr_const

lemma Inter_const (s : set β) : (⋂ i : ι, s) = s := infi_const

lemma Union_eq_const (hf : ∀ i, f i = s) : (⋃ i, f i) = s := (Union_congr hf).trans $ Union_const _

lemma Inter_eq_const (hf : ∀ i, f i = s) : (⋂ i, f i) = s := (Inter_congr hf).trans $ Inter_const _

end nonempty

@[simp] theorem compl_Union (s : ι → set β) : (⋃ i, s i)ᶜ = (⋂ i, (s i)ᶜ) :=

compl_supr

lemma compl_Union₂ (s : Π i, κ i → set α) : (⋃ i j, s i j)ᶜ = ⋂ i j, (s i j)ᶜ :=

by simp_rw compl_Union

@[simp] theorem compl_Inter (s : ι → set β) : (⋂ i, s i)ᶜ = (⋃ i, (s i)ᶜ) :=

compl_infi

lemma compl_Inter₂ (s : Π i, κ i → set α) : (⋂ i j, s i j)ᶜ = ⋃ i j, (s i j)ᶜ :=

by simp_rw compl_Inter

theorem Union_eq_compl_Inter_compl (s : ι → set β) : (⋃ i, s i) = (⋂ i, (s i)ᶜ)ᶜ :=

by simp only [compl_Inter, compl_compl]

theorem Inter_eq_compl_Union_compl (s : ι → set β) : (⋂ i, s i) = (⋃ i, (s i)ᶜ)ᶜ :=

by simp only [compl_Union, compl_compl]

theorem inter_Union (s : set β) (t : ι → set β) :

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

inf_supr_eq _ _

theorem Union_inter (s : set β) (t : ι → set β) :

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

supr_inf_eq _ _

theorem Union_union_distrib (s : ι → set β) (t : ι → set β) :

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

supr_sup_eq

theorem Inter_inter_distrib (s : ι → set β) (t : ι → set β) :

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

infi_inf_eq

theorem union_Union [nonempty ι] (s : set β) (t : ι → set β) :

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

sup_supr

theorem Union_union [nonempty ι] (s : set β) (t : ι → set β) :

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

supr_sup

theorem inter_Inter [nonempty ι] (s : set β) (t : ι → set β) :

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

inf_infi

theorem Inter_inter [nonempty ι] (s : set β) (t : ι → set β) :

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

infi_inf

theorem union_Inter (s : set β) (t : ι → set β) :

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

sup_infi_eq _ _

theorem Inter_union (s : ι → set β) (t : set β) :

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

infi_sup_eq _ _

theorem Union_diff (s : set β) (t : ι → set β) :

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

Union_inter _ _

theorem diff_Union [nonempty ι] (s : set β) (t : ι → set β) :

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

by rw [diff_eq, compl_Union, inter_Inter]; refl

theorem diff_Inter (s : set β) (t : ι → set β) :

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

by rw [diff_eq, compl_Inter, inter_Union]; refl

lemma directed_on_Union {r} {f : ι → set α} (hd : directed (⊆) f)

(h : ∀ x, directed_on r (f x)) : directed_on r (⋃ x, f x) :=

by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact

λ a₁ b₁ fb₁ a₂ b₂ fb₂,

let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂,

⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in

⟨x, ⟨z, xf⟩, xa₁, xa₂⟩

lemma Union_inter_subset {ι α} {s t : ι → set α} : (⋃ i, s i ∩ t i) ⊆ (⋃ i, s i) ∩ (⋃ i, t i) :=

le_supr_inf_supr s t

lemma Union_inter_of_monotone {ι α} [preorder ι] [is_directed ι (≤)] {s t : ι → set α}

(hs : monotone s) (ht : monotone t) : (⋃ i, s i ∩ t i) = (⋃ i, s i) ∩ (⋃ i, t i) :=

supr_inf_of_monotone hs ht

lemma Union_inter_of_antitone {ι α} [preorder ι] [is_directed ι (swap (≤))] {s t : ι → set α}

(hs : antitone s) (ht : antitone t) : (⋃ i, s i ∩ t i) = (⋃ i, s i) ∩ (⋃ i, t i) :=

supr_inf_of_antitone hs ht

lemma Inter_union_of_monotone {ι α} [preorder ι] [is_directed ι (swap (≤))] {s t : ι → set α}

(hs : monotone s) (ht : monotone t) : (⋂ i, s i ∪ t i) = (⋂ i, s i) ∪ (⋂ i, t i) :=

infi_sup_of_monotone hs ht

lemma Inter_union_of_antitone {ι α} [preorder ι] [is_directed ι (≤)] {s t : ι → set α}

(hs : antitone s) (ht : antitone t) : (⋂ i, s i ∪ t i) = (⋂ i, s i) ∪ (⋂ i, t i) :=

infi_sup_of_antitone hs ht

lemma Union_Inter_subset {s : ι → ι' → set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j :=

supr_infi_le_infi_supr (flip s)

lemma Union_option {ι} (s : option ι → set α) : (⋃ o, s o) = s none ∪ ⋃ i, s (some i) :=

supr_option s

lemma Inter_option {ι} (s : option ι → set α) : (⋂ o, s o) = s none ∩ ⋂ i, s (some i) :=

infi_option s

variables (p : ι → Prop) [decidable_pred p]

lemma Union_dite (f : Π i, p i → set α) (g : Π i, ¬p i → set α) :

(⋃ i, if h : p i then f i h else g i h) = (⋃ i (h : p i), f i h) ∪ (⋃ i (h : ¬ p i), g i h) :=

supr_dite _ _ _

lemma Union_ite (f g : ι → set α) :

(⋃ i, if p i then f i else g i) = (⋃ i (h : p i), f i) ∪ (⋃ i (h : ¬ p i), g i) :=

Union_dite _ _ _

lemma Inter_dite (f : Π i, p i → set α) (g : Π i, ¬p i → set α) :

(⋂ i, if h : p i then f i h else g i h) = (⋂ i (h : p i), f i h) ∩ (⋂ i (h : ¬ p i), g i h) :=

infi_dite _ _ _

lemma Inter_ite (f g : ι → set α) :

(⋂ i, if p i then f i else g i) = (⋂ i (h : p i), f i) ∩ (⋂ i (h : ¬ p i), g i) :=

Inter_dite _ _ _

lemma image_projection_prod {ι : Type*} {α : ι → Type*} {v : Π (i : ι), set (α i)}

(hv : (pi univ v).nonempty) (i : ι) :

(λ (x : Π (i : ι), α i), x i) '' (⋂ k, (λ (x : Π (j : ι), α j), x k) ⁻¹' v k) = v i:=

classical,

apply subset.antisymm,

{ simp [Inter_subset] },

{ intros y y_in,

simp only [mem_image, mem_Inter, mem_preimage],

rcases hv with ⟨z, hz⟩,

refine ⟨function.update z i y, _, update_same i y z⟩,

rw @forall_update_iff ι α _ z i y (λ i t, t ∈ v i),

exact ⟨y_in, λ j hj, by simpa using hz j⟩ },

theorem Inter_false {s : false → set α} : Inter s = univ := infi_false

theorem Union_false {s : false → set α} : Union s = ∅ := supr_false

@[simp] theorem Inter_true {s : true → set α} : Inter s = s trivial := infi_true

@[simp] theorem Union_true {s : true → set α} : Union s = s trivial := supr_true

@[simp] theorem Inter_exists {p : ι → Prop} {f : Exists p → set α} :

(⋂ x, f x) = (⋂ i (h : p i), f ⟨i, h⟩) :=

infi_exists

@[simp] theorem Union_exists {p : ι → Prop} {f : Exists p → set α} :

(⋃ x, f x) = (⋃ i (h : p i), f ⟨i, h⟩) :=

supr_exists

@[simp] lemma Union_empty : (⋃ i : ι, ∅ : set α) = ∅ := supr_bot

@[simp] lemma Inter_univ : (⋂ i : ι, univ : set α) = univ := infi_top

variables {s : ι → set α}

@[simp] lemma Union_eq_empty : (⋃ i, s i) = ∅ ↔ ∀ i, s i = ∅ := supr_eq_bot

@[simp] lemma Inter_eq_univ : (⋂ i, s i) = univ ↔ ∀ i, s i = univ := infi_eq_top

@[simp] lemma nonempty_Union : (⋃ i, s i).nonempty ↔ ∃ i, (s i).nonempty :=

by simp [nonempty_iff_ne_empty]

@[simp] lemma nonempty_bUnion {t : set α} {s : α → set β} :

(⋃ i ∈ t, s i).nonempty ↔ ∃ i ∈ t, (s i).nonempty :=

by simp [nonempty_iff_ne_empty]

lemma Union_nonempty_index (s : set α) (t : s.nonempty → set β) :

(⋃ h, t h) = ⋃ x ∈ s, t ⟨x, ‹_›⟩ :=

supr_exists

@[simp] theorem Inter_Inter_eq_left {b : β} {s : Π x : β, x = b → set α} :

(⋂ x (h : x = b), s x h) = s b rfl :=

infi_infi_eq_left

@[simp] theorem Inter_Inter_eq_right {b : β} {s : Π x : β, b = x → set α} :

(⋂ x (h : b = x), s x h) = s b rfl :=

infi_infi_eq_right

@[simp] theorem Union_Union_eq_left {b : β} {s : Π x : β, x = b → set α} :

(⋃ x (h : x = b), s x h) = s b rfl :=

supr_supr_eq_left

@[simp] theorem Union_Union_eq_right {b : β} {s : Π x : β, b = x → set α} :

(⋃ x (h : b = x), s x h) = s b rfl :=

supr_supr_eq_right

theorem Inter_or {p q : Prop} (s : p ∨ q → set α) :

(⋂ h, s h) = (⋂ h : p, s (or.inl h)) ∩ (⋂ h : q, s (or.inr h)) :=

infi_or

theorem Union_or {p q : Prop} (s : p ∨ q → set α) :

(⋃ h, s h) = (⋃ i, s (or.inl i)) ∪ (⋃ j, s (or.inr j)) :=

supr_or

theorem Union_and {p q : Prop} (s : p ∧ q → set α) :

(⋃ h, s h) = ⋃ hp hq, s ⟨hp, hq⟩ :=

supr_and

theorem Inter_and {p q : Prop} (s : p ∧ q → set α) :

(⋂ h, s h) = ⋂ hp hq, s ⟨hp, hq⟩ :=

infi_and

lemma Union_comm (s : ι → ι' → set α) : (⋃ i i', s i i') = ⋃ i' i, s i i' := supr_comm

lemma Inter_comm (s : ι → ι' → set α) : (⋂ i i', s i i') = ⋂ i' i, s i i' := infi_comm

lemma Union₂_comm (s : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → set α) :

(⋃ i₁ j₁ i₂ j₂, s i₁ j₁ i₂ j₂) = ⋃ i₂ j₂ i₁ j₁, s i₁ j₁ i₂ j₂ :=

supr₂_comm _

lemma Inter₂_comm (s : Π i₁, κ₁ i₁ → Π i₂, κ₂ i₂ → set α) :

(⋂ i₁ j₁ i₂ j₂, s i₁ j₁ i₂ j₂) = ⋂ i₂ j₂ i₁ j₁, s i₁ j₁ i₂ j₂ :=

infi₂_comm _

@[simp] theorem bUnion_and (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 ⟨hx, hy⟩ :=

by simp only [Union_and, @Union_comm _ ι']

@[simp] theorem bUnion_and' (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 ⟨hy, hx⟩ :=

by simp only [Union_and, @Union_comm _ ι]

@[simp] theorem bInter_and (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 ⟨hx, hy⟩ :=

by simp only [Inter_and, @Inter_comm _ ι']

@[simp] theorem bInter_and' (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 ⟨hy, hx⟩ :=

by simp only [Inter_and, @Inter_comm _ ι]

@[simp] theorem Union_Union_eq_or_left {b : β} {p : β → Prop} {s : Π x : β, (x = b ∨ p x) → set α} :

(⋃ x h, s x h) = s b (or.inl rfl) ∪ ⋃ x (h : p x), s x (or.inr h) :=

by simp only [Union_or, Union_union_distrib, Union_Union_eq_left]

@[simp] theorem Inter_Inter_eq_or_left {b : β} {p : β → Prop} {s : Π x : β, (x = b ∨ p x) → set α} :

(⋂ x h, s x h) = s b (or.inl rfl) ∩ ⋂ x (h : p x), s x (or.inr h) :=

by simp only [Inter_or, Inter_inter_distrib, Inter_Inter_eq_left]

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

y ∈ ⋃ x ∈ s, t x :=

mem_Union₂_of_mem xs ytx

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

y ∈ ⋂ x ∈ s, t x :=

mem_Inter₂_of_mem h

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

u x ⊆ (⋃ x ∈ s, u x) :=

subset_Union₂ x xs

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

(⋂ x ∈ s, t x) ⊆ t x :=

Inter₂_subset x xs

theorem bUnion_subset_bUnion_left {s s' : set α} {t : α → set β}

(h : s ⊆ s') : (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s', t x) :=

Union₂_subset $ λ x hx, subset_bUnion_of_mem $ h hx

theorem bInter_subset_bInter_left {s s' : set α} {t : α → set β}

(h : s' ⊆ s) : (⋂ x ∈ s, t x) ⊆ (⋂ x ∈ s', t x) :=

subset_Inter₂ $ λ x hx, bInter_subset_of_mem $ h hx

lemma bUnion_mono {s s' : set α} {t t' : α → set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) :

(⋃ x ∈ s', t x) ⊆ ⋃ x ∈ s, t' x :=

(bUnion_subset_bUnion_left hs).trans $ Union₂_mono h

lemma bInter_mono {s s' : set α} {t t' : α → set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) :

(⋂ x ∈ s', t x) ⊆ (⋂ x ∈ s, t' x) :=

(bInter_subset_bInter_left hs).trans $ Inter₂_mono h

theorem bUnion_eq_Union (s : set α) (t : Π x ∈ s, set β) :

(⋃ x ∈ s, t x ‹_›) = (⋃ x : s, t x x.2) :=

supr_subtype'

theorem bInter_eq_Inter (s : set α) (t : Π x ∈ s, set β) :

(⋂ x ∈ s, t x ‹_›) = (⋂ x : s, t x x.2) :=

infi_subtype'

theorem Union_subtype (p : α → Prop) (s : {x // p x} → set β) :

(⋃ x : {x // p x}, s x) = ⋃ x (hx : p x), s ⟨x, hx⟩ :=

supr_subtype

theorem Inter_subtype (p : α → Prop) (s : {x // p x} → set β) :

(⋂ x : {x // p x}, s x) = ⋂ x (hx : p x), s ⟨x, hx⟩ :=

infi_subtype

theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=

infi_emptyset

theorem bInter_univ (u : α → set β) : (⋂ x ∈ @univ α, u x) = ⋂ x, u x :=

infi_univ

@[simp] lemma bUnion_self (s : set α) : (⋃ x ∈ s, s) = s :=

subset.antisymm (Union₂_subset $ λ x hx, subset.refl s) (λ x hx, mem_bUnion hx hx)

@[simp] lemma Union_nonempty_self (s : set α) : (⋃ h : s.nonempty, s) = s :=

by rw [Union_nonempty_index, bUnion_self]

theorem bInter_singleton (a : α) (s : α → set β) : (⋂ x ∈ ({a} : set α), s x) = s a :=

infi_singleton

theorem bInter_union (s t : set α) (u : α → set β) :

(⋂ x ∈ s ∪ t, u x) = (⋂ x ∈ s, u x) ∩ (⋂ x ∈ t, u x) :=

infi_union

theorem bInter_insert (a : α) (s : set α) (t : α → set β) :

(⋂ x ∈ insert a s, t x) = t a ∩ (⋂ x ∈ s, t x) :=

by simp

theorem bInter_pair (a b : α) (s : α → set β) :

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

by rw [bInter_insert, bInter_singleton]

lemma bInter_inter {ι α : Type*} {s : set ι} (hs : s.nonempty) (f : ι → set α) (t : set α) :

(⋂ i ∈ s, f i ∩ t) = (⋂ i ∈ s, f i) ∩ t :=

haveI : nonempty s := hs.to_subtype,

simp [bInter_eq_Inter, ← Inter_inter]

lemma inter_bInter {ι α : Type*} {s : set ι} (hs : s.nonempty) (f : ι → set α) (t : set α) :

(⋂ i ∈ s, t ∩ f i) = t ∩ ⋂ i ∈ s, f i :=

rw [inter_comm, ← bInter_inter hs],

simp [inter_comm]

theorem bUnion_empty (s : α → set β) : (⋃ x ∈ (∅ : set α), s x) = ∅ :=

supr_emptyset

theorem bUnion_univ (s : α → set β) : (⋃ x ∈ @univ α, s x) = ⋃ x, s x :=

supr_univ

theorem bUnion_singleton (a : α) (s : α → set β) : (⋃ x ∈ ({a} : set α), s x) = s a :=

supr_singleton

@[simp] theorem bUnion_of_singleton (s : set α) : (⋃ x ∈ s, {x}) = s :=

ext $ by simp

theorem bUnion_union (s t : set α) (u : α → set β) :

(⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) :=

supr_union

@[simp] lemma Union_coe_set {α β : Type*} (s : set α) (f : s → set β) :

(⋃ i, f i) = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩ :=

Union_subtype _ _

@[simp] lemma Inter_coe_set {α β : Type*} (s : set α) (f : s → set β) :

(⋂ i, f i) = ⋂ i ∈ s, f ⟨i, ‹i ∈ s›⟩ :=

Inter_subtype _ _

theorem bUnion_insert (a : α) (s : set α) (t : α → set β) :

(⋃ x ∈ insert a s, t x) = t a ∪ (⋃ x ∈ s, t x) :=

by simp

theorem bUnion_pair (a b : α) (s : α → set β) :

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

by simp

lemma inter_Union₂ (s : set α) (t : Π i, κ i → set α) : s ∩ (⋃ i j, t i j) = ⋃ i j, s ∩ t i j :=

by simp only [inter_Union]

lemma Union₂_inter (s : Π i, κ i → set α) (t : set α) : (⋃ i j, s i j) ∩ t = ⋃ i j, s i j ∩ t :=

by simp_rw Union_inter

lemma union_Inter₂ (s : set α) (t : Π i, κ i → set α) : s ∪ (⋂ i j, t i j) = ⋂ i j, s ∪ t i j :=

by simp_rw union_Inter

lemma Inter₂_union (s : Π i, κ i → set α) (t : set α) : (⋂ i j, s i j) ∪ t = ⋂ i j, s i j ∪ t :=

by simp_rw Inter_union

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

x ∈ ⋃₀ S :=

⟨t, ht, hx⟩

theorem not_mem_of_not_mem_sUnion {x : α} {t : set α} {S : set (set α)}

(hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t :=

λ h, hx ⟨t, ht, h⟩

theorem sInter_subset_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : ⋂₀ S ⊆ t :=

Inf_le tS

theorem subset_sUnion_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : t ⊆ ⋃₀ S :=

le_Sup tS

lemma subset_sUnion_of_subset {s : set α} (t : set (set α)) (u : set α) (h₁ : s ⊆ u)

(h₂ : u ∈ t) : s ⊆ ⋃₀ t :=

subset.trans h₁ (subset_sUnion_of_mem h₂)

theorem sUnion_subset {S : set (set α)} {t : set α} (h : ∀ t' ∈ S, t' ⊆ t) : (⋃₀ S) ⊆ t :=

Sup_le h

@[simp] theorem sUnion_subset_iff {s : set (set α)} {t : set α} : ⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t :=

@Sup_le_iff (set α) _ _ _

theorem subset_sInter {S : set (set α)} {t : set α} (h : ∀ t' ∈ S, t ⊆ t') : t ⊆ (⋂₀ S) :=

le_Inf h

@[simp] theorem subset_sInter_iff {S : set (set α)} {t : set α} : t ⊆ (⋂₀ S) ↔ ∀ t' ∈ S, t ⊆ t' :=

@le_Inf_iff (set α) _ _ _

theorem sUnion_subset_sUnion {S T : set (set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T :=

sUnion_subset $ λ s hs, subset_sUnion_of_mem (h hs)

theorem sInter_subset_sInter {S T : set (set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S :=

subset_sInter $ λ s hs, sInter_subset_of_mem (h hs)

@[simp] theorem sUnion_empty : ⋃₀ ∅ = (∅ : set α) := Sup_empty

@[simp] theorem sInter_empty : ⋂₀ ∅ = (univ : set α) := Inf_empty

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

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

@[simp] theorem sUnion_eq_empty {S : set (set α)} : (⋃₀ S) = ∅ ↔ ∀ s ∈ S, s = ∅ := Sup_eq_bot

@[simp] theorem sInter_eq_univ {S : set (set α)} : (⋂₀ S) = univ ↔ ∀ s ∈ S, s = univ := Inf_eq_top

@[simp] theorem nonempty_sUnion {S : set (set α)} : (⋃₀ S).nonempty ↔ ∃ s ∈ S, set.nonempty s :=

by simp [nonempty_iff_ne_empty]

lemma nonempty.of_sUnion {s : set (set α)} (h : (⋃₀ s).nonempty) : s.nonempty :=

let ⟨s, hs, _⟩ := nonempty_sUnion.1 h in ⟨s, hs⟩

lemma nonempty.of_sUnion_eq_univ [nonempty α] {s : set (set α)} (h : ⋃₀ s = univ) : s.nonempty :=

nonempty.of_sUnion $ h.symm ▸ univ_nonempty

theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T := Sup_union

theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union

@[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T :=

Sup_insert

@[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T :=

Inf_insert

@[simp] lemma sUnion_diff_singleton_empty (s : set (set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s :=

Sup_diff_singleton_bot s

@[simp] lemma sInter_diff_singleton_univ (s : set (set α)) : ⋂₀ (s \ {univ}) = ⋂₀ s :=

Inf_diff_singleton_top s

theorem sUnion_pair (s t : set α) : ⋃₀ {s, t} = s ∪ t :=

Sup_pair

theorem sInter_pair (s t : set α) : ⋂₀ {s, t} = s ∩ t :=

Inf_pair

@[simp] theorem sUnion_image (f : α → set β) (s : set α) : ⋃₀ (f '' s) = ⋃ x ∈ s, f x := Sup_image

@[simp] theorem sInter_image (f : α → set β) (s : set α) : ⋂₀ (f '' s) = ⋂ x ∈ s, f x := Inf_image

@[simp] theorem sUnion_range (f : ι → set β) : ⋃₀ (range f) = ⋃ x, f x := rfl

@[simp] theorem sInter_range (f : ι → set β) : ⋂₀ (range f) = ⋂ x, f x := rfl

lemma Union_eq_univ_iff {f : ι → set α} : (⋃ i, f i) = univ ↔ ∀ x, ∃ i, x ∈ f i :=

by simp only [eq_univ_iff_forall, mem_Union]

lemma Union₂_eq_univ_iff {s : Π i, κ i → set α} : (⋃ i j, s i j) = univ ↔ ∀ a, ∃ i j, a ∈ s i j :=

by simp only [Union_eq_univ_iff, mem_Union]

lemma sUnion_eq_univ_iff {c : set (set α)} :

⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b :=

by simp only [eq_univ_iff_forall, mem_sUnion]

lemma Inter_eq_empty_iff {f : ι → set α} : (⋂ i, f i) = ∅ ↔ ∀ x, ∃ i, x ∉ f i :=

by simp [set.eq_empty_iff_forall_not_mem]

lemma Inter₂_eq_empty_iff {s : Π i, κ i → set α} : (⋂ i j, s i j) = ∅ ↔ ∀ a, ∃ i j, a ∉ s i j :=

by simp only [eq_empty_iff_forall_not_mem, mem_Inter, not_forall]

lemma sInter_eq_empty_iff {c : set (set α)} :

⋂₀ c = ∅ ↔ ∀ a, ∃ b ∈ c, a ∉ b :=

by simp [set.eq_empty_iff_forall_not_mem]

@[simp] theorem nonempty_Inter {f : ι → set α} : (⋂ i, f i).nonempty ↔ ∃ x, ∀ i, x ∈ f i :=

by simp [nonempty_iff_ne_empty, Inter_eq_empty_iff]

@[simp] lemma nonempty_Inter₂ {s : Π i, κ i → set α} :

(⋂ i j, s i j).nonempty ↔ ∃ a, ∀ i j, a ∈ s i j :=

by simp [nonempty_iff_ne_empty, Inter_eq_empty_iff]

@[simp] theorem nonempty_sInter {c : set (set α)}:

(⋂₀ c).nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b :=

by simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]

theorem compl_sUnion (S : set (set α)) :

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

ext $ λ x, by simp

theorem sUnion_eq_compl_sInter_compl (S : set (set α)) :

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

by rw [←compl_compl (⋃₀ S), compl_sUnion]

theorem compl_sInter (S : set (set α)) :

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

by rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

theorem sInter_eq_compl_sUnion_compl (S : set (set α)) :

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

by rw [←compl_compl (⋂₀ S), compl_sInter]

theorem inter_empty_of_inter_sUnion_empty {s t : set α} {S : set (set α)} (hs : t ∈ S)

(h : s ∩ ⋃₀ S = ∅) :

s ∩ t = ∅ :=

eq_empty_of_subset_empty $ by rw ← h; exact

inter_subset_inter_right _ (subset_sUnion_of_mem hs)

theorem range_sigma_eq_Union_range {γ : α → Type*} (f : sigma γ → β) :

range f = ⋃ a, range (λ b, f ⟨a, b⟩) :=

set.ext $ by simp

theorem Union_eq_range_sigma (s : α → set β) : (⋃ i, s i) = range (λ a : Σ i, s i, a.2) :=

by simp [set.ext_iff]

theorem Union_eq_range_psigma (s : ι → set β) : (⋃ i, s i) = range (λ a : Σ' i, s i, a.2) :=

by simp [set.ext_iff]

theorem Union_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : set (sigma σ)) :

(⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s)) = s :=

ext x,

simp only [mem_Union, mem_image, mem_preimage],

split,

{ rintro ⟨i, a, h, rfl⟩, exact h },

{ intro h, cases x with i a, exact ⟨i, a, h, rfl⟩ }

lemma sigma.univ (X : α → Type*) : (set.univ : set (Σ a, X a)) = ⋃ a, range (sigma.mk a) :=

set.ext $ λ x, iff_of_true trivial ⟨range (sigma.mk x.1), set.mem_range_self _, x.2, sigma.eta x⟩

lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) :=

sUnion_subset $ λ t' ht', subset_sUnion_of_mem $ h ht'

lemma Union_subset_Union_const {s : set α} (h : ι → ι₂) : (⋃ i : ι, s) ⊆ (⋃ j : ι₂, s) :=

@supr_const_mono (set α) ι ι₂ _ s h

@[simp] lemma Union_singleton_eq_range {α β : Type*} (f : α → β) :

(⋃ (x : α), {f x}) = range f :=

by { ext x, simp [@eq_comm _ x] }

lemma Union_of_singleton (α : Type*) : (⋃ x, {x} : set α) = univ :=

by simp

lemma Union_of_singleton_coe (s : set α) :

(⋃ (i : s), {i} : set α) = s :=

by simp

lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=

by rw [← sUnion_image, image_id']

lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h : i ∈ s), i) :=

by rw [← sInter_image, image_id']

lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i) :=

by simp only [←sUnion_range, subtype.range_coe]

lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i) :=

by simp only [←sInter_range, subtype.range_coe]

@[simp] lemma Union_of_empty [is_empty ι] (s : ι → set α) : (⋃ i, s i) = ∅ := supr_of_empty _

@[simp] lemma Inter_of_empty [is_empty ι] (s : ι → set α) : (⋂ i, s i) = univ := infi_of_empty _

lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=

sup_eq_supr s₁ s₂

lemma inter_eq_Inter {s₁ s₂ : set α} : s₁ ∩ s₂ = ⋂ b : bool, cond b s₁ s₂ :=

inf_eq_infi s₁ s₂

lemma sInter_union_sInter {S T : set (set α)} :

(⋂₀ S) ∪ (⋂₀ T) = (⋂ p ∈ S ×ˢ T, (p : (set α) × (set α)).1 ∪ p.2) :=

Inf_sup_Inf

lemma sUnion_inter_sUnion {s t : set (set α)} :

(⋃₀ s) ∩ (⋃₀ t) = (⋃ p ∈ s ×ˢ t, (p : (set α) × (set α )).1 ∩ p.2) :=

Sup_inf_Sup

lemma bUnion_Union (s : ι → set α) (t : α → set β) :

(⋃ x ∈ ⋃ i, s i, t x) = ⋃ i (x ∈ s i), t x :=

by simp [@Union_comm _ ι]

lemma bInter_Union (s : ι → set α) (t : α → set β) :

(⋂ x ∈ ⋃ i, s i, t x) = ⋂ i (x ∈ s i), t x :=

by simp [@Inter_comm _ ι]

lemma sUnion_Union (s : ι → set (set α)) : ⋃₀ (⋃ i, s i) = ⋃ i, ⋃₀ (s i) :=

by simp only [sUnion_eq_bUnion, bUnion_Union]

theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i :=

by simp only [sInter_eq_bInter, bInter_Union]

lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α))

{f : ∀ (s : C), β → s} (hf : ∀ (s : C), surjective (f s)) :

(⋃ (y : β), range (λ (s : C), (f s y).val)) = ⋃₀ C :=

ext x, split,

{ rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩, refine ⟨_, hs, _⟩, exact (f ⟨s, hs⟩ y).2 },

{ rintro ⟨s, hs, hx⟩, cases hf ⟨s, hs⟩ ⟨x, hx⟩ with y hy, refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, _⟩,

exact congr_arg subtype.val hy }

lemma Union_range_eq_Union (C : ι → set α) {f : ∀ (x : ι), β → C x}

(hf : ∀ (x : ι), surjective (f x)) :

(⋃ (y : β), range (λ (x : ι), (f x y).val)) = ⋃ x, C x :=

ext x, rw [mem_Union, mem_Union], split,

{ rintro ⟨y, i, rfl⟩, exact ⟨i, (f i y).2⟩ },

{ rintro ⟨i, hx⟩, cases hf i ⟨x, hx⟩ with y hy,

exact ⟨y, i, congr_arg subtype.val hy⟩ }

lemma union_distrib_Inter_left (s : ι → set α) (t : set α) : t ∪ (⋂ i, s i) = (⋂ i, t ∪ s i) :=

sup_infi_eq _ _

lemma union_distrib_Inter₂_left (s : set α) (t : Π i, κ i → set α) :

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