def Set.iUnion {α : Type u_1} {ι : Type u_3} (x : ι → Set α) : Set α

Equations

• Set.iUnion x = {a : α | ∃ (i : ι), a ∈ x i}

def Set.iInter {α : Type u_1} {ι : Type u_3} (x : ι → Set α) : Set α

Equations

• Set.iInter x = {a : α | ∀ (i : ι), a ∈ x i}

def Set.iUnionBuilder : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Set.elabiUnionBuilder : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Set.iUnion.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for set builder notation.

Equations

• One or more equations did not get rendered due to their size.

def Set.iInterBuilder : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Set.elabiInterBuilder : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Set.iInter.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for set builder notation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Set.mem_iUnion_iff {α : Type u_1} {ι : Type u_3} {a : α} {x : ι → Set α} : a ∈ ⋃ i : ι, x i ↔ ∃ (i : ι), a ∈ x i

theorem Set.mem_iUnion_of {α : Type u_1} {ι : Type u_3} {a : α} {i : ι} {x : ι → Set α} (h : a ∈ x i) : a ∈ ⋃ i : ι, x i

theorem Set.of_mem_iUnion {α : Type u_1} {ι : Type u_3} {a : α} {x : ι → Set α} (h : a ∈ ⋃ i : ι, x i) : ∃ (i : ι), a ∈ x i

@[simp]

theorem Set.subset_iUnion {α : Type u_1} {ι : Type u_3} {i : ι} {x : ι → Set α} : x i ⊆ ⋃ i : ι, x i

@[simp]

theorem Set.iUnion_subset_iff_all {α : Type u_1} {ι : Type u_3} {x : ι → Set α} {y : Set α} : ⋃ i : ι, x i ⊆ y ↔ ∀ (i : ι), x i ⊆ y

