theorem Finset.sdiff_erase_notMem {α : Type u_1} {s t : Finset α} {a : α} [DecidableEq α] (h : a ∉ s) : s \ t.erase a = s \ t

theorem Finset.sdiff_subset_iff {α : Type u_1} {s t r : Finset α} [DecidableEq α] : s \ t ⊆ r ↔ s ⊆ t ∪ r

theorem Finset.pair_sdiff_left {α : Type u_1} {a b : α} [DecidableEq α] (hne : a ≠ b) : {a, b} \ {a} = {b}

theorem Finset.pair_sdiff_right {α : Type u_1} {a b : α} [DecidableEq α] (hne : a ≠ b) : {a, b} \ {b} = {a}

theorem Finset.erase_eq_empty_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∈ s) : s.erase a = ∅ ↔ s = {a}

theorem Finset.coe_card_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : ↑(s ∩ t).card = ↑s.card + ↑t.card - ↑(s ∪ t).card

theorem Finset.singleton_subset_inter_and_union_subset_singleton {α : Type u_1} [DecidableEq α] {s t : Finset α} {e : α} (h : {e} ⊆ s ∩ t) (h' : s ∪ t ⊆ {e}) : s = {e} ∧ t = {e}

theorem Finset.singleton_of_mem_card_le_one {α : Type u_1} {e : α} {s : Finset α} (hs : s.card ≤ 1) (he : e ∈ s) : s = {e}

theorem Finset.inter_ssubset_of_not_subset_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : ¬s ⊆ t) : s ∩ t ⊂ s

theorem Finset.inter_ssubset_of_not_subset_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : ¬t ⊆ s) : s ∩ t ⊂ t

theorem Finset.finset_biUnion_union {α : Type u_1} {β : Type u_2} [DecidableEq α] (s t : Finset α) (u : α → Finset β) [DecidableEq β] : (s ∪ t).biUnion u = s.biUnion u ∪ t.biUnion u

theorem Finset.finset_biUnion_inter {α : Type u_1} {β : Type u_2} [DecidableEq α] (s t : Finset α) (u : α → Finset β) [DecidableEq β] : (s ∩ t).biUnion u ⊆ s.biUnion u ∩ t.biUnion u

theorem Finset.erase_inter_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : (s ∩ t).erase a = s.erase a ∩ t.erase a

@[simp]

theorem Finset.coe_nontrivial {α : Type u_3} {s : Finset α} : (↑s).Nontrivial ↔ s.Nontrivial

theorem Finset.subset_range_two {P : Finset ℕ} (hP : P ⊆ range 2) : P = ∅ ∨ P = {0} ∨ P = {1} ∨ P = {0, 1}

theorem List.toFinset_subset {α : Type u_1} [DecidableEq α] {a b : List α} (hab : a ⊆ b) : a.toFinset ⊆ b.toFinset

theorem Finset.interval_induction {α : Type u_1} {a b : α} [LinearOrder α] {F : Finset α} {R : α → α → Prop} (hjoin : ∀ (a c b : α), a < c → c < b → R a c → R c b → R a b) (hab : a < b) (hgap : ∀ (s t : α), a ≤ s → s < t → t ≤ b → s = a ∨ s ∈ F → t = b ∨ t ∈ F → (∀ u ∈ F, u ∉ Set.Ioo s t) → R s t) : R a b

A relation that joins adjacent intervals holds across an interval if it holds on each successive gap of a finite set of cut points. The gaps are the subintervals whose endpoints lie in {a, b} ∪ F and whose interiors avoid F.