Finsets in Fin n

A few constructions for Finsets in Fin n.

Main declarations

• Finset.attachFin: Turns a Finset of naturals strictly less than n into a Finset (Fin n).

def Finset.attachFin (s : Finset ℕ) {n : ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) : Finset (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

• Finset.attachFin s h = { val := Multiset.pmap (fun a ha => { val := a, isLt := ha }) s.val h, nodup := (_ : Multiset.Nodup (Multiset.pmap (fun a ha => { val := a, isLt := ha }) s.val h)) }

@[simp]

theorem Finset.mem_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) {a : Fin n} : a ∈ Finset.attachFin s h ↔ ↑a ∈ s

@[simp]

theorem Finset.card_attachFin {n : ℕ} (s : Finset ℕ) (h : ∀ (m : ℕ), m ∈ s → m < n) : Finset.card (Finset.attachFin s h) = Finset.card s