Constructing finite sets by adding one element

This file contains the definitions of {a} : Finset α, insert a s : Finset α and Finset.cons, all ways to construct a Finset by adding one element.

Main declarations

• Finset.induction_on: Induction on finsets. To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty finset, and to show that if it holds for some Finset α, then it holds for the finset obtained by inserting a new element.
• Finset.instSingletonFinset: Denoted by {a}; the finset consisting of one element.
• insert and Finset.cons: For any a : α, insert s a returns s ∪ {a}. cons s a h returns the same except that it requires a hypothesis stating that a is not already in s. This does not require decidable equality on the type α.

Tags

finite sets, finset

Subset and strict subset relations

singleton

instance Finset.instSingleton {α : Type u_1} : Singleton α (Finset α)

{a} : Finset a is the set {a} containing a and nothing else.

This differs from insert a ∅ in that it does not require a DecidableEq instance for α.

@[simp]

theorem Finset.singleton_val {α : Type u_1} (a : α) : {a}.val = {a}

@[simp]

theorem Finset.mem_singleton {α : Type u_1} {a b : α} : b ∈ {a} ↔ b = a

theorem Finset.eq_of_mem_singleton {α : Type u_1} {x y : α} (h : x ∈ {y}) : x = y

theorem Finset.notMem_singleton {α : Type u_1} {a b : α} : a ∉ {b} ↔ a ≠ b

@[deprecated Finset.notMem_singleton (since := "2025-05-23")]

theorem Finset.not_mem_singleton {α : Type u_1} {a b : α} : a ∉ {b} ↔ a ≠ b

Alias of Finset.notMem_singleton.

theorem Finset.mem_singleton_self {α : Type u_1} (a : α) : a ∈ {a}

@[simp]

theorem Finset.val_eq_singleton_iff {α : Type u_1} {a : α} {s : Finset α} : s.val = {a} ↔ s = {a}

theorem Finset.singleton_injective {α : Type u_1} : Function.Injective singleton

@[simp]

theorem Finset.singleton_inj {α : Type u_1} {a b : α} : {a} = {b} ↔ a = b

@[simp]

theorem Finset.singleton_nonempty {α : Type u_1} (a : α) : {a}.Nonempty

@[simp]

theorem Finset.singleton_ne_empty {α : Type u_1} (a : α) : {a} ≠ ∅

theorem Finset.empty_ssubset_singleton {α : Type u_1} {a : α} : ∅ ⊂ {a}

@[simp]

theorem Finset.coe_singleton {α : Type u_1} (a : α) : ↑{a} = {a}

@[simp]

theorem Finset.coe_eq_singleton {α : Type u_1} {s : Finset α} {a : α} : ↑s = {a} ↔ s = {a}

theorem Finset.coe_subset_singleton {α : Type u_1} {s : Finset α} {a : α} : ↑s ⊆ {a} ↔ s ⊆ {a}

theorem Finset.singleton_subset_coe {α : Type u_1} {s : Finset α} {a : α} : {a} ⊆ ↑s ↔ {a} ⊆ s

theorem Finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : Finset α} {a : α} : s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

theorem Finset.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : Finset α} {a : α} : s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

theorem Finset.nonempty_iff_eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} : s.Nonempty ↔ s = {default}

theorem Finset.Nonempty.eq_singleton_default {α : Type u_1} [Unique α] {s : Finset α} : s.Nonempty → s = {default}

Alias of the forward direction of Finset.nonempty_iff_eq_singleton_default.

theorem Finset.singleton_iff_unique_mem {α : Type u_1} (s : Finset α) : (∃ (a : α), s = {a}) ↔ ∃! a : α, a ∈ s

theorem Finset.singleton_subset_set_iff {α : Type u_1} {s : Set α} {a : α} : ↑{a} ⊆ s ↔ a ∈ s

@[simp]

theorem Finset.singleton_subset_iff {α : Type u_1} {s : Finset α} {a : α} : {a} ⊆ s ↔ a ∈ s

@[simp]

theorem Finset.subset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} : s ⊆ {a} ↔ s = ∅ ∨ s = {a}

theorem Finset.singleton_subset_singleton {α : Type u_1} {a b : α} : {a} ⊆ {b} ↔ a = b

theorem Finset.Nonempty.subset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} (h : s.Nonempty) : s ⊆ {a} ↔ s = {a}

theorem Finset.subset_singleton_iff' {α : Type u_1} {s : Finset α} {a : α} : s ⊆ {a} ↔ ∀ b ∈ s, b = a

