theorem Set.iUnion_eq_single_of_forall_subset {α : Type u_1} {ι : Sort u_3} {s : ι → Set α} {a : ι} (hi : ∀ (i : ι), i ≠ a → s i ⊆ s a) : ⋃ (i : ι), s i = s a

theorem Set.iUnion_eq_single {α : Type u_1} {ι : Sort u_3} (s : ι → Set α) {a : ι} (hi : ∀ (i : ι), i ≠ a → s i = ∅) : ⋃ (i : ι), s i = s a

theorem Set.iUnion_inter_right_inter_eq_of_pairwise_disjoint {α : Type u_1} {ι : Type u_2} {s t : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) {j : ι} : (⋃ (i : ι), s i ∩ t i) ∩ s j = s j ∩ t j

theorem Set.iUnion_inter_left_inter_eq_of_pairwise_disjoint {α : Type u_1} {ι : Type u_2} {s t : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) {j : ι} : (⋃ (i : ι), t i ∩ s i) ∩ s j = t j ∩ s j

theorem Set.biUnion_eq_biUnion_nonempty {α : Type u_1} {ι : Type u_2} (s : ι → Set α) {u : Set ι} : ⋃ i ∈ u, s i = ⋃ i ∈ {i : ι | i ∈ u ∧ (s i).Nonempty}, s i

theorem Set.sInter_subset_sUnion {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) : ⋂₀ s ⊆ ⋃₀ s

theorem Set.inter_distrib_biInter {α : Type u_1} {ι : Type u_2} (s : ι → Set α) {u : Set ι} (hu : u.Nonempty) (t : Set α) : t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i

theorem Set.biInter_distrib_inter {α : Type u_1} {ι : Type u_2} (s : ι → Set α) {u : Set ι} (hu : u.Nonempty) (t : Set α) : (⋂ i ∈ u, s i) ∩ t = ⋂ i ∈ u, s i ∩ t

theorem Set.union_distrib_biUnion {α : Type u_1} {ι : Type u_2} (s : ι → Set α) {u : Set ι} (hu : u.Nonempty) (t : Set α) : t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i

theorem Set.biUnion_distrib_union {α : Type u_1} {ι : Type u_2} (s : ι → Set α) {u : Set ι} (hu : u.Nonempty) (t : Set α) : (⋃ i ∈ u, s i) ∪ t = ⋃ i ∈ u, s i ∪ t

theorem Set.inter_distrib_sInter {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) (t : Set α) : t ∩ ⋂₀ s = ⋂ x ∈ s, t ∩ x

theorem Set.sInter_distrib_inter {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) (t : Set α) : ⋂₀ s ∩ t = ⋂ x ∈ s, x ∩ t

theorem Set.union_distrib_sUnion {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) (t : Set α) : t ∪ ⋃₀ s = ⋃ x ∈ s, t ∪ x

theorem Set.sUnion_distrib_union {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) (t : Set α) : ⋃₀ s ∪ t = ⋃ x ∈ s, x ∪ t

theorem Set.sdiff_eq_sdiff_inter_of_subset {α : Type u_1} {s t : Set α} (h : s ⊆ t) (r : Set α) : s \ r = s \ (r ∩ t)

theorem Set.sdiff_union_eq_union_of_subset {α : Type u_1} (s : Set α) {t r : Set α} (h : t ⊆ r) : s \ t ∪ r = s ∪ r

theorem Set.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} {s t r : Set α} : s \ t = s \ r ↔ t ∩ s = r ∩ s

@[simp]

theorem Set.sdiff_inter_sdiff_right {α : Type u_1} {s t r : Set α} : t \ s ∩ (r \ s) = (t ∩ r) \ s

@[simp]

theorem Set.iInter_sdiff_distrib {ι : Type u_3} {α : Type u_4} [Nonempty ι] {G : ι → Set α} {X : Set α} : (⋂ (i : ι), G i) \ X = ⋂ (i : ι), G i \ X

