theorem Set.Nontrivial.diff_singleton_nonempty {α : Type u_1} {s : Set α} (hs : s.Nontrivial) (x : α) : (s \ {x}).Nonempty

theorem Set.Nonempty.nontrivial_of_ssubset {α : Type u_1} {s t : Set α} (hs : s.Nonempty) (hst : s ⊂ t) : t.Nontrivial

theorem Set.Subsingleton.subset_or_disjoint {α : Type u_1} {s : Set α} (hs : s.Subsingleton) (t : Set α) : s ⊆ t ∨ Disjoint s t

theorem Set.Subsingleton.subset_of_nonempty_inter {α : Type u_1} {s t : Set α} (hs : s.Subsingleton) (hst : (s ∩ t).Nonempty) : s ⊆ t

theorem Set.Subsingleton.disjoint_iff_left {α : Type u_1} {s t : Set α} (hs : s.Subsingleton) : Disjoint s t ↔ s ⊆ t → s = ∅

theorem Set.Subsingleton.disjoint_iff_right {α : Type u_1} {s t : Set α} (hs : s.Subsingleton) : Disjoint t s ↔ s ⊆ t → s = ∅

theorem Set.Subsingleton.eq_or_eq_of_subset {α : Type u_1} {s t : Set α} (h : s.Subsingleton) (hts : t ⊆ s) : t = ∅ ∨ t = s

theorem Set.Subsingleton.exists_eq_of_singleton_of_nonempty {α : Type u_1} {s : Set α} (h : s.Subsingleton) (hne : s.Nonempty) : ∃ (x : α), s = {x}

@[simp]

theorem Set.insert_subsingleton_iff {α : Type u_1} {x : α} {s : Set α} : (insert x s).Subsingleton ↔ s ⊆ {x}

@[simp]

theorem Set.pair_subsingleton_iff {α : Type u_1} {x y : α} : {x, y}.Subsingleton ↔ x = y