Documentation

Mathlib.Data.Finset.Basic

Basic lemmas on finite sets #

This file contains lemmas on the interaction of various definitions on the Finset type.

For an explanation of Finset design decisions, please see Mathlib/Data/Finset/Defs.lean.

Main declarations #

Main definitions #

Equivalences between finsets #

Tags #

finite sets, finset

Lattice structure #

union #

@[simp]
theorem Finset.disjUnion_eq_union {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) :
s.disjUnion t h = s t
@[simp]
theorem Finset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
@[simp]
theorem Finset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} :

inter #

theorem Finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} :
¬Disjoint s t (s t).Nonempty
theorem Finset.Nonempty.not_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} :
(s t).Nonempty¬Disjoint s t

Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter.

theorem Finset.disjoint_or_nonempty_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
Disjoint s t (s t).Nonempty
theorem Finset.disjoint_of_subset_iff_left_eq_empty {α : Type u_1} {s t : Finset α} (h : s t) :
instance Finset.isDirected_le {α : Type u_1} :
IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 x2
instance Finset.isDirected_subset {α : Type u_1} :
IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 x2

erase #

@[simp]
theorem Finset.erase_empty {α : Type u_1} [DecidableEq α] (a : α) :
.erase a =
theorem Finset.Nontrivial.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nontrivial) :
(s.erase a).Nonempty
@[simp]
theorem Finset.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) :
(s.erase a).Nonempty s.Nontrivial
@[simp]
theorem Finset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) :
{a}.erase a =
@[simp]
theorem Finset.erase_insert_eq_erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
(insert a s).erase a = s.erase a
theorem Finset.erase_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
(insert a s).erase a = s
theorem Finset.erase_insert_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} (h : a b) :
(insert a s).erase b = insert a (s.erase b)
theorem Finset.erase_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} (ha : as) (hb : a b) :
(Finset.cons a s ha).erase b = Finset.cons a (s.erase b)
@[simp]
theorem Finset.insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a s) :
insert a (s.erase a) = s
theorem Finset.erase_eq_iff_eq_insert {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (hs : a s) (ht : at) :
s.erase a = t s = insert a t
theorem Finset.insert_erase_invOn {α : Type u_1} [DecidableEq α] {a : α} :
Set.InvOn (insert a) (fun (s : Finset α) => s.erase a) {s : Finset α | a s} {s : Finset α | as}
theorem Finset.erase_ssubset {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a s) :
s.erase a s
theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s t at, s t.erase a
theorem Finset.erase_ssubset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
s.erase a insert a s
theorem Finset.erase_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : as) :
(Finset.cons a s h).erase a = s
theorem Finset.subset_insert_iff {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} :
s insert a t s.erase a t
theorem Finset.erase_insert_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
(insert a s).erase a s
theorem Finset.insert_erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
s insert a (s.erase a)
theorem Finset.subset_insert_iff_of_not_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : as) :
s insert a t s t
theorem Finset.erase_subset_iff_of_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a t) :
s.erase a t s t
theorem Finset.erase_injOn' {α : Type u_1} [DecidableEq α] (a : α) :
Set.InjOn (fun (s : Finset α) => s.erase a) {s : Finset α | a s}
theorem Finset.Nontrivial.exists_cons_eq {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) :
∃ (t : Finset α) (a : α) (ha : at) (b : α) (hb : bt) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) = s

sdiff #

theorem Finset.erase_sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hab : a b) (hb : b s) :
s.erase a \ s.erase b = {b}
theorem Finset.sdiff_singleton_eq_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
s \ {a} = s.erase a
theorem Finset.erase_eq {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
s.erase a = s \ {a}
theorem Finset.disjoint_erase_comm {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
Disjoint (s.erase a) t Disjoint s (t.erase a)
theorem Finset.disjoint_insert_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : at) :
Disjoint (s.erase a) (insert a t) Disjoint s t
theorem Finset.disjoint_erase_insert {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : as) :
Disjoint (insert a s) (t.erase a) Disjoint s t
theorem Finset.disjoint_of_erase_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : at) (hst : Disjoint (s.erase a) t) :
theorem Finset.disjoint_of_erase_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : as) (hst : Disjoint s (t.erase a)) :
theorem Finset.inter_erase {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) :
s t.erase a = (s t).erase a
@[simp]
theorem Finset.erase_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) :
s.erase a t = (s t).erase a
theorem Finset.erase_sdiff_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
s.erase a \ t = (s \ t).erase a
theorem Finset.erase_inter_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
s.erase a t = s t.erase a
theorem Finset.erase_union_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
(s t).erase a = s.erase a t.erase a
theorem Finset.insert_inter_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
insert a (s t) = insert a s insert a t
theorem Finset.erase_sdiff_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) :
(s \ t).erase a = s.erase a \ t.erase a
theorem Finset.erase_union_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (ha : a t) (s : Finset α) :
s.erase a t = s t
theorem Finset.union_erase_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) (t : Finset α) :
s t.erase a = s t
@[simp, deprecated Finset.erase_eq_of_not_mem]
theorem Finset.sdiff_singleton_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : as) :
s \ {a} = s
theorem Finset.sdiff_union_erase_cancel {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (hts : t s) (ha : a t) :
s \ t t.erase a = s.erase a
theorem Finset.sdiff_insert {α : Type u_1} [DecidableEq α] (s t : Finset α) (x : α) :
s \ insert x t = (s \ t).erase x
theorem Finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {x : α} (hxs : x s) (hxt : xt) :
insert x (s \ insert x t) = s \ t
theorem Finset.sdiff_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a s) :
s \ t.erase a = insert a (s \ t)
theorem Finset.sdiff_erase_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a s) :
s \ s.erase a = {a}
theorem Finset.erase_eq_empty_iff {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
s.erase a = s = s = {a}
theorem Finset.sdiff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} :
Disjoint (t \ s) s
theorem Finset.disjoint_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} :
Disjoint s (t \ s)
theorem Finset.disjoint_sdiff_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
Disjoint (s \ t) (s t)

