Documentation

@[implicit_reducible]

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

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} ≠ ∅

@[simp]

theorem Finset.empty_ne_singleton {α : 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 = ∅

🔹 coverage

@[reducible, inline]

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

Prop

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

Instances For

theorem Finset.nontrivial_def {α : Type u_1} {s : Finset α} :

s.Nontrivial ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

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 α)

@[implicit_reducible]

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

Unique (Finset α)

@[implicit_reducible]

instance Finset.instUniqueSubtypeMemSingleton {α : Type u_1} (i : α) :

Unique ↥{i}

@[simp]

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

↑default = i

@[implicit_reducible]

instance Finset.Nontrivial.instDecidablePred {α : Type u_1} :

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.

Instances For

@[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

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.

Instances For

@[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.

Instances For

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.

Instances For

insert #

@[implicit_reducible]

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

@[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

@[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)

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.instNonemptyElemCoeInsert {α : 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

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

@[simp]

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) :

↥(insert x t) ≃ Option ↥t

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

Instances For

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.

Instances For

@[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.

Instances For

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.

Instances For

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 : ↥(cons a s ha)) => f ↑a_1) ↔ Pairwise (Function.onFun r fun (a : ↥s) => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)