Documentation

Init.Data.List.Nat.Basic

Miscellaneous List lemmas, that require more Nat lemmas than are available in Init.Data.List.Lemmas. #

In particular, omega is available here.

dropLast #

source
theorem List.tail_dropLast {α : Type u_1} (l : List α) :
l.dropLast.tail = l.tail.dropLast
source
@[simp]
theorem List.dropLast_reverse {α : Type u_1} (l : List α) :
l.reverse.dropLast = l.tail.reverse

filter #

source
theorem List.length_filter_lt_length_iff_exists {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} :
(filter p l).length < l.length ↔ ∃ (x : α✝), x ∈ l ∧ ¬p x = true

reverse #

source
theorem List.getElem_eq_getElem_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) :
l[i] = l.reverse[l.length - 1 - i]

leftpad #

source
theorem List.leftpad_length {α : Type u_1} (n : Nat) (a : α) (l : List α) :
(leftpad n a l).length = max n l.length

The length of the List returned by List.leftpad n a l is equal to the larger of n and l.length

eraseIdx #

source
theorem List.mem_eraseIdx_iff_getElem {α : Type u_1} {x : α} {l : List α} {k : Nat} :
x ∈ l.eraseIdx k ↔ ∃ (i : Nat), ∃ (h : i < l.length), i ≠ k ∧ l[i] = x
source
theorem List.mem_eraseIdx_iff_getElem? {α : Type u_1} {x : α} {l : List α} {k : Nat} :
x ∈ l.eraseIdx k ↔ ∃ (i : Nat), i ≠ k ∧ l[i]? = some x

min? #

source
theorem List.min?_eq_some_iff' {a : Nat} {xs : List Nat} :
xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b
source
theorem List.min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
l.min?.get ⋯ ≤ a
source
theorem List.min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
l.min?.getD k ≤ a

max? #

source
theorem List.max?_eq_some_iff' {a : Nat} {xs : List Nat} :
xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → b ≤ a
source
theorem List.le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
a ≤ l.max?.get ⋯
source
theorem List.le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
a ≤ l.max?.getD k
source
@[reducible, inline, deprecated List.min?_eq_some_iff' (since := "2024-09-29")]
abbrev List.minimum?_eq_some_iff' {a : Nat} {xs : List Nat} :
xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b
Equations
Instances For
    source
    @[reducible, inline, deprecated List.min?_cons' (since := "2024-09-29")]
    abbrev List.minimum?_cons' {α : Type u_1} {x : α} [Min α] {xs : List α} :
    (x :: xs).min? = some (foldl min x xs)
    Equations
    Instances For
      source
      @[reducible, inline, deprecated List.min?_getD_le_of_mem (since := "2024-09-29")]
      abbrev List.minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
      l.min?.getD k ≤ a
      Equations
      Instances For
        source
        @[reducible, inline, deprecated List.max?_eq_some_iff' (since := "2024-09-29")]
        abbrev List.maximum?_eq_some_iff' {a : Nat} {xs : List Nat} :
        xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → b ≤ a
        Equations
        Instances For
          source
          @[reducible, inline, deprecated List.max?_cons' (since := "2024-09-29")]
          abbrev List.maximum?_cons' {α : Type u_1} {x : α} [Max α] {xs : List α} :
          (x :: xs).max? = some (foldl max x xs)
          Equations
          Instances For
            source
            @[reducible, inline, deprecated List.le_max?_getD_of_mem (since := "2024-09-29")]
            abbrev List.le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
            a ≤ l.max?.getD k
            Equations
            Instances For