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)
.
@[simp]
theorem
Finset.card_attachFin
{n : ℕ}
(s : Finset ℕ)
(h : ∀ (m : ℕ), m ∈ s → m < n)
:
Finset.card (Finset.attachFin s h) = Finset.card s