Attaching a proof of membership to a finite set

Main declarations

• Finset.attach: Given s : Finset α, attach s forms a finset of elements of the subtype {a // a ∈ s}; in other words, it attaches elements to a proof of membership in the set.

Tags

finite sets, finset

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

• s.attach = { val := s.val.attach, nodup := ⋯ }

@[simp]

theorem Finset.attach_val {α : Type u_1} (s : Finset α) : s.attach.val = s.val.attach

@[simp]

theorem Finset.mem_attach {α : Type u_1} (s : Finset α) (x : { x : α // x ∈ s }) : x ∈ s.attach

@[simp]

theorem Finset.coe_attach {α : Type u_1} (s : Finset α) : ↑s.attach = Set.univ