def List.maxD {α : Type u_1} [Max α] (d : α) (l : List α) : α

Equations

• List.maxD d l = match l.max? with | some m => m | none => d

theorem List.maxD_of_empty_eq {α : Type} [Max α] {d : α} : maxD d [] = d

theorem List.all_le_maxD {l : List Nat} (d a : Nat) : a ∈ l → a ≤ maxD d l

theorem List.maxD_of_append_lt {m a : Nat} {l : List Nat} (h : maxD 0 l < m) (ha : a < m) : maxD 0 (l ++ [a]) < m

theorem List.maxD_le_of_all_le {m : Nat} {l : List Nat} (h : ∀ (a : Nat), a ∈ l → a ≤ m) : maxD 0 l ≤ m

theorem List.maxD_all_lt_of_lt {l : List Nat} {d m : Nat} (h : maxD d l < m) (a : Nat) : a ∈ l → a < m

theorem List.maxD_of_map_all_lt {α : Type u_1} {l : List α} {d m : Nat} (f : α → Nat) (h : maxD d (map f l) < m) (hmem : ∀ (a : α), a ∈ l → f a ∈ map f l) (a : α) : a ∈ l → f a < m

theorem List.maxD_of_all_map_le {m : Nat} {α : Type} {l : List α} {f : α → Nat} (h : ∀ (a : α), a ∈ l → f a ≤ m) : maxD 0 (map f l) ≤ m

theorem List.singleton_val_of {α : Type u_1} (a : α) (arr : List α) (h1 : arr = [a]) (h2 : 0 < arr.length) : arr.get ⟨0, h2⟩ = a

theorem List.singleton_val {α : Type u_1} (a : α) (h : 0 < [a].length) : [a].get ⟨0, h⟩ = a

theorem List.get_of_fun_eq {α : Type u_1} {l1 l2 : List α} {f : List α → List α} (h : f l1 = f l2) (n : Fin (f l1).length) : (f l1).get n = (f l2).get ⟨↑n, ⋯⟩

theorem List.eq_of_dropLast_eq_last_eq {α : Type u_1} {l1 l2 : List α} (hd : l1.dropLast = l2.dropLast) (hl1 : l1.length - 1 < l1.length) (hl2 : l2.length - 1 < l2.length) (heq : l1.get ⟨l1.length - 1, hl1⟩ = l2.get ⟨l2.length - 1, hl2⟩) : l1 = l2

theorem List.get_last_of_concat {α : Type u_1} {last : α} {l : List α} (h : (l ++ [last]).length - 1 < (l ++ [last]).length) : (l ++ [last]).get ⟨(l ++ [last]).length - 1, h⟩ = last

theorem List.eq_succ_of_tail_nth {α : Type u_1} {n : Nat} {head : α} {tail : List α} (data : List α) (h1 : n + 1 < data.length) (h2 : data = head :: tail) (h3 : n < tail.length) : tail.get ⟨n, h3⟩ = data.get ⟨n + 1, h1⟩

theorem List.eq_succ_of_tail_nth_pred {α : Type u_1} {n : Nat} {head : α} {tail : List α} (data : List α) (h0 : n ≠ 0) (h1 : n < data.length) (h2 : data = head :: tail) (h3 : n - 1 < tail.length) : tail.get ⟨n - 1, h3⟩ = data.get ⟨n, h1⟩

theorem List.chain_split {α : Type u_1} {R : α → α → Prop} {a b : α} {l₁ l₂ : List α} : IsChain R (a :: (l₁ ++ b :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ IsChain R (b :: l₂)

theorem List.chain_append_cons_cons {α : Type u_1} {R : α → α → Prop} {a b c : α} {l₁ l₂ : List α} : IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)

theorem List.chain_iff_get {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} : IsChain R (a :: l) ↔ (∀ (h : 0 < l.length), R a (l.get ⟨0, h⟩)) ∧ ∀ (i : Nat) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

theorem List.ext_get_iff {α : Type u_1} {l₁ l₂ : List α} : l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