@[simp]

theorem Set.biInter_sdiff_distrib {ι : Type u_3} {α : Type u_4} {s : Set ι} (hs : s.Nonempty) {G : ι → Set α} {X : Set α} : (⋂ i ∈ s, G i) \ X = ⋂ i ∈ s, G i \ X

@[simp]

theorem Set.sInter_sdiff_distrib {α : Type u_3} {s : Set (Set α)} (hs : s.Nonempty) {X : Set α} : ⋂₀ s \ X = ⋂₀ ((fun (x : Set α) => x \ X) '' s)

theorem Set.insert_inter_insert_eq {α : Type u_1} {A : Set α} {b c : α} (hne : b ≠ c) : insert b A ∩ insert c A = A

theorem Set.insert_union_insert_eq {α : Type u_1} {A : Set α} {b c : α} : insert b A ∪ insert c A = insert c (insert b A)

theorem Set.notMem_or_exists_eq_insert_notMem {α : Type u_1} (s : Set α) (x : α) : x ∉ s ∨ ∃ (s₀ : Set α), x ∉ s₀ ∧ s = insert x s₀

theorem Set.biInter_diff_singleton_eq_diff {α : Type u_1} (s : Set α) {t : Set α} (ht : t.Nonempty) : ⋂ i ∈ t, s \ {i} = s \ t

theorem Set.subset_sdiff_singleton_iff {α : Type u_1} {s t : Set α} {x : α} : s ⊆ t \ {x} ↔ s ⊆ t ∧ x ∉ s

theorem Set.image_preimage_image {α : Type u_1} {β : Type u_3} {s : Set α} {f : α → β} : f '' f ⁻¹' f '' s = f '' s

theorem Set.ssubset_sdiff_iff {α : Type u_1} {s t r : Set α} : s ⊂ t \ r ↔ s ⊆ t ∧ Disjoint s r ∧ ¬t ⊆ s ∪ r

theorem Set.sdiff_ssubset_sdiff {α : Type u_1} {s t r : Set α} (hst : s ⊂ t) (hstr : ¬t ⊆ s ∪ r) : s \ r ⊂ t \ r

theorem Set.sdiff_ssubset_sdiff_right {α : Type u_1} {s t r : Set α} (htr : t ⊆ r) (hst : s ⊂ t) : r \ t ⊂ r \ s

theorem Set.sdiff_ssubset_sdiff_right' {α : Type u_1} {s t r : Set α} (hstr : s ∩ r ⊂ t ∩ r) : r \ t ⊂ r \ s

theorem Set.sdiff_ssubset_sdiff_iff {α : Type u_1} (A B C : Set α) : A \ B ⊂ A \ C ↔ A ∩ C ⊂ A ∩ B

theorem Set.union_sdiff_eq_sdiff {α : Type u_1} {A B C : Set α} (hBC : B ⊆ C) : (A ∪ B) \ C = A \ C

theorem Set.InjOn.image_sdiff' {α : Type u_1} {β : Type u_3} {s x y : Set α} {f : α → β} (hs : InjOn f s) (hx : x ⊆ s) (hy : y ⊆ s) : f '' (x \ y) = f '' x \ f '' y

@[simp]

theorem Set.insert_eq_singleton_iff {α : Type u_1} {x y : α} {s : Set α} : insert x s = {y} ↔ x = y ∧ ∀ a ∈ s, a = y

theorem Set.disjoint_iff_forall_notMem {α : Type u_1} (A B : Set α) : Disjoint A B ↔ ∀ ⦃x : α⦄, x ∈ A → x ∉ B

theorem Set.sdiff_symmDiff_sdiff {α : Type u_1} (A B C : Set α) : symmDiff (A \ B) (A \ C) = A ∩ symmDiff B C

theorem Set.symmDiff_sdiff_distrib {α : Type u_1} (A B C : Set α) : symmDiff A B \ C = symmDiff (A \ C) (B \ C)

