Documentation

Batteries.Data.Fin.Lemmas

foldl/foldr #

theorem Fin.foldl_assoc {α : Sort u_1} {n : Nat} {op : ααα} [ha : Std.Associative op] {f : Fin nα} {a₁ a₂ : α} :
foldl n (fun (x : α) (i : Fin n) => op x (f i)) (op a₁ a₂) = op a₁ (foldl n (fun (x : α) (i : Fin n) => op x (f i)) a₂)
theorem Fin.foldr_assoc {α : Sort u_1} {n : Nat} {op : ααα} [ha : Std.Associative op] {f : Fin nα} {a₁ a₂ : α} :
foldr n (fun (i : Fin n) (x : α) => op (f i) x) (op a₁ a₂) = op (foldr n (fun (i : Fin n) (x : α) => op (f i) x) a₁) a₂

clamp #

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

findSome? #

@[simp]
theorem Fin.findSome?_zero {α : Type u_1} {f : Fin 0Option α} :
@[simp]
theorem Fin.findSome?_one {α : Type u_1} {f : Fin 1Option α} :
findSome? f = f 0
theorem Fin.findSome?_succ {n : Nat} {α : Type u_1} {f : Fin (n + 1)Option α} :
findSome? f = (f 0).or (findSome? fun (i : Fin n) => f i.succ)
theorem Fin.findSome?_succ_of_some {n : Nat} {α : Type u_1} {x : α} {f : Fin (n + 1)Option α} (h : f 0 = some x) :
theorem Fin.findSome?_succ_of_isSome {n : Nat} {α : Type u_1} {f : Fin (n + 1)Option α} (h : (f 0).isSome = true) :
findSome? f = f 0
theorem Fin.findSome?_succ_of_none {n : Nat} {α : Type u_1} {f : Fin (n + 1)Option α} (h : f 0 = none) :
findSome? f = findSome? fun (i : Fin n) => f i.succ
theorem Fin.findSome?_succ_of_isNone {n : Nat} {α : Type u_1} {f : Fin (n + 1)Option α} (h : (f 0).isNone = true) :
findSome? f = findSome? fun (i : Fin n) => f i.succ
@[simp]
theorem Fin.findSome?_eq_some_iff {n : Nat} {α : Type u_1} {a : α} {f : Fin nOption α} :
findSome? f = some a (i : Fin n), f i = some a ∀ (j : Fin n), j < if j = none
@[simp]
theorem Fin.findSome?_eq_none_iff {n : Nat} {α : Type u_1} {f : Fin nOption α} :
findSome? f = none ∀ (i : Fin n), f i = none
theorem Fin.isNone_findSome?_iff {n : Nat} {α : Type u_1} {f : Fin nOption α} :
(findSome? f).isNone = true ∀ (i : Fin n), (f i).isNone = true
@[deprecated Fin.isNone_findSome?_iff (since := "2025-09-28")]
theorem Fin.findSome?_isNone_iff {n : Nat} {α : Type u_1} {f : Fin nOption α} :
(findSome? f).isNone = true ∀ (i : Fin n), (f i).isNone = true

Alias of Fin.isNone_findSome?_iff.

@[simp]
theorem Fin.isSome_findSome?_iff {n : Nat} {α : Type u_1} {f : Fin nOption α} :
@[deprecated Fin.isSome_findSome?_iff (since := "2025-09-28")]
theorem Fin.findSome?_isSome_iff {n : Nat} {α : Type u_1} {f : Fin nOption α} :

Alias of Fin.isSome_findSome?_iff.

theorem Fin.exists_minimal_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin nOption α} (h : findSome? f = some x) :
(i : Fin n), f i = some x ∀ (j : Fin n), j < if j = none
theorem Fin.exists_eq_some_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin nOption α} (h : findSome? f = some x) :
(i : Fin n), f i = some x
@[deprecated Fin.exists_eq_some_of_findSome?_eq_some (since := "2025-09-28")]
theorem Fin.exists_of_findSome?_eq_some {n : Nat} {α : Type u_1} {x : α} {f : Fin nOption α} (h : findSome? f = some x) :
(i : Fin n), f i = some x

Alias of Fin.exists_eq_some_of_findSome?_eq_some.