@[simp]

theorem Finset.ssubset_singleton_iff {α : Type u_1} {s : Finset α} {a : α} : s ⊂ {a} ↔ s = ∅

theorem Finset.eq_empty_of_ssubset_singleton {α : Type u_1} {s : Finset α} {x : α} (hs : s ⊂ {x}) : s = ∅

@[reducible, inline]

abbrev Finset.Nontrivial {α : Type u_1} (s : Finset α) : Prop

A finset is nontrivial if it has at least two elements.

theorem Finset.Nontrivial.nonempty {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) : s.Nonempty

@[simp]

theorem Finset.not_nontrivial_empty {α : Type u_1} : ¬∅.Nontrivial

@[simp]

theorem Finset.not_nontrivial_singleton {α : Type u_1} {a : α} : ¬{a}.Nontrivial

theorem Finset.Nontrivial.ne_singleton {α : Type u_1} {s : Finset α} {a : α} (hs : s.Nontrivial) : s ≠ {a}

theorem Finset.Nontrivial.exists_ne {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) (a : α) : ∃ b ∈ s, b ≠ a

theorem Finset.eq_singleton_or_nontrivial {α : Type u_1} {s : Finset α} {a : α} (ha : a ∈ s) : s = {a} ∨ s.Nontrivial

theorem Finset.nontrivial_iff_ne_singleton {α : Type u_1} {s : Finset α} {a : α} (ha : a ∈ s) : s.Nontrivial ↔ s ≠ {a}

theorem Finset.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u_1} {s : Finset α} : s.Nonempty → (∃ (a : α), s = {a}) ∨ s.Nontrivial

@[simp]

theorem Finset.nontrivial_coe {α : Type u_1} {s : Finset α} : (↑s).Nontrivial ↔ s.Nontrivial

theorem Finset.Nontrivial.of_coe {α : Type u_1} {s : Finset α} : (↑s).Nontrivial → s.Nontrivial

Alias of the forward direction of Finset.nontrivial_coe.

theorem Finset.Nontrivial.coe {α : Type u_1} {s : Finset α} : s.Nontrivial → (↑s).Nontrivial

Alias of the reverse direction of Finset.nontrivial_coe.

theorem Finset.Nontrivial.not_subset_singleton {α : Type u_1} {s : Finset α} {a : α} (hs : s.Nontrivial) : ¬s ⊆ {a}

instance Finset.instNontrivial {α : Type u_1} [Nonempty α] : Nontrivial (Finset α)

instance Finset.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (Finset α)

