Finsets in `fin n` #

A few constructions for finsets in fin n.

Main declarations #

finset.attach_fin: Turns a finset of naturals strictly less than n into a finset (fin n).

def finset.attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) :

Given a finset s of ℕ contained in {0,..., n-1}, the corresponding finset in fin n is s.attach_fin h where h is a proof that all elements of s are less than n.

Equations

s.attach_fin h = {val := multiset.pmap (λ (a : ℕ) (ha : a < n), ⟨a, ha⟩) s.val h, nodup := _}

source

@[simp]

theorem finset.mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) {a : fin n} :

a ∈ s.attach_fin h ↔ ↑a ∈ s

source

@[simp]

theorem finset.card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ (m : ℕ), m ∈ s → m < n) :

(s.attach_fin h).card = s.card

Finsets in fin n #

Main declarations #

Finsets in `fin n` #