theorem Set.disjoint_sdiff_iff {α : Type u_1} (A B C : Set α) : Disjoint (A \ B) C ↔ A ∩ C ⊆ B

theorem Set.sdiff_symmDiff {α : Type u_1} (A B : Set α) : symmDiff (A \ B) A = A ∩ B

theorem Set.symmDiff_union_left {α : Type u_1} (A B C : Set α) : symmDiff (A ∪ B) (A ∪ C) = symmDiff B C \ A

theorem Set.union_diff_diff {α : Type u_1} (A B : Set α) : (A ∪ B) \ (A \ B) = B

theorem Set.iUnion_bool {α : Type u_1} {s : Bool → Set α} : ⋃ (i : Bool), s i = s true ∪ s false

theorem Set.iInter_bool {α : Type u_1} {s : Bool → Set α} : ⋂ (i : Bool), s i = s true ∩ s false

@[simp]

theorem Set.pair_nontrivial_iff {α : Type u_1} {x y : α} : {x, y}.Nontrivial ↔ x ≠ y

theorem Set.pairwise_on_bool' {α : Type u_3} {r : α → α → Prop} {f : Bool → α} (b : Bool) : Pairwise (Function.onFun r f) ↔ r (f b) (f !b) ∧ r (f !b) (f b)

theorem Set.pairwise_disjoint_on_bool' {α : Type u_3} {f : Bool → Set α} : Pairwise (Function.onFun Disjoint f) ↔ Disjoint (f true) (f false)

theorem Set.pairwise_disjoint_on_bool'' {α : Type u_3} {f : Bool → Set α} (b : Bool) : Pairwise (Function.onFun Disjoint f) ↔ Disjoint (f b) (f !b)

theorem Set.iUnion_bool' {α : Type u_3} (f : Bool → Set α) (b : Bool) : ⋃ (i : Bool), f i = f b ∪ f !b

theorem Set.iInter_bool' {α : Type u_3} (f : Bool → Set α) (b : Bool) : ⋂ (i : Bool), f i = f b ∩ f !b

theorem Set.sdiff_singleton_sdiff_eq {α : Type u_1} (s t : Set α) (x : α) : (s \ {x}) \ t = s \ insert x t

theorem Set.exists_partition_of_subset_iUnion {α : Type u_1} {ι : Type u_2} {s : Set α} {t : ι → Set α} (hst : s ⊆ ⋃ (i : ι), t i) : ∃ (r : ι → Set α), Pairwise (Function.onFun Disjoint r) ∧ ⋃ (i : ι), r i = s ∧ ∀ (i : ι), r i ⊆ t i

theorem Set.iUnion_sdiff_iUnion {ι : Type u_3} {α : Type u_4} {s t : ι → Set α} (hts : ∀ (i : ι), t i ⊆ s i) (hdj : Pairwise (Function.onFun Disjoint s)) : ⋃ (i : ι), s i \ t i = (⋃ (i : ι), s i) \ ⋃ (i : ι), t i

@[simp]

theorem Set.forall_mem_const' {α : Type u_3} {p : Prop} {s : Set α} (hs : s.Nonempty) : (∀ x ∈ s, p) ↔ p

@[simp]

theorem Set.forall_mem_and {α : Type u_3} {p q : α → Prop} {s : Set α} : (∀ x ∈ s, p x ∧ q x) ↔ (∀ x ∈ s, p x) ∧ ∀ x ∈ s, q x

theorem Set.biUnion_congr {α : Type u_3} {ι : Type u_4} {p : Set ι} {s t : ι → Set α} (h : ∀ i ∈ p, s i = t i) : ⋃ i ∈ p, s i = ⋃ i ∈ p, t i

theorem Set.biInter_congr {α : Type u_3} {ι : Type u_4} {p : Set ι} {s t : ι → Set α} (h : ∀ i ∈ p, s i = t i) : ⋂ i ∈ p, s i = ⋂ i ∈ p, t i