instance Finset.instUniqueSubtypeMemSingleton {α : Type u_1} (i : α) : Unique { x : α // x ∈ {i} }

@[simp]

theorem Finset.default_singleton {α : Type u_1} (i : α) : ↑default = i

instance Finset.Nontrivial.instDecidablePred {α : Type u_1} [DecidableEq α] : DecidablePred Finset.Nontrivial

cons

def Finset.cons {α : Type u_1} (a : α) (s : Finset α) (h : a ∉ s) : Finset α

cons a s h is the set {a} ∪ s containing a and the elements of s. It is the same as insert a s when it is defined, but unlike insert a s it does not require DecidableEq α, and the union is guaranteed to be disjoint.

@[simp]

theorem Finset.mem_cons {α : Type u_1} {s : Finset α} {a b : α} {h : a ∉ s} : b ∈ cons a s h ↔ b = a ∨ b ∈ s

theorem Finset.mem_cons_of_mem {α : Type u_1} {a b : α} {s : Finset α} {hb : b ∉ s} (ha : a ∈ s) : a ∈ cons b s hb

theorem Finset.mem_cons_self {α : Type u_1} (a : α) (s : Finset α) {h : a ∉ s} : a ∈ cons a s h

@[simp]

theorem Finset.cons_val {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (cons a s h).val = a ::ₘ s.val

theorem Finset.eq_of_mem_cons_of_notMem {α : Type u_1} {s : Finset α} {a b : α} (has : a ∉ s) (h : b ∈ cons a s has) (hb : b ∉ s) : b = a

@[deprecated Finset.eq_of_mem_cons_of_notMem (since := "2025-05-23")]

theorem Finset.eq_of_mem_cons_of_not_mem {α : Type u_1} {s : Finset α} {a b : α} (has : a ∉ s) (h : b ∈ cons a s has) (hb : b ∉ s) : b = a

Alias of Finset.eq_of_mem_cons_of_notMem.

theorem Finset.mem_of_mem_cons_of_ne {α : Type u_1} {s : Finset α} {a : α} {has : a ∉ s} {i : α} (hi : i ∈ cons a s has) (hia : i ≠ a) : i ∈ s

theorem Finset.forall_mem_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) (p : α → Prop) : (∀ x ∈ cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x

theorem Finset.forall_of_forall_cons {α : Type u_1} {s : Finset α} {a : α} {p : α → Prop} {h : a ∉ s} (H : ∀ x ∈ cons a s h, p x) (x : α) : x ∈ s → p x

Useful in proofs by induction.

@[simp]

theorem Finset.mk_cons {α : Type u_1} {a : α} {s : Multiset α} (h : (a ::ₘ s).Nodup) : { val := a ::ₘ s, nodup := h } = cons a { val := s, nodup := ⋯ } ⋯

@[simp]

theorem Finset.cons_empty {α : Type u_1} (a : α) : cons a ∅ ⋯ = {a}

@[simp]

theorem Finset.cons_nonempty {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : (cons a s h).Nonempty

@[simp]

theorem Finset.cons_ne_empty {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : cons a s h ≠ ∅

@[simp]

theorem Finset.nonempty_mk {α : Type u_1} {m : Multiset α} {hm : m.Nodup} : { val := m, nodup := hm }.Nonempty ↔ m ≠ 0

@[simp]

theorem Finset.coe_cons {α : Type u_1} {a : α} {s : Finset α} {h : a ∉ s} : ↑(cons a s h) = insert a ↑s

theorem Finset.subset_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : s ⊆ cons a s h

theorem Finset.ssubset_cons {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s) : s ⊂ cons a s h

theorem Finset.cons_subset {α : Type u_1} {s t : Finset α} {a : α} {h : a ∉ s} : cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t

@[simp]

theorem Finset.cons_subset_cons {α : Type u_1} {s t : Finset α} {a : α} {hs : a ∉ s} {ht : a ∉ t} : cons a s hs ⊆ cons a t ht ↔ s ⊆ t

theorem Finset.ssubset_iff_exists_cons_subset {α : Type u_1} {s t : Finset α} : s ⊂ t ↔ ∃ (a : α) (h : a ∉ s), cons a s h ⊆ t

theorem Finset.cons_swap {α : Type u_1} {s : Finset α} {a b : α} (hb : b ∉ s) (ha : a ∉ cons b s hb) : cons a (cons b s hb) ha = cons b (cons a s ⋯) ⋯

def Finset.consPiProd {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ cons a s has → f i) : f a × ((i : α) → i ∈ s → f i)

Split the added element of cons off a Pi type.

@[simp]

theorem Finset.consPiProd_snd {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ cons a s has → f i) (i : α) (hi : i ∈ s) : (consPiProd f has x).2 i hi = x i ⋯

@[simp]

theorem Finset.consPiProd_fst {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ cons a s has → f i) : (consPiProd f has x).1 = x a ⋯

def Finset.prodPiCons {α : Type u_1} {s : Finset α} [DecidableEq α] (f : α → Type u_3) {a : α} (has : a ∉ s) (x : f a × ((i : α) → i ∈ s → f i)) (i : α) : i ∈ cons a s has → f i

Combine a product with a pi type to pi of cons.

def Finset.consPiProdEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α} (has : a ∉ s) : ((i : α) → i ∈ cons a s has → f i) ≃ f a × ((i : α) → i ∈ s → f i)

The equivalence between pi types on cons and the product.

insert

instance Finset.instInsert {α : Type u_1} [DecidableEq α] : Insert α (Finset α)

insert a s is the set {a} ∪ s containing a and the elements of s.

theorem Finset.insert_def {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s = { val := Multiset.ndinsert a s.val, nodup := ⋯ }

@[simp]

theorem Finset.insert_val {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).val = Multiset.ndinsert a s.val

theorem Finset.insert_val' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).val = (a ::ₘ s.val).dedup

theorem Finset.insert_val_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).val = a ::ₘ s.val

@[deprecated Finset.insert_val_of_notMem (since := "2025-05-23")]

theorem Finset.insert_val_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).val = a ::ₘ s.val

Alias of Finset.insert_val_of_notMem.

@[simp]

theorem Finset.mem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} : a ∈ insert b s ↔ a = b ∨ a ∈ s

theorem Finset.mem_insert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : a ∈ insert a s

theorem Finset.mem_insert_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (h : a ∈ s) : a ∈ insert b s

theorem Finset.mem_of_mem_insert_of_ne {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (h : b ∈ insert a s) : b ≠ a → b ∈ s

theorem Finset.eq_of_mem_insert_of_notMem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (ha : b ∈ insert a s) (hb : b ∉ s) : b = a

@[deprecated Finset.eq_of_mem_insert_of_notMem (since := "2025-05-23")]

theorem Finset.eq_of_mem_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (ha : b ∈ insert a s) (hb : b ∉ s) : b = a

Alias of Finset.eq_of_mem_insert_of_notMem.

@[simp]

theorem Finset.insert_empty {α : Type u_1} [DecidableEq α] {a : α} : insert a ∅ = {a}

A version of LawfulSingleton.insert_empty_eq that works with dsimp.

@[simp]

theorem Finset.cons_eq_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s) : cons a s h = insert a s

@[simp]

theorem Finset.coe_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : ↑(insert a s) = insert a ↑s

theorem Finset.mem_insert_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {x y : α} : x ∈ insert y s ↔ x ∈ insert y ↑s

instance Finset.instLawfulSingleton {α : Type u_1} [DecidableEq α] : LawfulSingleton α (Finset α)

@[simp]

theorem Finset.insert_eq_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∈ s) : insert a s = s

