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 = Finset.Iio n

@[simp]

theorem Fin.Ioi_zero_eq_map {n : ℕ} : Finset.Ioi 0 = Finset.map (Fin.succEmbedding n).toEmbedding Finset.univ

@[simp]

theorem Fin.Iio_last_eq_map {n : ℕ} : Finset.Iio (Fin.last n) = Finset.map Fin.castSuccEmb.toEmbedding Finset.univ

@[simp]

theorem Fin.Ioi_succ {n : ℕ} (i : Fin n) : Finset.Ioi (Fin.succ i) = Finset.map (Fin.succEmbedding n).toEmbedding (Finset.Ioi i)

@[simp]

theorem Fin.Iio_castSucc {n : ℕ} (i : Fin n) : Finset.Iio (Fin.castSucc i) = Finset.map Fin.castSuccEmb.toEmbedding (Finset.Iio i)

theorem Fin.card_filter_univ_succ' {n : ℕ} (p : Fin (n + 1) → Prop) [DecidablePred p] : 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) [DecidablePred p] : 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 : ℕ} [DecidableEq α] (a : α) (v : Vector α n) : Finset.card (Finset.filter (fun i => a = Vector.get v i) Finset.univ) = List.count a (Vector.toList v)