mathlib3 documentation

data.finset.fin

Finsets in fin n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A few constructions for finsets in fin n.

Main declarations #

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