Finsets in Fin n
#
A few constructions for Finsets in Fin n
.
Main declarations #
Finset.attachFin
: Turns a Finset of naturals strictly less thann
into aFinset (Fin 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 := ⋯ }