mathlib documentation

data.finset.fin

Finsets in fin n #

A few constructions for finsets in fin n.

Main declarations #

def finset.attach_fin (s : finset ) {n : } (h : ∀ (m : ), m sm < 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
@[simp]
theorem finset.mem_attach_fin {n : } {s : finset } (h : ∀ (m : ), m sm < n) {a : fin n} :
@[simp]
theorem finset.card_attach_fin {n : } (s : finset ) (h : ∀ (m : ), m sm < n) :