Documentation

Batteries.Data.Fin.Lemmas

theorem Fin.le_antisymm_iff {n : Nat} {x : Fin n} {y : Fin n} :
x = y x y y x
theorem Fin.le_antisymm {n : Nat} {x : Fin n} {y : Fin n} (h1 : x y) (h2 : y x) :
x = y

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) :
(Fin.enum n).size = n
@[simp]
theorem Fin.enum_zero :
Fin.enum 0 = #[]
@[simp]
theorem Fin.getElem_enum {n : Nat} (i : Nat) (h : i < (Fin.enum n).size) :
(Fin.enum n)[i] = i,
@[simp]
theorem Fin.length_list (n : Nat) :
(Fin.list n).length = n
@[simp]
theorem Fin.getElem_list {n : Nat} (i : Nat) (h : i < (Fin.list n).length) :
(Fin.list n)[i] = Fin.cast i, h
@[deprecated Fin.getElem_list]
theorem Fin.get_list {n : Nat} (i : Fin (Fin.list n).length) :
(Fin.list n).get i = Fin.cast i
@[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)
theorem Fin.list_succ_last (n : Nat) :
Fin.list (n + 1) = List.map Fin.castSucc (Fin.list n) ++ [Fin.last n]
theorem Fin.list_reverse (n : Nat) :
(Fin.list n).reverse = List.map Fin.rev (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 m, 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
@[irreducible]
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 i.succ) (f x m, h) m
@[simp]
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 i.succ) (f x 0)
theorem Fin.foldl_succ_last {α : Sort u_1} {n : Nat} (f : αFin (n + 1)α) (x : α) :
Fin.foldl (n + 1) f x = f (Fin.foldl n (fun (x : α) (x_1 : Fin n) => f x x_1.castSucc) x) (Fin.last n)
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 0, 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 m + 1, h x = Fin.foldr.loop n f m, (f m, 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 m + 1, h x = f 0 (Fin.foldr.loop n (fun (i : Fin n) => f i.succ) m, x)
@[simp]
theorem Fin.foldr_zero {α : Sort u_1} (f : Fin 0αα) (x : α) :
Fin.foldr 0 f x = 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 i.succ) x)
theorem Fin.foldr_succ_last {n : Nat} {α : Sort u_1} (f : Fin (n + 1)αα) (x : α) :
Fin.foldr (n + 1) f x = Fin.foldr n (fun (x : Fin n) => f x.castSucc) (f (Fin.last n) x)
theorem Fin.foldr_eq_foldr_list {n : Nat} {α : Type u_1} (f : Fin nαα) (x : α) :

foldl/foldr #

theorem Fin.foldl_rev {n : Nat} {α : Sort u_1} (f : Fin nαα) (x : α) :
Fin.foldl n (fun (x : α) (i : Fin n) => f i.rev x) x = Fin.foldr n f x
theorem Fin.foldr_rev {α : Sort u_1} {n : Nat} (f : αFin nα) (x : α) :
Fin.foldr n (fun (i : Fin n) (x : α) => f x i.rev) x = Fin.foldl n f x