mathlib documentation

data.finset.basic

Finite sets

mathlib has several different models for finite sets, and it can be confusing when you're first getting used to them!

This file builds the basic theory of finset α, modelled as a multiset α without duplicates.

It's "constructive" in the since that there is an underlying list of elements, although this is wrapped in a quotient by permutations, so anytime you actually use this list you're obligated to show you didn't depend on the ordering.

There's also the typeclass fintype α (which asserts that there is some finset α containing every term of type α) as well as the predicate finite on s : set α (which asserts nonempty (fintype s)).

structure finset  :
Type u_4Type u_4

finset α is the type of finite sets of elements of α. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

theorem finset.eq_of_veq {α : Type u_1} {s t : finset α} :
s.val = t.vals = t

@[simp]
theorem finset.val_inj {α : Type u_1} {s t : finset α} :
s.val = t.val s = t

@[simp]
theorem finset.erase_dup_eq_self {α : Type u_1} [decidable_eq α] (s : finset α) :

@[instance]
def finset.has_decidable_eq {α : Type u_1} [decidable_eq α] :

Equations

membership

@[instance]
def finset.has_mem {α : Type u_1} :
has_mem α (finset α)

Equations
theorem finset.mem_def {α : Type u_1} {a : α} {s : finset α} :
a s a s.val

@[simp]
theorem finset.mem_mk {α : Type u_1} {a : α} {s : multiset α} {nd : s.nodup} :
a {val := s, nodup := nd} a s

@[instance]
def finset.decidable_mem {α : Type u_1} [h : decidable_eq α] (a : α) (s : finset α) :

Equations

set coercion

@[instance]
def finset.set.has_lift {α : Type u_1} :
has_lift (finset α) (set α)

Convert a finset to a set in the natural way.

Equations
@[simp]
theorem finset.mem_coe {α : Type u_1} {a : α} {s : finset α} :
a s a s

@[simp]
theorem finset.set_of_mem {α : Type u_1} {s : finset α} :
{a : α | a s} = s

@[simp]
theorem finset.coe_mem {α : Type u_1} {s : finset α} (x : s) :
x s

@[simp]
theorem finset.mk_coe {α : Type u_1} {s : finset α} (x : s) {h : x s} :
x, h⟩ = x

@[instance]
def finset.decidable_mem' {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

Equations

extensionality

theorem finset.ext_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ ∀ (a : α), a s₁ a s₂

@[ext]
theorem finset.ext {α : Type u_1} {s₁ s₂ : finset α} :
(∀ (a : α), a s₁ a s₂)s₁ = s₂

