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]
@[simp]
theorem
fin.card_filter_univ_succ'
{n : ℕ}
(p : fin (n + 1) → Prop)
[decidable_pred p] :
(finset.filter p finset.univ).card = ite (p 0) 1 0 + (finset.filter (p ∘ fin.succ) finset.univ).card
theorem
fin.card_filter_univ_succ
{n : ℕ}
(p : fin (n + 1) → Prop)
[decidable_pred p] :
(finset.filter p finset.univ).card = ite (p 0) ((finset.filter (p ∘ fin.succ) finset.univ).card + 1) (finset.filter (p ∘ fin.succ) finset.univ).card
theorem
fin.card_filter_univ_eq_vector_nth_eq_count
{α : Type u_1}
{n : ℕ}
[decidable_eq α]
(a : α)
(v : vector α n) :
(finset.filter (λ (i : fin n), a = v.nth i) finset.univ).card = list.count a v.to_list