The structure of fintype (fin n) #
This file contains some basic results about the fintype instance for fin,
especially properties of finset.univ : finset (fin n).
@[simp]
theorem
fin.univ_filter_zero_lt
{n : ℕ} :
finset.filter (λ (i : fin n.succ), 0 < i) finset.univ = finset.map (fin.succ_embedding n).to_embedding finset.univ
@[simp]
theorem
fin.univ_filter_succ_lt
{n : ℕ}
(j : fin n) :
finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ = finset.map (fin.succ_embedding n).to_embedding (finset.filter (λ (i : fin n), j < i) finset.univ)