attach #

@[simp]
theorem Finset.attach_empty {α : Type u_1} :
.attach =
@[simp]
theorem Finset.attach_nonempty_iff {α : Type u_1} {s : Finset α} :
s.attach.Nonempty s.Nonempty
theorem Finset.Nonempty.attach {α : Type u_1} {s : Finset α} :
s.Nonemptys.attach.Nonempty

Alias of the reverse direction of Finset.attach_nonempty_iff.

@[simp]
theorem Finset.attach_eq_empty_iff {α : Type u_1} {s : Finset α} :
s.attach = s =

filter #

theorem Finset.filter_singleton {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) :
Finset.filter p {a} = if p a then {a} else
theorem Finset.filter_cons_of_pos {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (s : Finset α) (ha : as) (hp : p a) :
theorem Finset.filter_cons_of_neg {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (s : Finset α) (ha : as) (hp : ¬p a) :
theorem Finset.disjoint_filter {α : Type u_1} {s : Finset α} {p q : αProp} [DecidablePred p] [DecidablePred q] :
Disjoint (Finset.filter p s) (Finset.filter q s) xs, p x¬q x
theorem Finset.disjoint_filter_filter' {α : Type u_1} (s t : Finset α) {p q : αProp} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) :
theorem Finset.disjoint_filter_filter_neg {α : Type u_1} (s t : Finset α) (p : αProp) [DecidablePred p] [(x : α) → Decidable ¬p x] :
Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)
@[deprecated Finset.disjoint_filter_filter_neg]
theorem Finset.filter_inter_filter_neg_eq {α : Type u_1} (s t : Finset α) (p : αProp) [DecidablePred p] [(x : α) → Decidable ¬p x] :
Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)

Alias of Finset.disjoint_filter_filter_neg.

