Documentation

Mathlib.Data.Finset.Attach

Attaching a proof of membership to a finite set #

Main declarations #

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
Instances For
    @[simp]
    theorem Finset.attach_val {α : Type u_1} (s : Finset α) :
    @[simp]
    theorem Finset.mem_attach {α : Type u_1} (s : Finset α) (x : { x : α // x s }) :