@[simp]

theorem Finset.insert_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : insert a s = s ↔ a ∈ s

theorem Finset.insert_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} : insert a s ≠ s ↔ a ∉ s

theorem Finset.pair_eq_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a, a} = {a}

theorem Finset.insert_comm {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s)

@[deprecated Finset.insert_comm (since := "2024-11-29")]

theorem Finset.Insert.comm {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s)

Alias of Finset.insert_comm.

theorem Finset.coe_pair {α : Type u_1} [DecidableEq α] {a b : α} : ↑{a, b} = {a, b}

@[simp]

theorem Finset.coe_eq_pair {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} : ↑s = {a, b} ↔ s = {a, b}

theorem Finset.pair_comm {α : Type u_1} [DecidableEq α] (a b : α) : {a, b} = {b, a}

theorem Finset.insert_idem {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a (insert a s) = insert a s

@[simp]

theorem Finset.insert_nonempty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).Nonempty

@[simp]

theorem Finset.insert_ne_empty {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : insert a s ≠ ∅

instance Finset.instNonemptyElemToSetInsert {α : Type u_1} [DecidableEq α] (i : α) (s : Finset α) : Nonempty ↑↑(insert i s)

theorem Finset.ne_insert_of_notMem {α : Type u_1} [DecidableEq α] (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t

@[deprecated Finset.ne_insert_of_notMem (since := "2025-05-23")]

theorem Finset.ne_insert_of_not_mem {α : Type u_1} [DecidableEq α] (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t

Alias of Finset.ne_insert_of_notMem.

theorem Finset.insert_subset_iff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Finset.insert_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t

@[simp]

theorem Finset.subset_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s ⊆ insert a s

theorem Finset.insert_subset_insert {α : Type u_1} [DecidableEq α] (a : α) {s t : Finset α} (h : s ⊆ t) : insert a s ⊆ insert a t

@[simp]

theorem Finset.insert_subset_insert_iff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t

theorem Finset.insert_inj {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (ha : a ∉ s) : insert a s = insert b s ↔ a = b

theorem Finset.insert_inj_on {α : Type u_1} [DecidableEq α] (s : Finset α) : Set.InjOn (fun (a : α) => insert a s) (↑s)ᶜ

theorem Finset.ssubset_iff {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

theorem Finset.ssubset_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∉ s) : s ⊂ insert a s

theorem Finset.cons_induction {α : Type u_3} {motive : Finset α → Prop} (empty : motive ∅) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) (s : Finset α) : motive s

theorem Finset.cons_induction_on {α : Type u_3} {motive : Finset α → Prop} (s : Finset α) (empty : motive ∅) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : motive s

theorem Finset.induction {α : Type u_3} {motive : Finset α → Prop} [DecidableEq α] (empty : motive ∅) (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) (s : Finset α) : motive s

theorem Finset.induction_on {α : Type u_3} {motive : Finset α → Prop} [DecidableEq α] (s : Finset α) (empty : motive ∅) (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) : motive s

To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α, then it holds for the Finset obtained by inserting a new element.

theorem Finset.induction_on' {α : Type u_3} {motive : Finset α → Prop} [DecidableEq α] (S : Finset α) (empty : motive ∅) (insert : ∀ (a : α) (s : Finset α), a ∈ S → s ⊆ S → a ∉ s → motive s → motive (insert a s)) : motive S

To prove a proposition about S : Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α ⊆ S, then it holds for the Finset obtained by inserting a new element of S.

theorem Finset.Nonempty.cons_induction {α : Type u_3} {motive : (s : Finset α) → s.Nonempty → Prop} (singleton : ∀ (a : α), motive {a} ⋯) (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (cons a s h) ⋯) {s : Finset α} (hs : s.Nonempty) : motive s hs

To prove a proposition about a nonempty s : Finset α, it suffices to show it holds for all singletons and that if it holds for nonempty t : Finset α, then it also holds for the Finset obtained by inserting an element in t.

theorem Finset.Nonempty.exists_cons_eq {α : Type u_3} {s : Finset α} (hs : s.Nonempty) : ∃ (t : Finset α) (a : α) (ha : a ∉ t), cons a t ha = s

def Finset.subtypeInsertEquivOption {α : Type u_1} [DecidableEq α] {t : Finset α} {x : α} (h : x ∉ t) : { i : α // i ∈ insert x t } ≃ Option { i : α // i ∈ t }

Inserting an element to a finite set is equivalent to the option type.

def Finset.insertPiProd {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i) : f a × ((i : α) → i ∈ s → f i)

Split the added element of insert off a Pi type.

@[simp]

theorem Finset.insertPiProd_fst {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i) : (insertPiProd f x).1 = x a ⋯

@[simp]

theorem Finset.insertPiProd_snd {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i) (i : α) (hi : i ∈ s) : (insertPiProd f x).2 i hi = x i ⋯

def Finset.prodPiInsert {α : Type u_1} [DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α} (x : f a × ((i : α) → i ∈ s → f i)) (i : α) : i ∈ insert a s → f i

Combine a product with a pi type to pi of insert.

def Finset.insertPiProdEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α} (has : a ∉ s) : ((i : α) → i ∈ insert a s → f i) ≃ f a × ((i : α) → i ∈ s → f i)

The equivalence between pi types on insert and the product.

theorem Finset.exists_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : α → Prop) : (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

theorem Finset.forall_mem_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (p : α → Prop) : (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x

theorem Finset.forall_of_forall_insert {α : Type u_1} [DecidableEq α] {p : α → Prop} {a : α} {s : Finset α} (H : ∀ x ∈ insert a s, p x) (x : α) (h : x ∈ s) : p x

Useful in proofs by induction.

@[simp]

theorem Multiset.toFinset_zero {α : Type u_1} [DecidableEq α] : toFinset 0 = ∅

@[simp]

theorem Multiset.toFinset_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : (a ::ₘ s).toFinset = insert a s.toFinset

@[simp]

theorem Multiset.toFinset_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.toFinset = {a}

@[simp]

theorem List.toFinset_nil {α : Type u_1} [DecidableEq α] : [].toFinset = ∅

@[simp]

theorem List.toFinset_cons {α : Type u_1} [DecidableEq α] {l : List α} {a : α} : (a :: l).toFinset = insert a l.toFinset

theorem List.toFinset_replicate_of_ne_zero {α : Type u_1} [DecidableEq α] {a : α} {n : ℕ} (hn : n ≠ 0) : (replicate n a).toFinset = {a}

@[simp]

theorem List.toFinset_eq_empty_iff {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset = ∅ ↔ l = []

@[simp]

theorem List.toFinset_nonempty_iff {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.Nonempty ↔ l ≠ []

@[simp]

theorem Finset.toList_eq_singleton_iff {α : Type u_1} {a : α} {s : Finset α} : s.toList = [a] ↔ s = {a}

@[simp]

theorem Finset.toList_singleton {α : Type u_1} (a : α) : {a}.toList = [a]

theorem Finset.toList_cons {α : Type u_1} {a : α} {s : Finset α} (h : a ∉ s) : (cons a s h).toList.Perm (a :: s.toList)

theorem Finset.toList_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).toList.Perm (a :: s.toList)

theorem Finset.pairwise_cons' {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) : Pairwise (Function.onFun r fun (a_1 : { x : α // x ∈ cons a s ha }) => f ↑a_1) ↔ Pairwise (Function.onFun r fun (a : { x : α // x ∈ s }) => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

theorem Finset.pairwise_cons {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (r : α → α → Prop) : Pairwise (Function.onFun r fun (a_1 : { x : α // x ∈ cons a s ha }) => ↑a_1) ↔ Pairwise (Function.onFun r fun (a : { x : α // x ∈ s }) => ↑a) ∧ ∀ b ∈ s, r a b ∧ r b a