mathlib3 documentation

data.fintype.fin

The structure of fintype (fin n) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains some basic results about the fintype instance for fin, especially properties of finset.univ : finset (fin n).

source
theorem fin.map_subtype_embedding_univ {n : ℕ} :
finset.map fin.coe_embedding finset.univ = finset.Iio n
source
@[simp]
theorem fin.Ioi_zero_eq_map {n : ℕ} :
finset.Ioi 0 = finset.map (fin.succ_embedding n).to_embedding finset.univ
source
@[simp]
theorem fin.Iio_last_eq_map {n : ℕ} :
finset.Iio (fin.last n) = finset.map fin.cast_succ.to_embedding finset.univ
source
@[simp]
theorem fin.Ioi_succ {n : ℕ} (i : fin n) :
finset.Ioi i.succ = finset.map (fin.succ_embedding n).to_embedding (finset.Ioi i)
source
@[simp]
theorem fin.Iio_cast_succ {n : ℕ} (i : fin n) :
finset.Iio (⇑fin.cast_succ i) = finset.map fin.cast_succ.to_embedding (finset.Iio i)
source
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
source
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
source
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