theorem Fin.eq_none_of_findSome?_eq_none {n : Nat} {α : Type u_1} {f : Fin nOption α} (h : findSome? f = none) (i : Fin n) :
f i = none
theorem Fin.exists_isSome_of_isSome_findSome? {n : Nat} {α : Type u_1} {f : Fin nOption α} (h : (findSome? f).isSome = true) :
(i : Fin n), (f i).isSome = true
theorem Fin.isNone_of_isNone_findSome? {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin nOption α} (h : (findSome? f).isNone = true) :
(f i).isNone = true
theorem Fin.isSome_findSome?_of_isSome {n : Nat} {α : Type u_1} {i : Fin n} {f : Fin nOption α} (h : (f i).isSome = true) :
theorem Fin.map_findSome? {n : Nat} {α : Type u_1} {β : Type u_2} (f : Fin nOption α) (g : αβ) :
Option.map g (findSome? f) = findSome? fun (x : Fin n) => Option.map g (f x)

Fin.find? #

@[simp]
theorem Fin.find?_zero {p : Fin 0Bool} :
@[simp]
theorem Fin.find?_one {p : Fin 1Bool} :
theorem Fin.find?_succ {n : Nat} {p : Fin (n + 1)Bool} :
find? p = if p 0 = true then some 0 else Option.map succ (find? fun (i : Fin n) => p i.succ)
@[simp]
theorem Fin.find?_eq_some_iff {n : Nat} {i : Fin n} {p : Fin nBool} :
find? p = some i p i = true ∀ (j : Fin n), j < ip j = false
theorem Fin.isSome_find?_iff {n : Nat} {p : Fin nBool} :
@[deprecated Fin.isSome_find?_iff (since := "2025-09-28")]
theorem Fin.find?_isSome_iff {n : Nat} {p : Fin nBool} :

Alias of Fin.isSome_find?_iff.

@[simp]
theorem Fin.find?_eq_none_iff {n : Nat} {p : Fin nBool} :
find? p = none ∀ (i : Fin n), p i = false
theorem Fin.isNone_find?_iff {n : Nat} {p : Fin nBool} :
(find? p).isNone = true ∀ (i : Fin n), p i = false
@[deprecated Fin.isNone_find?_iff (since := "2025-09-28")]
theorem Fin.find?_isNone_iff {n : Nat} {p : Fin nBool} :
(find? p).isNone = true ∀ (i : Fin n), p i = false

Alias of Fin.isNone_find?_iff.

theorem Fin.eq_true_of_find?_eq_some {n : Nat} {i : Fin n} {p : Fin nBool} (h : find? p = some i) :
p i = true
theorem Fin.eq_false_of_find?_eq_some_of_lt {n : Nat} {i : Fin n} {p : Fin nBool} (h : find? p = some i) (j : Fin n) :
j < ip j = false
theorem Fin.eq_false_of_find?_eq_none {n : Nat} {p : Fin nBool} (h : find? p = none) (i : Fin n) :
p i = false
theorem Fin.exists_eq_true_of_isSome_find? {n : Nat} {p : Fin nBool} (h : (find? p).isSome = true) :
(i : Fin n), p i = true
theorem Fin.eq_false_of_isNone_find? {n : Nat} {i : Fin n} {p : Fin nBool} (h : (find? p).isNone = true) :
p i = false
theorem Fin.isSome_find?_of_eq_true {n : Nat} {i : Fin n} {p : Fin nBool} (h : p i = true) :
theorem Fin.get_find?_eq_true {n : Nat} {p : Fin nBool} (h : (find? p).isSome = true) :
p ((find? p).get h) = true
theorem Fin.get_find?_minimal {n : Nat} {p : Fin nBool} (h : (find? p).isSome = true) (j : Fin n) :
j < (find? p).get hp j = false

exists #

theorem Fin.exists_eq_true_iff_exists_minimal_eq_true {n : Nat} (p : Fin nBool) :
( (i : Fin n), p i = true) (i : Fin n), p i = true ∀ (j : Fin n), j < ip j = false
theorem Fin.exists_iff_exists_minimal {n : Nat} (p : Fin nProp) [DecidablePred p] :
( (i : Fin n), p i) (i : Fin n), p i ∀ (j : Fin n), j < i¬p j