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.Iio_last_eq_map
{n : ℕ}
:
Finset.Iio (Fin.last n) = Finset.map Fin.castSuccEmb Finset.univ
@[simp]
theorem
Fin.Ioi_succ
{n : ℕ}
(i : Fin n)
:
Finset.Ioi i.succ = Finset.map (Fin.succEmb n) (Finset.Ioi i)
@[simp]
theorem
Fin.Iio_castSucc
{n : ℕ}
(i : Fin n)
:
Finset.Iio i.castSucc = Finset.map Fin.castSuccEmb (Finset.Iio i)
theorem
Fin.card_filter_univ_succ
{n : ℕ}
(p : Fin (n + 1) → Prop)
[DecidablePred p]
:
(Finset.filter p Finset.univ).card = if p 0 then (Finset.filter (p ∘ Fin.succ) Finset.univ).card + 1 else (Finset.filter (p ∘ Fin.succ) Finset.univ).card
theorem
Fin.card_filter_univ_succ'
{n : ℕ}
(p : Fin (n + 1) → Prop)
[DecidablePred p]
:
(Finset.filter p Finset.univ).card = (if p 0 then 1 else 0) + (Finset.filter (p ∘ Fin.succ) Finset.univ).card
theorem
Fin.card_filter_univ_eq_vector_get_eq_count
{α : Type u_1}
{n : ℕ}
[DecidableEq α]
(a : α)
(v : Mathlib.Vector α n)
:
(Finset.filter (fun (i : Fin n) => v.get i = a) Finset.univ).card = List.count a v.toList