@[simp]
theorem finset.coe_inj {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ s₁ = s₂

theorem finset.coe_injective {α : Type u_1} :

subset

@[instance]
def finset.has_subset {α : Type u_1} :

Equations
theorem finset.subset_def {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁.val s₂.val

@[simp]
theorem finset.subset.refl {α : Type u_1} (s : finset α) :
s s

theorem finset.subset_of_eq {α : Type u_1} {s t : finset α} :
s = ts t

theorem finset.subset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ s₂s₂ s₃s₁ s₃

theorem finset.superset.trans {α : Type u_1} {s₁ s₂ s₃ : finset α} :
s₁ s₂s₂ s₃s₁ s₃

theorem finset.mem_of_subset {α : Type u_1} {s₁ s₂ : finset α} {a : α} :
s₁ s₂a s₁a s₂

theorem finset.subset.antisymm {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂s₂ s₁s₁ = s₂

theorem finset.subset_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ ∀ ⦃x : α⦄, x s₁x s₂

@[simp]
theorem finset.coe_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂

@[simp]
theorem finset.val_le_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val s₂.val s₁ s₂

@[instance]
def finset.has_ssubset {α : Type u_1} :

Equations
theorem finset.subset.antisymm_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁ = s₂ s₁ s₂ s₂ s₁

@[simp]
theorem finset.le_iff_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂

@[simp]
theorem finset.lt_iff_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ < s₂ s₁ s₂

@[simp]
theorem finset.coe_ssubset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂ s₁ s₂

@[simp]
theorem finset.val_lt_iff {α : Type u_1} {s₁ s₂ : finset α} :
s₁.val < s₂.val s₁ s₂

theorem finset.ssubset_iff_of_subset {α : Type u_1} {s₁ s₂ : finset α} :
s₁ s₂(s₁ s₂ ∃ (x : α) (H : x s₂), x s₁)

Nonempty

def finset.nonempty {α : Type u_1} :
finset α → Prop

The property s.nonempty expresses the fact that the finset s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Equations
@[simp]
theorem finset.coe_nonempty {α : Type u_1} {s : finset α} :

theorem finset.nonempty.bex {α : Type u_1} {s : finset α} :
s.nonempty(∃ (x : α), x s)

theorem finset.nonempty.mono {α : Type u_1} {s t : finset α} :
s ts.nonempty → t.nonempty

empty

def finset.empty {α : Type u_1} :

The empty finset

Equations
@[instance]
def finset.has_emptyc {α : Type u_1} :

Equations
@[instance]
def finset.inhabited {α : Type u_1} :

Equations
@[simp]
theorem finset.empty_val {α : Type u_1} :

@[simp]
theorem finset.not_mem_empty {α : Type u_1} (a : α) :

@[simp]
theorem finset.not_nonempty_empty {α : Type u_1} :

@[simp]
theorem finset.mk_zero {α : Type u_1} :
{val := 0, nodup := _} =

theorem finset.ne_empty_of_mem {α : Type u_1} {a : α} {s : finset α} :
a ss

theorem finset.nonempty.ne_empty {α : Type u_1} {s : finset α} :
s.nonemptys

@[simp]
theorem finset.empty_subset {α : Type u_1} (s : finset α) :

theorem finset.eq_empty_of_forall_not_mem {α : Type u_1} {s : finset α} :
(∀ (x : α), x s)s =

theorem finset.eq_empty_iff_forall_not_mem {α : Type u_1} {s : finset α} :
s = ∀ (x : α), x s

@[simp]
theorem finset.val_eq_zero {α : Type u_1} {s : finset α} :
s.val = 0 s =

theorem finset.subset_empty {α : Type u_1} {s : finset α} :

theorem finset.nonempty_of_ne_empty {α : Type u_1} {s : finset α} :
s → s.nonempty

theorem finset.nonempty_iff_ne_empty {α : Type u_1} {s : finset α} :

theorem finset.eq_empty_or_nonempty {α : Type u_1} (s : finset α) :

@[simp]
theorem finset.coe_empty {α : Type u_1} :

theorem finset.eq_empty_of_not_nonempty {α : Type u_1} (h : ¬nonempty α) (s : finset α) :
s =

A finset for an empty type is empty.

singleton

@[instance]
def finset.has_singleton {α : Type u_1} :

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

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

Equations
@[simp]
theorem finset.singleton_val {α : Type u_1} (a : α) :
{a}.val = a ::ₘ 0

@[simp]
theorem finset.mem_singleton {α : Type u_1} {a b : α} :
b {a} b = a

theorem finset.not_mem_singleton {α : Type u_1} {a b : α} :
a {b} a b

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

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

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

@[simp]
theorem finset.singleton_ne_empty {α : Type u_1} (a : α) :
{a}

@[simp]
theorem finset.coe_singleton {α : Type u_1} (a : α) :
{a} = {a}

theorem finset.eq_singleton_iff_unique_mem {α : Type u_1} {s : finset α} {a : α} :
s = {a} a s ∀ (x : α), x sx = a

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

cons

def finset.cons {α : Type u_1} (a : α) (s : finset α) :
a sfinset α

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 decidable_eq α, and the union is guaranteed to be disjoint.

Equations
@[simp]
theorem finset.mem_cons {α : Type u_1} {a : α} {s : finset α} {h : a s} {b : α} :
b finset.cons a s h b = a b s

@[simp]
theorem finset.cons_val {α : Type u_1} {a : α} {s : finset α} (h : a s) :
(finset.cons a s h).val = a ::ₘ s.val

@[simp]
theorem finset.mk_cons {α : Type u_1} {a : α} {s : multiset α} (h : (a ::ₘ s).nodup) :
{val := a ::ₘ s, nodup := h} = finset.cons a {val := s, nodup := _} _

@[simp]
theorem finset.nonempty_cons {α : Type u_1} {a : α} {s : finset α} (h : a s) :

@[simp]
theorem finset.nonempty_mk_coe {α : Type u_1} {l : list α} {hl : l.nodup} :

disjoint union

def finset.disj_union {α : Type u_1} (s t : finset α) :
(∀ (a : α), a sa t)finset α

disj_union s t h is the set such that a ∈ disj_union s t h iff a ∈ s or a ∈ t. It is the same as s ∪ t, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

Equations
@[simp]
theorem finset.mem_disj_union {α : Type u_1} {s t : finset α} {h : ∀ (a : α), a sa t} {a : α} :
a s.disj_union t h a s a t

insert

@[instance]
def finset.has_insert {α : Type u_1} [decidable_eq α] :

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

Equations
theorem finset.insert_def {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

@[simp]
theorem finset.insert_val {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

theorem finset.insert_val' {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

theorem finset.insert_val_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(insert a s).val = a ::ₘ s.val

@[simp]
theorem finset.mem_insert {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a insert b s a = b a s

theorem finset.mem_insert_self {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a insert a s

theorem finset.mem_insert_of_mem {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a sa insert b s

theorem finset.mem_of_mem_insert_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
b insert a sb ab s

@[simp]
theorem finset.cons_eq_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) (h : a s) :
finset.cons a s h = insert a s

@[simp]
theorem finset.coe_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

@[simp]
theorem finset.insert_eq_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a sinsert a s = s

@[simp]
theorem finset.insert_singleton_self_eq {α : Type u_1} [decidable_eq α] (a : α) :
{a, a} = {a}

theorem finset.insert.comm {α : Type u_1} [decidable_eq α] (a b : α) (s : finset α) :
insert a (insert b s) = insert b (insert a s)

theorem finset.insert_singleton_comm {α : Type u_1} [decidable_eq α] (a b : α) :
{a, b} = {b, a}

@[simp]
theorem finset.insert_idem {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
insert a (insert a s) = insert a s

@[simp]
theorem finset.insert_ne_empty {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :

theorem finset.ne_insert_of_not_mem {α : Type u_1} [decidable_eq α] (s t : finset α) {a : α} :
a ss insert a t

theorem finset.insert_subset {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :
insert a s t a t s t

theorem finset.subset_insert {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s insert a s

theorem finset.insert_subset_insert {α : Type u_1} [decidable_eq α] (a : α) {s t : finset α} :
s tinsert a s insert a t

theorem finset.ssubset_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t ∃ (a : α) (H : a s), insert a s t

theorem finset.ssubset_insert {α : Type u_1} [decidable_eq α] {s : finset α} {a : α} :
a ss insert a s

theorem finset.induction {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (h₁ : p ) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a sp sp (insert a s)) (s : finset α) :
p s

theorem finset.induction_on {α : Type u_1} {p : finset α → Prop} [decidable_eq α] (s : finset α) :
p (∀ ⦃a : α⦄ {s : finset α}, a sp sp (insert a s))p 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.

def finset.subtype_insert_equiv_option {α : Type u_1} [decidable_eq α] {t : finset α} {x : α} :
x t{i // i insert x t} option {i // i t}

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

Equations

union

@[instance]
def finset.has_union {α : Type u_1} [decidable_eq α] :

s ∪ t is the set such that a ∈ s ∪ t iff a ∈ s or a ∈ t.

Equations
theorem finset.union_val_nd {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val.ndunion s₂.val

@[simp]
theorem finset.union_val {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val s₂.val

@[simp]
theorem finset.mem_union {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂ a s₁ a s₂

@[simp]
theorem finset.disj_union_eq_union {α : Type u_1} [decidable_eq α] (s t : finset α) (h : ∀ (a : α), a sa t) :
s.disj_union t h = s t

theorem finset.mem_union_left {α : Type u_1} [decidable_eq α] {a : α} {s₁ : finset α} (s₂ : finset α) :
a s₁a s₁ s₂

theorem finset.mem_union_right {α : Type u_1} [decidable_eq α] {a : α} {s₂ : finset α} (s₁ : finset α) :
a s₂a s₁ s₂

theorem finset.not_mem_union {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂ a s₁ a s₂

@[simp]
theorem finset.coe_union {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂

theorem finset.union_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ s₃ : finset α} :
s₁ s₃s₂ s₃s₁ s₂ s₃

theorem finset.subset_union_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₁ s₂

theorem finset.subset_union_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₂ s₁ s₂

theorem finset.union_subset_union {α : Type u_1} [decidable_eq α] {s1 t1 s2 t2 : finset α} :
s1 t1s2 t2s1 s2 t1 t2

theorem finset.union_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ = s₂ s₁

@[simp]
theorem finset.union_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ (s₂ s₃)

@[simp]
theorem finset.union_idempotent {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s

theorem finset.union_left_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)

theorem finset.union_right_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ s₃ s₂

theorem finset.union_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s

@[simp]
theorem finset.union_empty {α : Type u_1} [decidable_eq α] (s : finset α) :
s = s

@[simp]
theorem finset.empty_union {α : Type u_1} [decidable_eq α] (s : finset α) :
s = s

theorem finset.insert_eq {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
insert a s = {a} s

@[simp]
theorem finset.insert_union {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
insert a s t = insert a (s t)

@[simp]
theorem finset.union_insert {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
s insert a t = insert a (s t)

theorem finset.insert_union_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : finset α) :
insert a (s t) = insert a s insert a t

@[simp]
theorem finset.union_eq_left_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t = s t s

@[simp]
theorem finset.left_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = s t t s

@[simp]
theorem finset.union_eq_right_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
t s = s t s

@[simp]
theorem finset.right_eq_union_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s = t s t s

inter

@[instance]
def finset.has_inter {α : Type u_1} [decidable_eq α] :

s ∩ t is the set such that a ∈ s ∩ t iff a ∈ s and a ∈ t.

Equations
theorem finset.inter_val_nd {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val.ndinter s₂.val

@[simp]
theorem finset.inter_val {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂).val = s₁.val s₂.val

@[simp]
theorem finset.mem_inter {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂ a s₁ a s₂

theorem finset.mem_of_mem_inter_left {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂a s₁

theorem finset.mem_of_mem_inter_right {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ s₂a s₂

theorem finset.mem_inter_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁a s₂a s₁ s₂

theorem finset.inter_subset_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ s₁

theorem finset.inter_subset_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ s₂

theorem finset.subset_inter {α : Type u_1} [decidable_eq α] {s₁ s₂ s₃ : finset α} :
s₁ s₂s₁ s₃s₁ s₂ s₃

@[simp]
theorem finset.coe_inter {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ s₂) = s₁ s₂

@[simp]
theorem finset.union_inter_cancel_left {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s t) s = s

@[simp]
theorem finset.union_inter_cancel_right {α : Type u_1} [decidable_eq α] {s t : finset α} :
(s t) t = t

theorem finset.inter_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ = s₂ s₁

@[simp]
theorem finset.inter_assoc {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ (s₂ s₃)

theorem finset.inter_left_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)

theorem finset.inter_right_comm {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ s₂ s₃ = s₁ s₃ s₂

@[simp]
theorem finset.inter_self {α : Type u_1} [decidable_eq α] (s : finset α) :
s s = s

@[simp]
theorem finset.inter_empty {α : Type u_1} [decidable_eq α] (s : finset α) :

@[simp]
theorem finset.empty_inter {α : Type u_1} [decidable_eq α] (s : finset α) :

@[simp]
theorem finset.inter_union_self {α : Type u_1} [decidable_eq α] (s t : finset α) :
s (t s) = s

@[simp]
theorem finset.insert_inter_of_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} :
a s₂insert a s₁ s₂ = insert a (s₁ s₂)

@[simp]
theorem finset.inter_insert_of_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} :
a s₁s₁ insert a s₂ = insert a (s₁ s₂)

@[simp]
theorem finset.insert_inter_of_not_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} :
a s₂insert a s₁ s₂ = s₁ s₂

@[simp]
theorem finset.inter_insert_of_not_mem {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} {a : α} :
a s₁s₁ insert a s₂ = s₁ s₂

@[simp]
theorem finset.singleton_inter_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s{a} s = {a}

@[simp]
theorem finset.singleton_inter_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s{a} s =

@[simp]
theorem finset.inter_singleton_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a ss {a} = {a}

@[simp]
theorem finset.inter_singleton_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a ss {a} =

theorem finset.inter_subset_inter {α : Type u_1} [decidable_eq α] {x y s t : finset α} :
x ys tx s y t

theorem finset.inter_subset_inter_right {α : Type u_1} [decidable_eq α] {x y s : finset α} :
x yx s y s

theorem finset.inter_subset_inter_left {α : Type u_1} [decidable_eq α] {x y s : finset α} :
x ys x s y

lattice laws

@[simp]
theorem finset.sup_eq_union {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t = s t

@[simp]
theorem finset.inf_eq_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
s t = s t

theorem finset.inter_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t u) = s t s u

theorem finset.inter_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
(s t) u = s u t u

theorem finset.union_distrib_left {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = (s t) (s u)

theorem finset.union_distrib_right {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s t u = (s u) (t u)

theorem finset.union_eq_empty_iff {α : Type u_1} [decidable_eq α] (A B : finset α) :
A B = A = B =

erase

def finset.erase {α : Type u_1} [decidable_eq α] :
finset αα → finset α

erase s a is the set s - {a}, that is, the elements of s which are not equal to a.

Equations
@[simp]
theorem finset.erase_val {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
(s.erase a).val = s.val.erase a

@[simp]
theorem finset.mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a s.erase b a b a s

theorem finset.not_mem_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
a s.erase a

@[simp]
theorem finset.erase_empty {α : Type u_1} [decidable_eq α] (a : α) :

theorem finset.ne_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
b s.erase ab a

theorem finset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
b s.erase ab s

theorem finset.mem_erase_of_ne_of_mem {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
a ba sa s.erase b

theorem finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : finset α} :
b sb s.erase ab = a

An element of s that is not an element of erase s a must be a.

theorem finset.erase_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(insert a s).erase a = s

theorem finset.insert_erase {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a sinsert a (s.erase a) = s

theorem finset.erase_subset_erase {α : Type u_1} [decidable_eq α] (a : α) {s t : finset α} :
s ts.erase a t.erase a

theorem finset.erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s.erase a s

@[simp]
theorem finset.coe_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(s.erase a) = s \ {a}

theorem finset.erase_ssubset {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a ss.erase a s

theorem finset.erase_eq_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a ss.erase a = s

theorem finset.subset_insert_iff {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :
s insert a t s.erase a t

theorem finset.erase_insert_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(insert a s).erase a s

theorem finset.insert_erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s insert a (s.erase a)

sdiff

@[instance]
def finset.has_sdiff {α : Type u_1} [decidable_eq α] :

s \ t is the set consisting of the elements of s that are not in t.

Equations
@[simp]
theorem finset.mem_sdiff {α : Type u_1} [decidable_eq α] {a : α} {s₁ s₂ : finset α} :
a s₁ \ s₂ a s₁ a s₂

theorem finset.not_mem_sdiff_of_mem_right {α : Type u_1} [decidable_eq α] {a : α} {s t : finset α} :
a ta s \ t

theorem finset.sdiff_union_of_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :
s₁ s₂s₂ \ s₁ s₁ = s₂

theorem finset.union_sdiff_of_subset {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :
s₁ s₂s₁ s₂ \ s₁ = s₂

theorem finset.inter_sdiff {α : Type u_1} [decidable_eq α] (s t u : finset α) :
s (t \ u) = s t \ u

@[simp]
theorem finset.inter_sdiff_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ (s₂ \ s₁) =

@[simp]
theorem finset.sdiff_inter_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₂ \ s₁ s₁ =

@[simp]
theorem finset.sdiff_self {α : Type u_1} [decidable_eq α] (s₁ : finset α) :
s₁ \ s₁ =

theorem finset.sdiff_inter_distrib_right {α : Type u_1} [decidable_eq α] (s₁ s₂ s₃ : finset α) :
s₁ \ (s₂ s₃) = s₁ \ s₂ s₁ \ s₃

@[simp]
theorem finset.sdiff_inter_self_left {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ (s₁ s₂) = s₁ \ s₂

@[simp]
theorem finset.sdiff_inter_self_right {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ (s₂ s₁) = s₁ \ s₂

theorem finset.inter_eq_sdiff_sdiff {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ s₂ = s₁ \ (s₁ \ s₂)

@[simp]
theorem finset.sdiff_empty {α : Type u_1} [decidable_eq α] {s₁ : finset α} :
s₁ \ = s₁

theorem finset.sdiff_subset_sdiff {α : Type u_1} [decidable_eq α] {s₁ s₂ t₁ t₂ : finset α} :
t₁ t₂s₂ s₁t₁ \ s₁ t₂ \ s₂

theorem finset.sdiff_subset_self {α : Type u_1} [decidable_eq α] {s₁ s₂ : finset α} :
s₁ \ s₂ s₁

@[simp]
theorem finset.coe_sdiff {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
(s₁ \ s₂) = s₁ \ s₂

@[simp]
theorem finset.union_sdiff_self_eq_union {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t \ s = s t

@[simp]
theorem finset.sdiff_union_self_eq_union {α : Type u_1} [decidable_eq α] {s t : finset α} :
s \ t t = s t

theorem finset.union_sdiff_symm {α : Type u_1} [decidable_eq α] {s t : finset α} :
s t \ s = t s \ t

theorem finset.sdiff_union_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t s t = s

@[simp]
theorem finset.sdiff_idem {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t \ t = s \ t

theorem finset.sdiff_eq_empty_iff_subset {α : Type u_1} [decidable_eq α] {s t : finset α} :
s \ t = s t

@[simp]
theorem finset.empty_sdiff {α : Type u_1} [decidable_eq α] (s : finset α) :

theorem finset.insert_sdiff_of_not_mem {α : Type u_1} [decidable_eq α] (s : finset α) {t : finset α} {x : α} :
x tinsert x s \ t = insert x (s \ t)

theorem finset.insert_sdiff_of_mem {α : Type u_1} [decidable_eq α] (s : finset α) {t : finset α} {x : α} :
x tinsert x s \ t = s \ t

@[simp]
theorem finset.sdiff_subset {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ t s

theorem finset.union_sdiff_distrib {α : Type u_1} [decidable_eq α] (s₁ s₂ t : finset α) :
(s₁ s₂) \ t = s₁ \ t s₂ \ t

theorem finset.sdiff_union_distrib {α : Type u_1} [decidable_eq α] (s t₁ t₂ : finset α) :
s \ (t₁ t₂) = s \ t₁ (s \ t₂)

theorem finset.union_sdiff_self {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t) \ t = s \ t

theorem finset.sdiff_singleton_eq_erase {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
s \ {a} = s.erase a

theorem finset.sdiff_sdiff_self_left {α : Type u_1} [decidable_eq α] (s t : finset α) :
s \ (s \ t) = s t

theorem finset.inter_eq_inter_of_sdiff_eq_sdiff {α : Type u_1} [decidable_eq α] {s t₁ t₂ : finset α} :
s \ t₁ = s \ t₂s t₁ = s t₂

attach

def finset.attach {α : Type u_1} (s : finset α) :
finset {x // x s}

attach s takes the elements of s and forms a new set of elements of the subtype {x // x ∈ s}.

Equations
theorem finset.sizeof_lt_sizeof_of_mem {α : Type u_1} [has_sizeof α] {x : α} {s : finset α} :
x ssizeof x < sizeof s

@[simp]
theorem finset.attach_val {α : Type u_1} (s : finset α) :

@[simp]
theorem finset.mem_attach {α : Type u_1} (s : finset α) (x : {x // x s}) :

@[simp]
theorem finset.attach_empty {α : Type u_1} :

piecewise

def finset.piecewise {α : Type u_1} {δ : α → Sort u_2} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] (i : α) :
δ i

s.piecewise f g is the function equal to f on the finset s, and to g on its complement.

Equations
@[simp]
theorem finset.piecewise_insert_self {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [decidable_eq α] {j : α} [Π (i : α), decidable (i insert j s)] :
(insert j s).piecewise f g j = f j

@[simp]
theorem finset.piecewise_empty {α : Type u_1} {δ : α → Sort u_4} (f g : Π (i : α), δ i) [Π (i : α), decidable (i )] :

theorem finset.piecewise_coe {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] [Π (j : α), decidable (j s)] :

@[simp]
theorem finset.piecewise_eq_of_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {i : α} :
i ss.piecewise f g i = f i

@[simp]
theorem finset.piecewise_eq_of_not_mem {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {i : α} :
i ss.piecewise f g i = g i

@[simp]
theorem finset.piecewise_insert_of_ne {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] [decidable_eq α] {i j : α} [Π (i : α), decidable (i insert j s)] :
i j(insert j s).piecewise f g i = s.piecewise f g i

theorem finset.piecewise_insert {α : Type u_1} {δ : α → Sort u_4} (s : finset α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] [decidable_eq α] (j : α) [Π (i : α), decidable (i insert j s)] :
(insert j s).piecewise f g = function.update (s.piecewise f g) j (f j)

theorem finset.update_eq_piecewise {α : Type u_1} {β : Type u_2} [decidable_eq α] (f : α → β) (i : α) (v : β) :
function.update f i v = {i}.piecewise (λ (j : α), v) f

@[instance]
def finset.decidable_dforall_finset {α : Type u_1} {s : finset α} {p : Π (a : α), a s → Prop} [hp : Π (a : α) (h : a s), decidable (p a h)] :
decidable (∀ (a : α) (h : a s), p a h)

Equations
@[instance]
def finset.decidable_eq_pi_finset {α : Type u_1} {s : finset α} {β : α → Type u_2} [h : Π (a : α), decidable_eq (β a)] :
decidable_eq (Π (a : α), a sβ a)

decidable equality for functions whose domain is bounded by finsets

Equations
@[instance]
def finset.decidable_dexists_finset {α : Type u_1} {s : finset α} {p : Π (a : α), a s → Prop} [hp : Π (a : α) (h : a s), decidable (p a h)] :
decidable (∃ (a : α) (h : a s), p a h)

Equations

filter

def finset.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] :
finset αfinset α

filter p s is the set of elements of s that satisfy p.

Equations
@[simp]
theorem finset.filter_val {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : finset α) :

@[simp]
theorem finset.mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : α} :
a finset.filter p s a s p a

@[simp]
theorem finset.filter_subset {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : finset α) :

theorem finset.filter_ssubset {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.filter p s s ∃ (x : α) (H : x s), ¬p x

theorem finset.filter_filter {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] (s : finset α) :
finset.filter q (finset.filter p s) = finset.filter (λ (a : α), p a q a) s

theorem finset.filter_true {α : Type u_1} {s : finset α} [h : decidable_pred (λ (_x : α), true)] :
finset.filter (λ (_x : α), true) s = s

@[simp]
theorem finset.filter_false {α : Type u_1} {h : decidable_pred (λ (a : α), false)} (s : finset α) :
finset.filter (λ (a : α), false) s =

@[simp]
theorem finset.filter_true_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
(∀ (x : α), x sp x)finset.filter p s = s

If all elements of a finset satisfy the predicate p, s.filter p is s.

theorem finset.filter_false_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
(∀ (x : α), x s¬p x)finset.filter p s =

If all elements of a finset fail to satisfy the predicate p, s.filter p is .

theorem finset.filter_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {s : finset α} :
(∀ (x : α), x s(p x q x))finset.filter p s = finset.filter q s

theorem finset.filter_empty {α : Type u_1} {p : α → Prop} [decidable_pred p] :

theorem finset.filter_subset_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s t : finset α} :

@[simp]
theorem finset.coe_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : finset α) :
(finset.filter p s) = {x ∈ s | p x}

theorem finset.filter_singleton {α : Type u_1} {p : α → Prop} [decidable_pred p] (a : α) :
finset.filter p {a} = ite (p a) {a}

theorem finset.filter_union {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s₁ s₂ : finset α) :
finset.filter p (s₁ s₂) = finset.filter p s₁ finset.filter p s₂

theorem finset.filter_union_right {α : Type u_1} [decidable_eq α] (p q : α → Prop) [decidable_pred p] [decidable_pred q] (s : finset α) :
finset.filter p s finset.filter q s = finset.filter (λ (x : α), p x q x) s

theorem finset.filter_mem_eq_inter {α : Type u_1} [decidable_eq α] {s t : finset α} [Π (i : α), decidable (i t)] :
finset.filter (λ (i : α), i t) s = s t

theorem finset.filter_inter {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] {s t : finset α} :

theorem finset.inter_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] {s t : finset α} :

theorem finset.filter_insert {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (a : α) (s : finset α) :

theorem finset.filter_or {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] [decidable_eq α] [decidable_pred (λ (a : α), p a q a)] (s : finset α) :
finset.filter (λ (a : α), p a q a) s = finset.filter p s finset.filter q s

theorem finset.filter_and {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] [decidable_eq α] [decidable_pred (λ (a : α), p a q a)] (s : finset α) :
finset.filter (λ (a : α), p a q a) s = finset.filter p s finset.filter q s

theorem finset.filter_not {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] [decidable_pred (λ (a : α), ¬p a)] (s : finset α) :
finset.filter (λ (a : α), ¬p a) s = s \ finset.filter p s

theorem finset.sdiff_eq_filter {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ s₂ = finset.filter (λ (_x : α), _x s₂) s₁

theorem finset.sdiff_eq_self {α : Type u_1} [decidable_eq α] (s₁ s₂ : finset α) :
s₁ \ s₂ = s₁ s₁ s₂

theorem finset.filter_union_filter_neg_eq {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] [decidable_pred (λ (a : α), ¬p a)] (s : finset α) :
finset.filter p s finset.filter (λ (a : α), ¬p a) s = s

theorem finset.filter_inter_filter_neg_eq {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s : finset α) :
finset.filter p s finset.filter (λ (a : α), ¬p a) s =

theorem finset.subset_union_elim {α : Type u_1} [decidable_eq α] {s : finset α} {t₁ t₂ : set α} :
s t₁ t₂(∃ (s₁ s₂ : finset α), s₁ s₂ = s s₁ t₁ s₂ t₂ \ t₁)

@[simp]
theorem finset.filter_congr_decidable {α : Type u_1} (s : finset α) (p : α → Prop) (h : decidable_pred p) [decidable_pred p] :

@[instance]
def finset.has_sep {α : Type u_1} :
has_sep α (finset α)

The following instance allows us to write { x ∈ s | p x } for finset.filter s p. Since the former notation requires us to define this for all propositions p, and finset.filter only works for decidable propositions, the notation { x ∈ s | p x } is only compatible with classical logic because it uses classical.prop_decidable. We don't want to redo all lemmas of finset.filter for has_sep.sep, so we make sure that simp unfolds the notation { x ∈ s | p x } to finset.filter s p. If p happens to be decidable, the simp-lemma filter_congr_decidable will make sure that finset.filter uses the right instance for decidability.

Equations
@[simp]
theorem finset.sep_def {α : Type u_1} (s : finset α) (p : α → Prop) :
{x ∈ s | p x} = finset.filter p s

theorem finset.filter_eq {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (eq b) s = ite (b s) {b}

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} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), a = b) s = ite (b s) {b}

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} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), b a) s = s.erase b

theorem finset.filter_ne' {β : Type u_2} [decidable_eq β] (s : finset β) (b : β) :
finset.filter (λ (a : β), a b) s = s.erase b

range

def finset.range  :

range n is the set of natural numbers less than n.

Equations
@[simp]

@[simp]
theorem finset.mem_range {n m : } :

@[simp]

@[simp]
theorem finset.range_one  :

@[simp]

@[simp]
theorem finset.self_mem_range_succ (n : ) :

@[simp]

theorem finset.exists_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∃ (x : α), x p x) false

theorem finset.exists_mem_insert {α : Type u_1} [d : decidable_eq α] (a : α) (s : finset α) (p : α → Prop) :
(∃ (x : α), x insert a s p x) p a ∃ (x : α), x s p x

theorem finset.forall_mem_empty_iff {α : Type u_1} (p : α → Prop) :
(∀ (x : α), x p x) true

theorem finset.forall_mem_insert {α : Type u_1} [d : decidable_eq α] (a : α) (s : finset α) (p : α → Prop) :
(∀ (x : α), x insert a sp x) p a ∀ (x : α), x sp x

def not_mem_range_equiv (k : ) :

Equivalence between the set of natural numbers which are ≥ k and , given by n → n - k.

Equations
@[simp]
theorem coe_not_mem_range_equiv (k : ) :
(not_mem_range_equiv k) = λ (i : {n // n multiset.range k}), i - k

@[simp]
theorem coe_not_mem_range_equiv_symm (k : ) :
((not_mem_range_equiv k).symm) = λ (j : ), j + k, _⟩

def option.to_finset {α : Type u_1} :
option αfinset α

Construct an empty or singleton finset from an option

Equations
  • o.to_finset = option.to_finset._match_1 o
  • option.to_finset._match_1 (some a) = {a}
  • option.to_finset._match_1 none =
@[simp]
theorem option.to_finset_none {α : Type u_1} :

@[simp]
theorem option.to_finset_some {α : Type u_1} {a : α} :
(some a).to_finset = {a}

@[simp]
theorem option.mem_to_finset {α : Type u_1} {a : α} {o : option α} :

erase_dup on list and multiset

def multiset.to_finset {α : Type u_1} [decidable_eq α] :
multiset αfinset α

to_finset s removes duplicates from the multiset s to produce a finset.

Equations
@[simp]
theorem multiset.to_finset_val {α : Type u_1} [decidable_eq α] (s : multiset α) :

theorem multiset.to_finset_eq {α : Type u_1} [decidable_eq α] {s : multiset α} (n : s.nodup) :
{val := s, nodup := n} = s.to_finset

@[simp]
theorem multiset.mem_to_finset {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

@[simp]
theorem multiset.to_finset_zero {α : Type u_1} [decidable_eq α] :

@[simp]
theorem multiset.to_finset_cons {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

@[simp]
theorem multiset.to_finset_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :

@[simp]
theorem multiset.to_finset_nsmul {α : Type u_1} [decidable_eq α] (s : multiset α) (n : ) :
n 0(n •ℕ s).to_finset = s.to_finset

@[simp]
theorem multiset.to_finset_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :

@[simp]
theorem multiset.to_finset_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :

theorem multiset.to_finset_eq_empty {α : Type u_1} [decidable_eq α] {m : multiset α} :

@[simp]
theorem multiset.to_finset_subset {α : Type u_1} [decidable_eq α] (m1 m2 : multiset α) :

def list.to_finset {α : Type u_1} [decidable_eq α] :
list αfinset α

to_finset l removes duplicates from the list l to produce a finset.

Equations
@[simp]
theorem list.to_finset_val {α : Type u_1} [decidable_eq α] (l : list α) :

theorem list.to_finset_eq {α : Type u_1} [decidable_eq α] {l : list α} (n : l.nodup) :
{val := l, nodup := n} = l.to_finset

@[simp]
theorem list.mem_to_finset {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :

@[simp]
theorem list.to_finset_nil {α : Type u_1} [decidable_eq α] :

@[simp]
theorem list.to_finset_cons {α : Type u_1} [decidable_eq α] {a : α} {l : list α} :

map

def finset.map {α : Type u_1} {β : Type u_2} :
β)finset αfinset β

When f is an embedding of α in β and s is a finset in α, then s.map f is the image finset in β. The embedding condition guarantees that there are no duplicates in the image.

Equations
@[simp]
theorem finset.map_val {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :

@[simp]
theorem finset.map_empty {α : Type u_1} {β : Type u_2} (f : α β) :

@[simp]
theorem finset.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {b : β} :
b finset.map f s ∃ (a : α) (H : a s), f a = b

theorem finset.mem_map' {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
f a finset.map f s a s

theorem finset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : finset α} :
a sf a finset.map f s

@[simp]
theorem finset.coe_map {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :

theorem finset.coe_map_subset_range {α : Type u_1} {β : Type u_2} (f : α β) (s : finset α) :

theorem finset.map_to_finset {α : Type u_1} {β : Type u_2} {f : α β} [decidable_eq α] [decidable_eq β] {s : multiset α} :

@[simp]
theorem finset.map_refl {α : Type u_1} {s : finset α} :

theorem finset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {s : finset α} {g : β γ} :

theorem finset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α β} {s₁ s₂ : finset α} :
finset.map f s₁ finset.map f s₂ s₁ s₂

theorem finset.map_inj {α : Type u_1} {β : Type u_2} {f : α β} {s₁ s₂ : finset α} :
finset.map f s₁ = finset.map f s₂ s₁ = s₂

def finset.map_embedding {α : Type u_1} {β : Type u_2} :
β)finset α finset β

Associate to an embedding f from α to β the embedding that maps a finset to its image under f.

Equations
@[simp]
theorem finset.map_embedding_apply {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :

theorem finset.map_filter {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} {p : β → Prop} [decidable_pred p] :

theorem finset.map_union {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α β} (s₁ s₂ : finset α) :
finset.map f (s₁ s₂) = finset.map f s₁ finset.map f s₂

theorem finset.map_inter {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α β} (s₁ s₂ : finset α) :
finset.map f (s₁ s₂) = finset.map f s₁ finset.map f s₂

@[simp]
theorem finset.map_singleton {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
finset.map f {a} = {f a}

@[simp]
theorem finset.map_insert {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (a : α) (s : finset α) :
finset.map f (insert a s) = insert (f a) (finset.map f s)

@[simp]
theorem finset.map_eq_empty {α : Type u_1} {β : Type u_2} {f : α β} {s : finset α} :

theorem finset.attach_map_val {α : Type u_1} {s : finset α} :

theorem finset.nonempty.map {α : Type u_1} {β : Type u_2} {s : finset α} (h : s.nonempty) (f : α β) :

theorem finset.range_add_one' (n : ) :
finset.range (n + 1) = insert 0 (finset.map {to_fun := λ (i : ), i + 1, inj' := _} (finset.range n))

image

def finset.image {α : Type u_1} {β : Type u_2} [decidable_eq β] :
(α → β)finset αfinset β

image f s is the forward image of s under f.

Equations
@[simp]
theorem finset.image_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : finset α) :

@[simp]
theorem finset.image_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :

@[simp]
theorem finset.mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {b : β} :
b finset.image f s ∃ (a : α) (H : a s), f a = b

theorem finset.mem_image_of_mem {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) {a : α} {s : finset α} :
a sf a finset.image f s

theorem finset.filter_mem_image_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : finset α) (t : finset β) :
(∀ (x : α), x sf x t)finset.filter (λ (y : β), y finset.image f s) t = finset.image f s

theorem finset.fiber_nonempty_iff_mem_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (s : finset α) (y : β) :
(finset.filter (λ (x : α), f x = y) s).nonempty y finset.image f s

@[simp]
theorem finset.coe_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → β} :

theorem finset.nonempty.image {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (f : α → β) :

theorem finset.image_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} [decidable_eq α] {s : multiset α} :

theorem finset.image_val_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :
(∀ (x : α), x s∀ (y : α), y sf x = f yx = y)(finset.image f s).val = multiset.map f s.val

@[simp]
theorem finset.image_id {α : Type u_1} {s : finset α} [decidable_eq α] :

theorem finset.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] {f : α → β} {s : finset α} [decidable_eq γ] {g : β → γ} :

theorem finset.image_subset_image {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s₁ s₂ : finset α} :
s₁ s₂finset.image f s₁ finset.image f s₂

theorem finset.image_subset_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : finset β} {f : α → β} :
finset.image f s t ∀ (x : α), x sf x t

theorem finset.image_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) :

theorem finset.coe_image_subset_range {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

theorem finset.image_filter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} {p : β → Prop} [decidable_pred p] :

theorem finset.image_union {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {f : α → β} (s₁ s₂ : finset α) :
finset.image f (s₁ s₂) = finset.image f s₁ finset.image f s₂

theorem finset.image_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} [decidable_eq α] (s₁ s₂ : finset α) :
(∀ (x y : α), f x = f yx = y)finset.image f (s₁ s₂) = finset.image f s₁ finset.image f s₂

@[simp]
theorem finset.image_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α → β) (a : α) :
finset.image f {a} = {f a}

@[simp]
theorem finset.image_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (f : α → β) (a : α) (s : finset α) :

@[simp]
theorem finset.image_eq_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

theorem finset.attach_image_val {α : Type u_1} [decidable_eq α] {s : finset α} :

@[simp]
theorem finset.attach_insert {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
(insert a s).attach = insert a, _⟩ (finset.image (λ (x : {x // x s}), x.val, _⟩) s.attach)

theorem finset.map_eq_image {α : Type u_1} {β : Type u_2} [decidable_eq β] (f : α β) (s : finset α) :

theorem finset.image_const {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} (h : s.nonempty) (b : β) :
finset.image (λ (a : α), b) s = {b}

@[instance]
def finset.functor [Π (P : Prop), decidable P] :

Because finset.image requires a decidable_eq instances for the target type, we can only construct a functor finset when working classically.

Equations
@[instance]

def finset.subtype {α : Type u_1} (p : α → Prop) [decidable_pred p] :
finset αfinset (subtype p)

Given a finset s and a predicate p, s.subtype p is the finset of subtype p whose elements belong to s.

Equations
@[simp]
theorem finset.mem_subtype {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} {a : subtype p} :

theorem finset.subtype_eq_empty {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : finset α} :
finset.subtype p s = ∀ (x : α), p xx s

@[simp]
theorem finset.subtype_map {α : Type u_1} {s : finset α} (p : α → Prop) [decidable_pred p] :

s.subtype p converts back to s.filter p with embedding.subtype.

theorem finset.subtype_map_of_mem {α : Type u_1} {s : finset α} {p : α → Prop} [decidable_pred p] :
(∀ (x : α), x sp x)finset.map (function.embedding.subtype p) (finset.subtype p s) = s

If all elements of a finset satisfy the predicate p, s.subtype p converts back to s with embedding.subtype.

theorem finset.property_of_mem_map_subtype {α : Type u_1} {p : α → Prop} (s : finset {x // p x}) {a : α} :
a finset.map (function.embedding.subtype (λ (x : α), p x)) sp a

If a finset of a subtype is converted to the main type with embedding.subtype, all elements of the result have the property of the subtype.

theorem finset.not_mem_map_subtype_of_not_property {α : Type u_1} {p : α → Prop} (s : finset {x // p x}) {a : α} :
¬p aa finset.map (function.embedding.subtype (λ (x : α), p x)) s

If a finset of a subtype is converted to the main type with embedding.subtype, the result does not contain any value that does not satisfy the property of the subtype.

theorem finset.map_subtype_subset {α : Type u_1} {t : set α} (s : finset t) :
(finset.map (function.embedding.subtype (λ (x : α), x t)) s) t

If a finset of a subtype is converted to the main type with embedding.subtype, the result is a subset of the set giving the subtype.

theorem finset.subset_image_iff {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset β} {t : set α} :
s f '' t ∃ (s' : finset α), s' t finset.image f s' = s

theorem multiset.to_finset_map {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (m : multiset α) :

card

def finset.card {α : Type u_1} :
finset α

card s is the cardinality (number of elements) of s.

Equations
theorem finset.card_def {α : Type u_1} (s : finset α) :

@[simp]
theorem finset.card_mk {α : Type u_1} {m : multiset α} {nodup : m.nodup} :
{val := m, nodup := nodup}.card = m.card

@[simp]
theorem finset.card_empty {α : Type u_1} :

@[simp]
theorem finset.card_eq_zero {α : Type u_1} {s : finset α} :
s.card = 0 s =

theorem finset.card_pos {α : Type u_1} {s : finset α} :

theorem finset.card_ne_zero_of_mem {α : Type u_1} {s : finset α} {a : α} :
a ss.card 0

theorem finset.card_eq_one {α : Type u_1} {s : finset α} :
s.card = 1 ∃ (a : α), s = {a}

@[simp]
theorem finset.card_insert_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(insert a s).card = s.card + 1

theorem finset.card_insert_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(insert a s).card = s.card

theorem finset.card_insert_le {α : Type u_1} [decidable_eq α] (a : α) (s : finset α) :
(insert a s).card s.card + 1

@[simp]
theorem finset.card_singleton {α : Type u_1} (a : α) :
{a}.card = 1

theorem finset.card_singleton_inter {α : Type u_1} [decidable_eq α] {x : α} {s : finset α} :
({x} s).card 1

theorem finset.card_erase_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(s.erase a).card = s.card.pred

theorem finset.card_erase_lt_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
a s(s.erase a).card < s.card

theorem finset.card_erase_le {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
(s.erase a).card s.card

theorem finset.pred_card_le_card_erase {α : Type u_1} [decidable_eq α] {a : α} {s : finset α} :
s.card - 1 (s.erase a).card

@[simp]
theorem finset.card_range (n : ) :

@[simp]
theorem finset.card_attach {α : Type u_1} {s : finset α} :

theorem multiset.to_finset_card_le {α : Type u_1} [decidable_eq α] (m : multiset α) :

theorem list.to_finset_card_le {α : Type u_1} [decidable_eq α] (l : list α) :

theorem finset.card_image_le {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :

theorem finset.card_image_of_inj_on {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} {s : finset α} :
(∀ (x : α), x s∀ (y : α), y sf x = f yx = y)(finset.image f s).card = s.card

theorem finset.card_image_of_injective {α : Type u_1} {β : Type u_2} [decidable_eq β] {f : α → β} (s : finset α) :

theorem finset.fiber_card_ne_zero_iff_mem_image {α : Type u_1} {β : Type u_2} (s : finset α) (f : α → β) [decidable_eq β] (y : β) :
(finset.filter (λ (x : α), f x = y) s).card 0 y finset.image f s

@[simp]
theorem finset.card_map {α : Type u_1} {β : Type u_2} (f : α β) {s : finset α} :

theorem finset.card_eq_of_bijective {α : Type u_1} {s : finset α} {n : } (f : Π (i : ), i < n → α) :
(∀ (a : α), a s(∃ (i : ) (h : i < n), f i h = a))(∀ (i : ) (h : i < n), f i h s)(∀ (i j : ) (hi : i < n) (hj : j < n), f i hi = f j hji = j)s.card = n

theorem finset.card_eq_succ {α : Type u_1} [decidable_eq α] {s : finset α} {n : } :
s.card = n + 1 ∃ (a : α) (t : finset α), a t insert a t = s t.card = n

theorem finset.card_le_of_subset {α : Type u_1} {s t : finset α} :
s ts.card t.card

theorem finset.eq_of_subset_of_card_le {α : Type u_1} {s t : finset α} :
s tt.card s.cards = t

theorem finset.card_lt_card {α : Type u_1} {s t : finset α} :
s ts.card < t.card

theorem finset.card_le_card_of_inj_on {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : α → β) :
(∀ (a : α), a sf a t)(∀ (a₁ : α), a₁ s∀ (a₂ : α), a₂ sf a₁ = f a₂a₁ = a₂)s.card t.card

theorem finset.exists_ne_map_eq_of_card_lt_of_maps_to {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (hc : t.card < s.card) {f : α → β} :
(∀ (a : α), a sf a t)(∃ (x : α) (H : x s) (y : α) (H : y s), x y f x = f y)

If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.

theorem finset.card_le_of_inj_on {α : Type u_1} {n : } {s : finset α} (f : → α) :
(∀ (i : ), i < nf i s)(∀ (i j : ), i < nj < nf i = f ji = j)n s.card

def finset.strong_induction_on {α : Type u_1} {p : finset αSort u_2} (s : finset α) :
(Π (s : finset α), (Π (t : finset α), t sp t)p s)p s

Suppose that, given objects defined on all strict subsets of any finset s, one knows how to define an object on s. Then one can inductively define an object on all finsets, starting from the empty set and iterating. This can be used either to define data, or to prove properties.

Equations
theorem finset.case_strong_induction_on {α : Type u_1} [decidable_eq α] {p : finset α → Prop} (s : finset α) :
p (∀ (a : α) (s : finset α), a s(∀ (t : finset α), t sp t)p (insert a s))p s

theorem finset.card_congr {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a s → β) :
(∀ (a : α) (ha : a s), f a ha t)(∀ (a b : α) (ha : a s) (hb : b s), f a ha = f b hba = b)(∀ (b : β), b t(∃ (a : α) (ha : a s), f a ha = b))s.card = t.card

theorem finset.card_union_add_card_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card + (s t).card = s.card + t.card

theorem finset.card_union_le {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s t).card s.card + t.card

theorem finset.card_union_eq {α : Type u_1} [decidable_eq α] {s t : finset α} :
disjoint s t(s t).card = s.card + t.card

theorem finset.surj_on_of_inj_on_of_card_le {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a s → β) (hf : ∀ (a : α) (ha : a s), f a ha t) (hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), f a₁ ha₁ = f a₂ ha₂a₁ = a₂) (hst : t.card s.card) (b : β) :
b t(∃ (a : α) (ha : a s), b = f a ha)

theorem finset.inj_on_of_surj_on_of_card_le {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (f : Π (a : α), a s → β) (hf : ∀ (a : α) (ha : a s), f a ha t) (hsurj : ∀ (b : β), b t(∃ (a : α) (ha : a s), b = f a ha)) (hst : s.card t.card) ⦃a₁ a₂ : α⦄ (ha₁ : a₁ s) (ha₂ : a₂ s) :
f a₁ ha₁ = f a₂ ha₂a₁ = a₂

bind

def finset.bind {α : Type u_1} {β : Type u_2} [decidable_eq β] :
finset α(α → finset β)finset β

bind s t is the union of t x over x ∈ s

Equations
@[simp]
theorem finset.bind_val {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (t : α → finset β) :
(s.bind t).val = (s.val.bind (λ (a : α), (t a).val)).erase_dup

@[simp]
theorem finset.bind_empty {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} :

@[simp]
theorem finset.mem_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} {b : β} :
b s.bind t ∃ (a : α) (H : a s), b t a

@[simp]
theorem finset.bind_insert {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t : α → finset β} [decidable_eq α] {a : α} :
(insert a s).bind t = t a s.bind t

@[simp]
theorem finset.singleton_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] {t : α → finset β} {a : α} :
{a}.bind t = t a

theorem finset.bind_inter {α : Type u_1} {β : Type u_2} [decidable_eq β] (s : finset α) (f : α → finset β) (t : finset β) :
s.bind f t = s.bind (λ (x : α), f x t)

theorem finset.inter_bind {α : Type u_1} {β : Type u_2} [decidable_eq β] (t : finset β) (s : finset α) (f : α → finset β) :
t s.bind f = s.bind (λ (x : α), t f x)

theorem finset.image_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {f : α → β} {s : finset α} {t : β → finset γ} :
(finset.image f s).bind t = s.bind (λ (a : α), t (f a))

theorem finset.bind_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [decidable_eq γ] {s : finset α} {t : α → finset β} {f : β → γ} :
finset.image f (s.bind t) = s.bind (λ (a : α), finset.image f (t a))

theorem finset.bind_to_finset {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : multiset α) (t : α → multiset β) :
(s.bind t).to_finset = s.to_finset.bind (λ (a : α), (t a).to_finset)

theorem finset.bind_mono {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {t₁ t₂ : α → finset β} :
(∀ (a : α), a st₁ a t₂ a)s.bind t₁ s.bind t₂

theorem finset.bind_subset_bind_of_subset_left {β : Type u_2} [decidable_eq β] {α : Type u_1} {s₁ s₂ : finset α} (t : α → finset β) :
s₁ s₂s₁.bind t s₂.bind t

theorem finset.bind_singleton {α : Type u_1} {β : Type u_2} [decidable_eq β] {s : finset α} {f : α → β} :
s.bind (λ (a : α), {f a}) = finset.image f s

@[simp]
theorem finset.bind_singleton_eq_self {α : Type u_1} {s : finset α} [decidable_eq α] :

theorem finset.bind_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] {s : finset α} {t : finset β} {f : α → β} :
(∀ (x : α), x sf x t)t.bind (λ (a : β), finset.filter (λ (c : α), f c = a) s) = s

theorem finset.image_bind_filter_eq {α : Type u_1} {β : Type u_2} [decidable_eq β] [decidable_eq α] (s : finset β) (g : β → α) :
(finset.image g s).bind (λ (a : α), finset.filter (λ (c : β), g c = a) s) = s

prod

def finset.product {α : Type u_1} {β : Type u_2} :
finset αfinset βfinset × β)

product s t is the set of pairs (a, b) such that a ∈ s and b ∈ t.

Equations
@[simp]
theorem finset.product_val {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :

@[simp]
theorem finset.mem_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {p : α × β} :
p s.product t p.fst s p.snd t

theorem finset.subset_product {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {s : finset × β)} :

theorem finset.product_eq_bind {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
s.product t = s.bind (λ (a : α), finset.image (λ (b : β), (a, b)) t)

@[simp]
theorem finset.card_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
(s.product t).card = (s.card) * t.card

theorem finset.filter_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] :
finset.filter (λ (x : α × β), p x.fst q x.snd) (s.product t) = (finset.filter p s).product (finset.filter q t)

theorem finset.filter_product_card {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] :
(finset.filter (λ (x : α × β), p x.fst q x.snd) (s.product t)).card = ((finset.filter p s).card) * (finset.filter q t).card + ((finset.filter (not p) s).card) * (finset.filter (not q) t).card

sigma

def finset.sigma {α : Type u_1} {σ : α → Type u_4} :
finset α(Π (a : α), finset (σ a))finset (Σ (a : α), σ a)

sigma s t is the set of dependent pairs ⟨a, b⟩ such that a ∈ s and b ∈ t a.

Equations
@[simp]
theorem finset.mem_sigma {α : Type u_1} {σ : α → Type u_4} {s : finset α} {t : Π (a : α), finset (σ a)} {p : sigma σ} :
p s.sigma t p.fst s p.