# Documentation

Mathlib.Data.Fintype.Fin

# 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).

theorem Fin.map_valEmbedding_univ {n : } :
Finset.map Fin.valEmbedding Finset.univ =
@[simp]
theorem Fin.Ioi_zero_eq_map {n : } :
= Finset.map ().toEmbedding Finset.univ
@[simp]
theorem Fin.Iio_last_eq_map {n : } :
= Finset.map Fin.castSucc.toEmbedding Finset.univ
@[simp]
theorem Fin.Ioi_succ {n : } (i : Fin n) :
= Finset.map ().toEmbedding ()
@[simp]
theorem Fin.Iio_castSucc {n : } (i : Fin n) :
Finset.Iio (Fin.castSucc.toEmbedding i) = Finset.map Fin.castSucc.toEmbedding ()
theorem Fin.card_filter_univ_succ' {n : } (p : Fin (n + 1)Prop) [inst : ] :
Finset.card (Finset.filter p Finset.univ) = (if p 0 then 1 else 0) + Finset.card (Finset.filter (p Fin.succ) Finset.univ)
theorem Fin.card_filter_univ_succ {n : } (p : Fin (n + 1)Prop) [inst : ] :
Finset.card (Finset.filter p Finset.univ) = if p 0 then Finset.card (Finset.filter (p Fin.succ) Finset.univ) + 1 else Finset.card (Finset.filter (p Fin.succ) Finset.univ)
theorem Fin.card_filter_univ_eq_vector_get_eq_count {α : Type u_1} {n : } [inst : ] (a : α) (v : Vector α n) :
Finset.card (Finset.filter (fun i => a = ) Finset.univ) =