Documentation

Std.Data.Fin.Lemmas

clamp #

@[simp]
theorem Fin.coe_clamp (n : Nat) (m : Nat) :
(Fin.clamp n m) = min n m

enum/list #

@[simp]
theorem Fin.size_enum (n : Nat) :
@[simp]
theorem Fin.getElem_enum {n : Nat} (i : Nat) (h : i < Array.size (Fin.enum n)) :
(Fin.enum n)[i] = { val := i, isLt := }
@[simp]
@[simp]
theorem Fin.get_list {n : Nat} (i : Fin (List.length (Fin.list n))) :
@[simp]
theorem Fin.list_zero :
Fin.list 0 = []
theorem Fin.list_succ (n : Nat) :
Fin.list (n + 1) = 0 :: List.map Fin.succ (Fin.list n)

foldl #

theorem Fin.foldl_loop_lt {α : Sort u_1} {n : Nat} {m : Nat} (f : αFin nα) (x : α) (h : m < n) :
Fin.foldl.loop n f x m = Fin.foldl.loop n f (f x { val := m, isLt := h }) (m + 1)
theorem Fin.foldl_loop_eq {α : Sort u_1} {n : Nat} (f : αFin nα) (x : α) :
Fin.foldl.loop n f x n = x
theorem Fin.foldl_loop {α : Sort u_1} {n : Nat} {m : Nat} (f : αFin (n + 1)α) (x : α) (h : m < n + 1) :
Fin.foldl.loop (n + 1) f x m = Fin.foldl.loop n (fun (x : α) (i : Fin n) => f x (Fin.succ i)) (f x { val := m, isLt := h }) m
theorem Fin.foldl_zero {α : Sort u_1} (f : αFin 0α) (x : α) :
Fin.foldl 0 f x = x
theorem Fin.foldl_succ {α : Sort u_1} {n : Nat} (f : αFin (n + 1)α) (x : α) :
Fin.foldl (n + 1) f x = Fin.foldl n (fun (x : α) (i : Fin n) => f x (Fin.succ i)) (f x 0)
theorem Fin.foldl_eq_foldl_list {α : Type u_1} {n : Nat} (f : αFin nα) (x : α) :

foldr #

theorem Fin.foldr_loop_zero {n : Nat} {α : Sort u_1} (f : Fin nαα) (x : α) :
Fin.foldr.loop n f { val := 0, property := } x = x
theorem Fin.foldr_loop_succ {n : Nat} {α : Sort u_1} {m : Nat} (f : Fin nαα) (x : α) (h : m < n) :
Fin.foldr.loop n f { val := m + 1, property := h } x = Fin.foldr.loop n f { val := m, property := } (f { val := m, isLt := h } x)
theorem Fin.foldr_loop {n : Nat} {α : Sort u_1} {m : Nat} (f : Fin (n + 1)αα) (x : α) (h : m + 1 n + 1) :
Fin.foldr.loop (n + 1) f { val := m + 1, property := h } x = f 0 (Fin.foldr.loop n (fun (i : Fin n) => f (Fin.succ i)) { val := m, property := } x)
theorem Fin.foldr_succ {n : Nat} {α : Sort u_1} (f : Fin (n + 1)αα) (x : α) :
Fin.foldr (n + 1) f x = f 0 (Fin.foldr n (fun (i : Fin n) => f (Fin.succ i)) x)
theorem Fin.foldr_eq_foldr_list {n : Nat} {α : Type u_1} (f : Fin nαα) (x : α) :