theorem Set.iUnion_empty_index {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (h : ι → False) : ⋃ i : ι, x i = ∅

@[simp]

theorem Set.iUnion_empty_iff {α : Type u_1} {ι : Type u_3} {x : ι → Set α} : ⋃ i : ι, x i = ∅ ↔ ∀ (i : ι), x i = ∅

@[simp]

theorem Set.mem_iInter_iff {α : Type u_1} {ι : Type u_3} {a : α} {x : ι → Set α} : a ∈ ⋂ i : ι, x i ↔ ∀ (i : ι), a ∈ x i

theorem Set.mem_iInter_of {α : Type u_1} {ι : Type u_3} {a : α} {x : ι → Set α} (h : ∀ (i : ι), a ∈ x i) : a ∈ ⋂ i : ι, x i

theorem Set.of_mem_iInter {α : Type u_1} {ι : Type u_3} {a : α} {i : ι} {x : ι → Set α} (h : a ∈ ⋂ i : ι, x i) : a ∈ x i

@[simp]

theorem Set.iInter_subset {α : Type u_1} {ι : Type u_3} {i : ι} {x : ι → Set α} : ⋂ i : ι, x i ⊆ x i

@[simp]

theorem Set.subset_iInter_iff_all {α : Type u_1} {ι : Type u_3} {x : ι → Set α} {y : Set α} : y ⊆ ⋂ i : ι, x i ↔ ∀ (i : ι), y ⊆ x i

theorem Set.iInter_empty_index {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (h : ι → False) : ⋂ i : ι, x i = Set.univ

@[simp]

theorem Set.iInter_univ_iff {α : Type u_1} {ι : Type u_3} {x : ι → Set α} : ⋂ i : ι, x i = Set.univ ↔ ∀ (i : ι), x i = Set.univ

@[simp]

theorem Set.iUnion_singleton {α : Type u_1} {x : Unit → Set α} : ⋃ i : Unit, x i = x PUnit.unit

@[simp]

theorem Set.iInter_singleton {α : Type u_1} {x : Unit → Set α} : ⋂ i : Unit, x i = x PUnit.unit

theorem Set.iUnion_singletons {α : Type u_1} {x : Set α} : ⋃ a : ↥x, {a.val} = x

theorem Set.iUnion_index_change_subset {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {f : ι' → ι} : ⋃ i' : ι', x (f i') ⊆ ⋃ i : ι, x i

theorem Set.iUnion_index_change_surj {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {f : ι' → ι} (h : Function.Surjective f) : ⋃ i' : ι', x (f i') = ⋃ i : ι, x i

theorem Set.iInter_subset_index_change {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {f : ι' → ι} : ⋂ i : ι, x i ⊆ ⋂ i' : ι', x (f i')

theorem Set.iInter_index_change_surj {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {f : ι' → ι} (h : Function.Surjective f) : ⋂ i' : ι', x (f i') = ⋂ i : ι, x i

theorem Set.iUnion_constant {α : Type u_1} {ι : Type u_3} {i : ι} {x : ι → Set α} (h : ∀ (i i' : ι), x i = x i') : ⋃ i : ι, x i = x i

theorem Set.iInter_constant {α : Type u_1} {ι : Type u_3} {i : ι} {x : ι → Set α} (h : ∀ (i i' : ι), x i = x i') : ⋂ i : ι, x i = x i

theorem Set.iUnion_index_mono {α : Type u_1} {ι : Type u_3} {x : ι → Set α} {p : ι → Prop} : ⋃ i : { i : ι // p i }, x i.val ⊆ ⋃ i : ι, x i

theorem Set.iInter_index_mono {α : Type u_1} {ι : Type u_3} {x : ι → Set α} {p : ι → Prop} : ⋂ i : ι, x i ⊆ ⋂ i : { i : ι // p i }, x i.val

theorem Set.iInter_subset_iUnion {α : Type u_1} {ι : Type u_3} {x : ι → Set α} [Nonempty ι] : ⋂ i : ι, x i ⊆ ⋃ i : ι, x i

theorem Set.iUnion_mono {α : Type u_1} {ι : Type u_3} {x x' : ι → Set α} (h : ∀ (i : ι), x i ⊆ x' i) : ⋃ i : ι, x i ⊆ ⋃ i : ι, x' i

theorem Set.iInter_mono {α : Type u_1} {ι : Type u_3} {x x' : ι → Set α} (h : ∀ (i : ι), x i ⊆ x' i) : ⋂ i : ι, x i ⊆ ⋂ i : ι, x' i

theorem Set.iUnion_assoc {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → ι' → Set α} : ⋃ i : ι × ι', x i.fst i.snd = ⋃ j : ι, ⋃ i : ι', x j i

theorem Set.iInter_assoc {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → ι' → Set α} : ⋂ i : ι × ι', x i.fst i.snd = ⋂ j : ι, ⋂ i : ι', x j i

theorem Set.iUnion_compl {α : Type u_1} {ι : Type u_3} {x : ι → Set α} : ⋃ i : ι, (x i)ᶜ = (⋂ i : ι, x i)ᶜ

theorem Set.iInter_compl {α : Type u_1} {ι : Type u_3} {x : ι → Set α} : ⋂ i : ι, (x i)ᶜ = (⋃ i : ι, x i)ᶜ

theorem Set.sprod_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {y' : ι' → Set β} : (⋃ i : ι, x i).prod (⋃ i : ι', y' i) = ⋃ j : ι × ι', (x j.fst).prod (y' j.snd)

theorem Set.sprod_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {y' : ι' → Set β} [inst : Nonempty ι] [inst' : Nonempty ι'] : (⋂ i : ι, x i).prod (⋂ i : ι', y' i) = ⋂ j : ι × ι', (x j.fst).prod (y' j.snd)

@[simp]

theorem Set.mem_union_iff {α : Type u_1} {a : α} {x x' : Set α} : a ∈ x ∪ x' ↔ a ∈ x ∨ a ∈ x'

@[simp]

theorem Set.mem_inter_iff {α : Type u_1} {a : α} {x x' : Set α} : a ∈ x ∩ x' ↔ a ∈ x ∧ a ∈ x'

theorem Set.union_eq_iUnion {α : Type u_1} {x x' : Set α} : x ∪ x' = ⋃ i : Bool, if i = true then x else x'

theorem Set.inter_eq_iInter {α : Type u_1} {x x' : Set α} : x ∩ x' = ⋂ i : Bool, if i = true then x else x'

theorem Set.union_comm {α : Type u_1} {x x' : Set α} : x ∪ x' = x' ∪ x

@[simp]

theorem Set.union_assoc {α : Type u_1} {x x' x'' : Set α} : x ∪ x' ∪ x'' = x ∪ (x' ∪ x'')

theorem Set.inter_comm {α : Type u_1} {x x' : Set α} : x ∩ x' = x' ∩ x

@[simp]

theorem Set.inter_assoc {α : Type u_1} {x x' x'' : Set α} : x ∩ x' ∩ x'' = x ∩ (x' ∩ x'')

@[simp]

theorem Set.subset_union_left {α : Type u_1} {x x' : Set α} : x ⊆ x ∪ x'

@[simp]

theorem Set.subset_union_right {α : Type u_1} {x x' : Set α} : x' ⊆ x ∪ x'

@[simp]

theorem Set.inter_subset_left {α : Type u_1} {x x' : Set α} : x ∩ x' ⊆ x

@[simp]

theorem Set.inter_subset_right {α : Type u_1} {x x' : Set α} : x ∩ x' ⊆ x'

@[simp]

theorem Set.inter_subset_union {α : Type u_1} {x x' : Set α} : x ∩ x' ⊆ x ∪ x'

theorem Set.subset_inter_iff {α : Type u_1} {x x' x'' : Set α} : x ⊆ x' ∩ x'' ↔ x ⊆ x' ∧ x ⊆ x''

theorem Set.union_subset_iff {α : Type u_1} {x x' x'' : Set α} : x ∪ x' ⊆ x'' ↔ x ⊆ x'' ∧ x' ⊆ x''

@[simp]

theorem Set.union_eq_iff_subset_left {α : Type u_1} {x x' : Set α} : x ∪ x' = x ↔ x' ⊆ x

@[simp]

theorem Set.union_eq_iff_subset_right {α : Type u_1} {x x' : Set α} : x ∪ x' = x' ↔ x ⊆ x'

@[simp]

theorem Set.inter_eq_iff_subset_left {α : Type u_1} {x x' : Set α} : x ∩ x' = x ↔ x ⊆ x'

@[simp]

theorem Set.inter_eq_iff_subset_right {α : Type u_1} {x x' : Set α} : x ∩ x' = x' ↔ x' ⊆ x

@[simp]

theorem Set.union_self {α : Type u_1} {x : Set α} : x ∪ x = x

@[simp]

theorem Set.inter_self {α : Type u_1} {x : Set α} : x ∩ x = x

theorem Set.union_inter_distrib_right {α : Type u_1} {x x' x'' : Set α} : x ∪ x' ∩ x'' = (x ∪ x') ∩ (x ∪ x'')

theorem Set.union_inter_distrib_left {α : Type u_1} {x x' x'' : Set α} : x ∩ x' ∪ x'' = (x ∪ x'') ∩ (x' ∪ x'')

theorem Set.inter_union_distrib_right {α : Type u_1} {x x' x'' : Set α} : x ∩ (x' ∪ x'') = x ∩ x' ∪ x ∩ x''

theorem Set.inter_union_distrib_left {α : Type u_1} {x x' x'' : Set α} : (x ∪ x') ∩ x'' = x ∩ x'' ∪ x' ∩ x''

@[simp]

theorem Set.inter_union_absorb_right_right {α : Type u_1} {x x' : Set α} : x ∩ (x' ∪ x) = x

@[simp]

theorem Set.inter_union_absorb_right_left {α : Type u_1} {x x' : Set α} : x ∩ (x ∪ x') = x

@[simp]

theorem Set.inter_union_absorb_left_right {α : Type u_1} {x x' : Set α} : (x' ∪ x) ∩ x = x

@[simp]

theorem Set.inter_union_absorb_left_left {α : Type u_1} {x x' : Set α} : (x ∪ x') ∩ x = x

@[simp]

theorem Set.union_inter_absorb_right_right {α : Type u_1} {x x' : Set α} : x ∪ x' ∩ x = x

@[simp]

theorem Set.union_inter_absorb_right_left {α : Type u_1} {x x' : Set α} : x ∪ x ∩ x' = x

@[simp]

theorem Set.union_inter_absorb_left_right {α : Type u_1} {x x' : Set α} : x' ∩ x ∪ x = x

@[simp]

theorem Set.union_inter_absorb_left_left {α : Type u_1} {x x' : Set α} : x ∩ x' ∪ x = x

@[simp]

theorem Set.union_univ {α : Type u_1} {x : Set α} : x ∪ Set.univ = Set.univ

@[simp]

theorem Set.univ_union {α : Type u_1} {x : Set α} : Set.univ ∪ x = Set.univ

@[simp]

theorem Set.union_empty {α : Type u_1} {x : Set α} : x ∪ ∅ = x

@[simp]

theorem Set.empty_union {α : Type u_1} {x : Set α} : ∅ ∪ x = x

@[simp]

theorem Set.inter_univ {α : Type u_1} {x : Set α} : x ∩ Set.univ = x

@[simp]

theorem Set.univ_inter {α : Type u_1} {x : Set α} : Set.univ ∩ x = x

@[simp]

theorem Set.inter_empty {α : Type u_1} {x : Set α} : x ∩ ∅ = ∅

@[simp]

theorem Set.empty_inter {α : Type u_1} {x : Set α} : ∅ ∩ x = ∅

@[simp]

theorem Set.compl_empty {α : Type u_1} : ∅ᶜ = Set.univ

@[simp]

theorem Set.compl_univ {α : Type u_1} : Set.univᶜ = ∅

theorem Set.compl_inter {α : Type u_1} {x x' : Set α} : (x ∩ x')ᶜ = xᶜ ∪ x'ᶜ

theorem Set.compl_union {α : Type u_1} {x x' : Set α} : (x ∪ x')ᶜ = xᶜ ∩ x'ᶜ

theorem Set.sdiff_union {α : Type u_1} {x x' x'' : Set α} : x \ (x' ∪ x'') = x \ x' ∩ (x \ x'')

theorem Set.sdiff_inter {α : Type u_1} {x x' x'' : Set α} : x \ (x' ∩ x'') = x \ x' ∪ x \ x''

@[simp]

theorem Set.sdiff_empty {α : Type u_1} {x : Set α} : x \ ∅ = x

@[simp]

theorem Set.empty_sdiff {α : Type u_1} {x : Set α} : ∅ \ x = ∅

@[simp]

theorem Set.sdiff_self {α : Type u_1} {x : Set α} : x \ x = ∅

theorem Set.sdiff_eq_inter_compl {α : Type u_1} {x x' : Set α} : x \ x' = x ∩ x'ᶜ

theorem Set.union_sdiff {α : Type u_1} {x x' x'' : Set α} : (x ∪ x') \ x'' = x \ x'' ∪ x' \ x''

theorem Set.inter_sdiff {α : Type u_1} {x x' x'' : Set α} : (x ∩ x') \ x'' = x \ x'' ∩ (x' \ x'')

theorem Set.sdiff_sdiff_right {α : Type u_1} {x x' x'' : Set α} : x \ (x' \ x'') = x \ x' ∪ x ∩ x''

theorem Set.sdiff_sdiff_left {α : Type u_1} {x x' x'' : Set α} : (x \ x') \ x'' = x \ (x' ∪ x'')

@[simp]

theorem Set.union_with_compl {α : Type u_1} {x : Set α} : x ∪ xᶜ = Set.univ

@[simp]

theorem Set.inter_with_compl {α : Type u_1} {x : Set α} : x ∩ xᶜ = ∅

theorem Set.union_mono {α : Type u_1} {x x' x'' x''' : Set α} (h : x ⊆ x') (h' : x'' ⊆ x''') : x ∪ x'' ⊆ x' ∪ x'''

theorem Set.union_mono_left {α : Type u_1} {x x' x'' : Set α} (h : x ⊆ x') : x ∪ x'' ⊆ x' ∪ x''

theorem Set.union_mono_right {α : Type u_1} {x x' x'' : Set α} (h : x' ⊆ x'') : x ∪ x' ⊆ x ∪ x''

theorem Set.inter_mono {α : Type u_1} {x x' x'' x''' : Set α} (h : x ⊆ x') (h' : x'' ⊆ x''') : x ∩ x'' ⊆ x' ∩ x'''

theorem Set.inter_mono_left {α : Type u_1} {x x' x'' : Set α} (h : x ⊆ x') : x ∩ x'' ⊆ x' ∩ x''

theorem Set.inter_mono_right {α : Type u_1} {x x' x'' : Set α} (h : x' ⊆ x'') : x ∩ x' ⊆ x ∩ x''

theorem Set.sdiff_mono_left {α : Type u_1} {x x' x'' : Set α} (h : x ⊆ x') : x \ x'' ⊆ x' \ x''

theorem Set.sdiff_mono_right {α : Type u_1} {x x' x'' : Set α} (h : x' ⊆ x'') : x \ x'' ⊆ x \ x'

@[simp]

theorem Set.sdiff_subset {α : Type u_1} {x x' : Set α} : x \ x' ⊆ x

@[simp]

theorem Set.sdiff_subset_compl {α : Type u_1} {x x' : Set α} : x \ x' ⊆ x'ᶜ

theorem Set.compl_inj {α : Type u_1} {x x' : Set α} (h : xᶜ = x'ᶜ) : x = x'

theorem Set.eq_compl_of {α : Type u_1} {x x' : Set α} (h : x ∪ x' = Set.univ) (h' : x ∩ x' = ∅) : x' = xᶜ

theorem Relation.iUnion_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {r : Relation α β} : r.image (⋃ i : ι, x i) = ⋃ i : ι, r.image (x i)

theorem Relation.iUnion_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {y : ι → Set β} {r : Relation α β} : r.preimage (⋃ i : ι, y i) = ⋃ i : ι, r.preimage (y i)

theorem Relation.subset_iInter_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {r : Relation α β} : r.image (⋂ i : ι, x i) ⊆ ⋂ i : ι, r.image (x i)

theorem Relation.subset_iInter_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {y : ι → Set β} {r : Relation α β} : r.preimage (⋂ i : ι, y i) ⊆ ⋂ i : ι, r.preimage (y i)

theorem Relation.union_image {α : Type u_1} {β : Type u_2} {r : Relation α β} {x x' : Set α} : r.image (x ∪ x') = r.image x ∪ r.image x'

theorem Relation.subset_inter_image {α : Type u_1} {β : Type u_2} {r : Relation α β} {x x' : Set α} : r.image (x ∩ x') ⊆ r.image x ∩ r.image x'

theorem Relation.union_preimage {α : Type u_1} {β : Type u_2} {r : Relation α β} {y y' : Set β} : r.preimage (y ∪ y') = r.preimage y ∪ r.preimage y'

theorem Relation.subset_inter_preimage {α : Type u_1} {β : Type u_2} {r : Relation α β} {y y' : Set β} : r.preimage (y ∩ y') ⊆ r.preimage y ∩ r.preimage y'

theorem Relation.rel_iUnion_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : Set α} {r : ι → Relation α β} : Relation.image (⋃ i : ι, r i) x = ⋃ i : ι, (r i).image x

theorem Relation.rel_iUnion_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {y : Set β} {r : ι → Relation α β} : Relation.preimage (⋃ i : ι, r i) y = ⋃ i : ι, (r i).preimage y

theorem Relation.rel_iInter_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {r : ι → Relation α β} {a : α} : Relation.image (⋂ i : ι, r i) {a} = ⋂ i : ι, (r i).image {a}

theorem Relation.rel_iInter_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {r : ι → Relation α β} {b : β} : Relation.preimage (⋂ i : ι, r i) {b} = ⋂ i : ι, (r i).preimage {b}

theorem Relation.iUnion_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {γ : Type u_5} {r : ι → Relation α β} {t : Relation γ α} : Relation.comp (⋃ i : ι, r i) t = ⋃ i : ι, (r i).comp t

theorem Relation.comp_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_3} {γ : Type u_5} {r : ι → Relation α β} {s : Relation β γ} : s.comp (⋃ i : ι, r i) = ⋃ i : ι, s.comp (r i)

theorem Relation.union_comp {α : Type u_1} {β : Type u_2} {γ : Type u_5} {t : Relation γ α} {r r' : Relation α β} : (r ∪ r').comp t = r.comp t ∪ r'.comp t

theorem Relation.comp_union {α : Type u_1} {β : Type u_2} {γ : Type u_5} {s : Relation β γ} {r r' : Relation α β} : s.comp (r ∪ r') = s.comp r ∪ s.comp r'

theorem Relation.rel_union_image {α : Type u_1} {β : Type u_2} {x : Set α} {r r' : Relation α β} : (r ∪ r').image x = r.image x ∪ r'.image x

theorem Relation.rel_union_preimage {α : Type u_1} {β : Type u_2} {y : Set β} {r r' : Relation α β} : (r ∪ r').preimage y = r.preimage y ∪ r'.preimage y

theorem Relation.rel_inter_image {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {a : α} : (r ∩ r').image {a} = r.image {a} ∩ r'.image {a}

theorem Relation.rel_inter_preimage {α : Type u_1} {β : Type u_2} {r r' : Relation α β} {b : β} : (r ∩ r').preimage {b} = r.preimage {b} ∩ r'.preimage {b}

theorem Relation.comp_inter_subset {α : Type u_1} {β : Type u_2} {γ : Type u_5} {s : Relation β γ} {r : Relation α β} {t : Relation α γ} : s.comp r ∩ t ⊆ (s ∩ t.comp r.inv).comp (r ∩ s.inv.comp t)

def Set.Disjoint {α : Type u_1} {ι : Type u_3} (x : ι → Set α) : Prop

Equations

• Set.Disjoint x = ∀ (i i' : ι), i ≠ i' → x i ∩ x i' = ∅

theorem Set.Disjoint.eq_of_subset_elem {α : Type u_1} {ι : Type u_3} {a : α} {x : ι → Set α} (hd : Set.Disjoint x) {y : Set α} (h : y.Nonempty) {i i' : ι} (ha : a ∈ x i) (ha' : a ∈ y) (h'' : y ⊆ x i') : i = i'

theorem Set.iUnion_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {f : α → β} : f '' ⋃ i : ι, x i = ⋃ i : ι, f '' x i

theorem Set.iUnion_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {y : ι → Set β} {f : α → β} : f ⁻¹' ⋃ i : ι, y i = ⋃ i : ι, f ⁻¹' y i

theorem Set.subset_iInter_image {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {f : α → β} : f '' ⋂ i : ι, x i ⊆ ⋂ i : ι, f '' x i

theorem Set.iInter_preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {y : ι → Set β} {f : α → β} : f ⁻¹' ⋂ i : ι, y i = ⋂ i : ι, f ⁻¹' y i

theorem Set.iInter_image_of_inj {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {f : α → β} [Nonempty ι] (h : Function.Injective f) : f '' ⋂ i : ι, x i = ⋂ i : ι, f '' x i

theorem Set.union_image {α : Type u_1} {β : Type u_2} {f : α → β} {x x' : Set α} : f '' (x ∪ x') = f '' x ∪ f '' x'

theorem Set.union_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {y y' : Set β} : f ⁻¹' (y ∪ y') = f ⁻¹' y ∪ f ⁻¹' y'

theorem Set.subset_inter_image {α : Type u_1} {β : Type u_2} {f : α → β} {x x' : Set α} : f '' (x ∩ x') ⊆ f '' x ∩ f '' x'

theorem Set.inter_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {y y' : Set β} : f ⁻¹' (y ∩ y') = f ⁻¹' y ∩ f ⁻¹' y'

theorem Set.sdiff_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {y y' : Set β} : f ⁻¹' (y \ y') = f ⁻¹' y \ f ⁻¹' y'

theorem Set.compl_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {y : Set β} : f ⁻¹' yᶜ = (f ⁻¹' y)ᶜ

theorem Set.sdiff_image_inj {α : Type u_1} {β : Type u_2} {f : α → β} {x x' : Set α} (h : Function.Injective f) : f '' (x \ x') = f '' x \ f '' x'

theorem Set.Disjoint.preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {f : α → β} {y : ι → Set β} (h : Set.Disjoint y) : Set.Disjoint (Set.preimage f ∘ y)

theorem Set.Disjoint.inj_of_nonempty {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (h : Set.Disjoint x) (h' : ∀ (i : ι), (x i).Nonempty) : Function.Injective x

theorem Set.Set.iUnion_iInter_distrib {α : Type u_5} {ι : Type u_6} {ι' : ι → Type} {x : (i : ι) → ι' i → Set α} : ⋃ i : ι, ⋂ i' : ι' i, x i i' = ⋂ f : (i : ι) → ι' i, ⋃ i : ι, x i (f i)

theorem Set.Set.iInter_iUnion_distrib {α : Type u_5} {ι : Type u_6} {ι' : ι → Type} {x : (i : ι) → ι' i → Set α} : ⋂ i : ι, ⋃ i' : ι' i, x i i' = ⋃ f : (i : ι) → ι' i, ⋂ i : ι, x i (f i)

theorem Set.Set.iInter_union_distrib {α : Type u_7} {ι : Type u_8} {ι' : Type u_9} {x : ι → Set α} {x' : ι' → Set α} : (⋂ i : ι, x i) ∪ ⋂ i' : ι', x' i' = ⋂ ii' : ι × ι', x ii'.fst ∪ x' ii'.snd

theorem Set.Set.iUnion_inter_distrib {α : Type u_7} {ι : Type u_8} {ι' : Type u_9} {x : ι → Set α} {x' : ι' → Set α} : (⋃ i : ι, x i) ∩ ⋃ i' : ι', x' i' = ⋃ ii' : ι × ι', x ii'.fst ∩ x' ii'.snd