Finsets in `fin n` #

A few constructions for finsets in fin n.

Main declarations #

finset.fin_range: {0, 1, ..., n - 1} as a finset (fin n).
finset.attach_fin: Turns a finset of naturals strictly less than n into a finset (fin n).

source

def finset.fin_range (n : ℕ) :

finset (fin n)

finset.fin_range n is the finset {0, 1, ..., n - 1}, as a finset (fin n).

Equations

finset.fin_range n = {val := ↑(list.fin_range n), nodup := _}

source

@[simp]

theorem finset.fin_range_card {n : ℕ} :

(finset.fin_range n).card = n

source

@[simp]

theorem finset.mem_fin_range {n : ℕ} (m : fin n) :

m ∈ finset.fin_range n

source

@[simp]

theorem finset.coe_fin_range (n : ℕ) :

↑(finset.fin_range n) = set.univ

source

def finset.attach_fin (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.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` #