Documentation

Mathlib.Data.Finset.Fin

Finsets in Fin n #

A few constructions for Finsets in Fin n.

Main declarations #

def Finset.attachFin (s : Finset ) {n : } (h : ms, m < 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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Finset.mem_attachFin {n : } {s : Finset } (h : ms, m < n) {a : Fin n} :
    @[simp]
    theorem Finset.card_attachFin {n : } (s : Finset ) (h : ms, m < n) :
    (Finset.attachFin s h).card = s.card