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

source
@[simp]
theorem Fin.map_valEmbedding_univ {n : ℕ} :
Finset.map valEmbedding Finset.univ = Finset.Iio n
source
@[simp]
theorem Fin.Ioi_zero_eq_map {n : ℕ} :
Finset.Ioi 0 = Finset.map (succEmb n) Finset.univ
source
@[simp]
theorem Fin.Iio_last_eq_map {n : ℕ} :
Finset.Iio (last n) = Finset.map castSuccEmb Finset.univ
source
theorem Fin.Ioi_succ {n : ℕ} (i : Fin n) :
Finset.Ioi i.succ = Finset.map (succEmb n) (Finset.Ioi i)
source
theorem Fin.Iio_castSucc {n : ℕ} (i : Fin n) :
Finset.Iio i.castSucc = Finset.map castSuccEmb (Finset.Iio i)
source
theorem Fin.card_filter_val_lt {n m : ℕ} :
{i : Fin n | ↑i < m}.card = min n m
source
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
source
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
source
theorem List.Vector.countP_toList {α : Type u_1} {n : ℕ} (p : α → Bool) (v : Vector α n) :
countP p v.toList = {i : Fin n | p (v.get i) = true}.card
source
theorem List.Vector.count_toList {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (v : Vector α n) :
count a v.toList = {i : Fin n | v.get i = a}.card
source
@[deprecated List.Vector.count_toList (since := "2026-10-19")]
theorem Fin.card_filter_univ_eq_vector_get_eq_count {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (v : List.Vector α n) :
List.count a v.toList = {i : Fin n | v.get i = a}.card

Alias of List.Vector.count_toList.

source
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.

source
theorem Finset.image_fin_univ {n : ℕ} :
image Fin.val univ = range n
source
@[simp]
theorem Finset.sup_fin_univ {α : Type u_1} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : ℕ → α) :
(univ.sup fun (n_1 : Fin n) => f ↑n_1) = (range n).sup f
source
@[simp]
theorem List.countP_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (p : α → Bool) :
countP p (ofFn f) = {i : Fin n | p (f i) = true}.card
source
@[simp]
theorem List.count_ofFn {α : Type u_1} {n : ℕ} [DecidableEq α] (f : Fin n → α) (a : α) :
count a (ofFn f) = {i : Fin n | f i = a}.card