theorem Finset.filter_disj_union {α : Type u_1} (p : αProp) [DecidablePred p] (s t : Finset α) (h : Disjoint s t) :
Finset.filter p (s.disjUnion t h) = (Finset.filter p s).disjUnion (Finset.filter p t)
theorem Finset.filter_cons {α : Type u_1} (p : αProp) [DecidablePred p] {a : α} (s : Finset α) (ha : as) :
Finset.filter p (Finset.cons a s ha) = if p a then Finset.cons a (Finset.filter p s) else Finset.filter p s
theorem Finset.filter_union {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s₁ s₂ : Finset α) :
Finset.filter p (s₁ s₂) = Finset.filter p s₁ Finset.filter p s₂
theorem Finset.filter_union_right {α : Type u_1} (p q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
Finset.filter p s Finset.filter q s = Finset.filter (fun (x : α) => p x q x) s
theorem Finset.filter_mem_eq_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} [(i : α) → Decidable (i t)] :
Finset.filter (fun (i : α) => i t) s = s t
theorem Finset.filter_inter_distrib {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s t : Finset α) :
theorem Finset.filter_inter {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s t : Finset α) :
theorem Finset.inter_filter {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s t : Finset α) :
theorem Finset.filter_insert {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) :
Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s
theorem Finset.filter_erase {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) :
Finset.filter p (s.erase a) = (Finset.filter p s).erase a
theorem Finset.filter_or {α : Type u_1} (p q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (a : α) => p a q a) s = Finset.filter p s Finset.filter q s
theorem Finset.filter_and {α : Type u_1} (p q : αProp) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (a : α) => p a q a) s = Finset.filter p s Finset.filter q s
theorem Finset.filter_not {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (a : α) => ¬p a) s = s \ Finset.filter p s
theorem Finset.filter_and_not {α : Type u_1} [DecidableEq α] (s : Finset α) (p q : αProp) [DecidablePred p] [DecidablePred q] :
Finset.filter (fun (a : α) => p a ¬q a) s = Finset.filter p s \ Finset.filter q s
theorem Finset.sdiff_eq_filter {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
s₁ \ s₂ = Finset.filter (fun (x : α) => xs₂) s₁
theorem Finset.subset_union_elim {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ t₂ : Set α} (h : s t₁ t₂) :
∃ (s₁ : Finset α) (s₂ : Finset α), s₁ s₂ = s s₁ t₁ s₂ t₂ \ t₁
theorem Finset.filter_eq {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
Finset.filter (Eq b) s = if b s then {b} else

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq' with the equality the other way.

theorem Finset.filter_eq' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
Finset.filter (fun (a : β) => a = b) s = if b s then {b} else

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq with the equality the other way.

theorem Finset.filter_ne {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
Finset.filter (fun (a : β) => b a) s = s.erase b
theorem Finset.filter_ne' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :
Finset.filter (fun (a : β) => a b) s = s.erase b
theorem Finset.filter_union_filter_neg_eq {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] [(x : α) → Decidable ¬p x] (s : Finset α) :
Finset.filter p s Finset.filter (fun (a : α) => ¬p a) s = s

range #

@[simp]
theorem Finset.range_filter_eq {n m : } :
Finset.filter (fun (x : ) => x = m) (Finset.range n) = if m < n then {m} else

dedup on list and multiset #

@[simp]
theorem Multiset.toFinset_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
(s + t).toFinset = s.toFinset t.toFinset
@[simp]
theorem Multiset.toFinset_nsmul {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ) :
n 0(n s).toFinset = s.toFinset
theorem Multiset.toFinset_eq_singleton_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
s.toFinset = {a} s.card 0 s = s.card {a}
@[simp]
theorem Multiset.toFinset_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
(s t).toFinset = s.toFinset t.toFinset
@[simp]
theorem Multiset.toFinset_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
(s t).toFinset = s.toFinset t.toFinset
@[simp]
theorem Multiset.toFinset_eq_empty {α : Type u_1} [DecidableEq α] {m : Multiset α} :
m.toFinset = m = 0
@[simp]
theorem Multiset.toFinset_nonempty {α : Type u_1} [DecidableEq α] {s : Multiset α} :
s.toFinset.Nonempty s 0
theorem Multiset.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] {s : Multiset α} :
s 0s.toFinset.Nonempty

Alias of the reverse direction of Multiset.toFinset_nonempty.

@[simp]
theorem Multiset.toFinset_filter {α : Type u_1} [DecidableEq α] (s : Multiset α) (p : αProp) [DecidablePred p] :
(Multiset.filter p s).toFinset = Finset.filter p s.toFinset
@[simp]
theorem List.toFinset_union {α : Type u_1} [DecidableEq α] (l l' : List α) :
(l l').toFinset = l.toFinset l'.toFinset
@[simp]
theorem List.toFinset_inter {α : Type u_1} [DecidableEq α] (l l' : List α) :
(l l').toFinset = l.toFinset l'.toFinset
theorem List.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] (l : List α) :
l []l.toFinset.Nonempty

Alias of the reverse direction of List.toFinset_nonempty_iff.

@[simp]
theorem List.toFinset_filter {α : Type u_1} [DecidableEq α] (s : List α) (p : αBool) :
(List.filter p s).toFinset = Finset.filter (fun (x : α) => p x = true) s.toFinset
@[simp]
theorem Finset.toList_eq_nil {α : Type u_1} {s : Finset α} :
s.toList = [] s =
theorem Finset.empty_toList {α : Type u_1} {s : Finset α} :
s.toList.isEmpty = true s =
@[simp]
theorem Finset.toList_empty {α : Type u_1} :
.toList = []
theorem Finset.Nonempty.toList_ne_nil {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :
s.toList []
theorem Finset.Nonempty.not_empty_toList {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :
¬s.toList.isEmpty = true

choose #

def Finset.chooseX {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a l p a) :
{ a : α // a l p a }

Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the corresponding subtype.

Equations
Instances For
    def Finset.choose {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a l p a) :
    α

    Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the ambient type.

    Equations
    Instances For
      theorem Finset.choose_spec {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a l p a) :
      Finset.choose p l hp l p (Finset.choose p l hp)
      theorem Finset.choose_mem {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a l p a) :
      theorem Finset.choose_property {α : Type u_1} (p : αProp) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a l p a) :
      p (Finset.choose p l hp)
      def Equiv.Finset.union {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) :
      { x : α // x s } { x : α // x t } { x : α // x s t }

      The disjoint union of finsets is a sum

      Equations
      Instances For
        @[simp]
        theorem Equiv.Finset.union_symm_inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : { x : α // x s }) :
        (Equiv.Finset.union s t h) (Sum.inl x) = x,
        @[simp]
        theorem Equiv.Finset.union_symm_inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : { x : α // x t }) :
        (Equiv.Finset.union s t h) (Sum.inr y) = y,
        def Equiv.piFinsetUnion {ι : Type u_5} [DecidableEq ι] (α : ιType u_4) {s t : Finset ι} (h : Disjoint s t) :
        ((i : { x : ι // x s }) → α i) × ((i : { x : ι // x t }) → α i) ((i : { x : ι // x s t }) → α i)

        The type of dependent functions on the disjoint union of finsets s ∪ t is equivalent to the type of pairs of functions on s and on t. This is similar to Equiv.sumPiEquivProdPi.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Multiset.toFinset_replicate {α : Type u_1} [DecidableEq α] (n : ) (a : α) :
          (Multiset.replicate n a).toFinset = if n = 0 then else {a}