Documentation

Mathlib.Data.Finset.Fin

Finsets in Fin n #

A few constructions for Finsets in Fin n.

Main declarations #

def Finset.attachFin (s : Finset ) {n : } (h : ms, m < n) :

Given a Finset s of contained in {0,..., n-1}, the corresponding Finset in Fin n is s.attachFin h where h is a proof that all elements of s are less than n.

Equations
  • s.attachFin h = { val := Multiset.pmap (fun (a : ) (ha : a < n) => a, ha) s.val h, nodup := }
Instances For
    @[simp]
    theorem Finset.mem_attachFin {n : } {s : Finset } (h : ms, m < n) {a : Fin n} :
    a s.attachFin h a s
    @[simp]
    theorem Finset.card_attachFin {n : } (s : Finset ) (h : ms, m < n) :
    (s.attachFin h).card = s.card