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]

theorem Fin.map_valEmbedding_univ {n : ℕ} : Finset.map valEmbedding Finset.univ = Finset.Iio n

@[simp]

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

@[simp]

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

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

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

theorem Fin.card_filter_val_lt {n m : ℕ} : {i : Fin n | ↑i < m}.card = min n m

theorem Fin.card_filter_univ_succ {n : ℕ} (p : Fin (n + 1) → Prop) [DecidablePred p] : {x : Fin (n + 1) | p x}.card = if p 0 then {x : Fin n | p x.succ}.card + 1 else {x : Fin n | p x.succ}.card

theorem Fin.card_filter_univ_succ' {n : ℕ} (p : Fin (n + 1) → Prop) [DecidablePred p] : {x : Fin (n + 1) | p x}.card = (if p 0 then 1 else 0) + {x : Fin n | p x.succ}.card

theorem Fin.card_filter_univ_eq_vector_get_eq_count {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (v : List.Vector α n) : {i : Fin n | v.get i = a}.card = List.count a v.toList

theorem Fin.lt_card_filter_univ_iff_apply_of_imp {n : ℕ} {j : Fin n} (p : Fin n → Prop) [DecidablePred p] (hp : ∀ (i j : Fin n), j ≤ i → p i → p j) : ↑j < {i : Fin n | p i}.card ↔ p j

Given a "downward-closed" predicate p on Fin n (which could be spelt Antitone p), then p holds for more than j elements iff it holds for p itself.