doc-next-gen

Mathlib.Data.List.MinMax

Module docstring

{"# Minimum and maximum of lists

Main definitions

The main definitions are argmax, argmin, minimum and maximum for lists.

argmax f l returns some a, where a of l that maximises f a. If there are a b such that f a = f b, it returns whichever of a or b comes first in the list. argmax f [] = none

minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for [] "}

List.argAux definition
(a : Option α) (b : α) : Option α
Full source 
/-- Auxiliary definition for `argmax` and `argmin`. -/
def argAux (a : Option α) (b : α) : Option α :=
  Option.casesOn a (some b) fun c => if r b c then some b else some c
Auxiliary function for argument optimization
Informal description
The auxiliary function `argAux` takes an optional value `a` of type `α` and a value `b` of type `α`, and returns an optional value of type `α`. If `a` is `none`, it returns `some b`. If `a` is `some c`, it returns `some b` if the relation `r b c` holds, otherwise it returns `some c`.
List.foldl_argAux_eq_none theorem
: l.foldl (argAux r) o = none ↔ l = [] ∧ o = none
Full source 
@[simp]
theorem foldl_argAux_eq_none : l.foldl (argAux r) o = none ↔ l = [] ∧ o = none :=
  List.reverseRecOn l (by simp) fun tl hd => by
    simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff, and_false, false_and,
      iff_false]
    cases foldl (argAux r) o tl
    · simp
    · simp only [false_iff, not_and]
      split_ifs <;> simp
Folding with `argAux` yields `none` iff the list is empty and initial value is `none`
Informal description
For any list `l` and optional value `o`, the result of folding `l` with the auxiliary function `argAux r` starting from `o` is `none` if and only if `l` is the empty list and `o` is `none`. In other words, the equality `foldl (argAux r) o l = none` holds precisely when both `l = []` and `o = none` are true.
List.argAux_self theorem
(hr₀ : Irreflexive r) (a : α) : argAux r (some a) a = a
Full source 
@[simp]
theorem argAux_self (hr₀ : Irreflexive r) (a : α) : argAux r (some a) a = a :=
  if_neg <| hr₀ _
Irreflexivity implies `argAux` preserves equality
Informal description
For an irreflexive relation $r$ and any element $a$ of type $\alpha$, the auxiliary function `argAux` satisfies $\text{argAux}_r (\text{some } a) a = a$.
List.not_of_mem_foldl_argAux theorem
(hr₀ : Irreflexive r) (hr₁ : Transitive r) : ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m
Full source 
theorem not_of_mem_foldl_argAux (hr₀ : Irreflexive r) (hr₁ : Transitive r) :
    ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m := by
  induction' l using List.reverseRecOn with tl a ih
  · simp
  intro b m o hb ho
  rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
  rcases hf : foldl (argAux r) o tl with - | c
  · rw [hf] at ho
    rw [foldl_argAux_eq_none] at hf
    simp_all [hf.1, hf.2, hr₀ _]
  rw [hf, Option.mem_def] at ho
  dsimp only at ho
  split_ifs at ho with hac <;> rcases mem_append.1 hb with h | h <;>
    injection ho with ho <;> subst ho
  · exact fun hba => ih h hf (hr₁ hba hac)
  · simp_all [hr₀ _]
  · exact ih h hf
  · simp_all
No Element in List is Related to Fold Result via Irreflexive Transitive Relation
Informal description
Let $r$ be an irreflexive and transitive relation on a type $\alpha$. For any list $l$ of elements in $\alpha$, optional value $o$, and elements $a, m \in \alpha$, if $a$ is in $l$ and $m$ is in the result of folding $l$ with $\text{argAux}_r$ starting from $o$, then it is not the case that $a \prec m$ under the relation $r$.
List.argmax definition
(f : α → β) (l : List α) : Option α
Full source 
/-- `argmax f l` returns `some a`, where `f a` is maximal among the elements of `l`, in the sense
that there is no `b ∈ l` with `f a < f b`. If `a`, `b` are such that `f a = f b`, it returns
whichever of `a` or `b` comes first in the list. `argmax f [] = none`. -/
def argmax (f : α → β) (l : List α) : Option α :=
  l.foldl (argAux fun b c => f c < f b) none
First maximal element of a list with respect to a function
Informal description
The function `argmax f l` returns an optional element of the list `l` (wrapped in `some`) that maximizes the function `f$. Specifically, it returns `some a` where `f a` is maximal in the sense that there is no `b ∈ l$ with `f a < f b`. If there are multiple elements with the same maximal value of `f`, it returns the first such element encountered in the list. If the list `l` is empty, it returns `none`.
List.argmin definition
(f : α → β) (l : List α)
Full source 
/-- `argmin f l` returns `some a`, where `f a` is minimal among the elements of `l`, in the sense
that there is no `b ∈ l` with `f b < f a`. If `a`, `b` are such that `f a = f b`, it returns
whichever of `a` or `b` comes first in the list. `argmin f [] = none`. -/
def argmin (f : α → β) (l : List α) :=
  l.foldl (argAux fun b c => f b < f c) none
First minimal element of a list with respect to a function
Informal description
The function `argmin f l` returns an optional element of the list `l` (wrapped in `some`) that minimizes the function `f`. Specifically, it returns `some a` where `f a` is minimal in the sense that there is no `b ∈ l` with `f b < f a`. If there are multiple elements with the same minimal value of `f`, it returns the first such element encountered in the list. If the list `l` is empty, it returns `none`.
List.argmax_nil theorem
(f : α → β) : argmax f [] = none
Full source 
@[simp]
theorem argmax_nil (f : α → β) : argmax f [] = none :=
  rfl
Maximizer of Empty List is None
Informal description
For any function $f : \alpha \to \beta$, the function $\text{argmax}\, f$ applied to the empty list returns $\text{none}$.
List.argmin_nil theorem
(f : α → β) : argmin f [] = none
Full source 
@[simp]
theorem argmin_nil (f : α → β) : argmin f [] = none :=
  rfl
Minimizer of Empty List is None
Informal description
For any function $f : \alpha \to \beta$, the function `argmin` applied to $f$ and the empty list `[]` returns `none`.
List.argmax_singleton theorem
{f : α → β} {a : α} : argmax f [a] = a
Full source 
@[simp]
theorem argmax_singleton {f : α → β} {a : α} : argmax f [a] = a :=
  rfl
Maximizer of Singleton List is Its Only Element
Informal description
For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the function `argmax` applied to $f$ and the singleton list $[a]$ returns $a$, i.e., $\text{argmax}\, f\, [a] = a$.
List.argmin_singleton theorem
{f : α → β} {a : α} : argmin f [a] = a
Full source 
@[simp]
theorem argmin_singleton {f : α → β} {a : α} : argmin f [a] = a :=
  rfl
Minimizer of Singleton List is Its Only Element
Informal description
For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the function `argmin` applied to $f$ and the singleton list $[a]$ returns $a$, i.e., $\text{argmin}\, f\, [a] = a$.
List.not_lt_of_mem_argmax theorem
: a ∈ l → m ∈ argmax f l → ¬f m < f a
Full source 
theorem not_lt_of_mem_argmax : a ∈ l → m ∈ argmax f l → ¬f m < f a :=
  not_of_mem_foldl_argAux _ (fun x h => lt_irrefl (f x) h)
    (fun _ _ z hxy hyz => lt_trans (a := f z) hyz hxy)
Maximal Elements Dominate All Others in List with Respect to Function $f$
Informal description
For any list $l$ of elements of type $\alpha$ and function $f : \alpha \to \beta$, if an element $a$ belongs to $l$ and $m$ is a maximal element of $l$ with respect to $f$ (i.e., $m \in \text{argmax}\, f\, l$), then it is not the case that $f(m) < f(a)$.
List.not_lt_of_mem_argmin theorem
: a ∈ l → m ∈ argmin f l → ¬f a < f m
Full source 
theorem not_lt_of_mem_argmin : a ∈ l → m ∈ argmin f l → ¬f a < f m :=
  not_of_mem_foldl_argAux _ (fun x h => lt_irrefl (f x) h)
    (fun x _ _ hxy hyz => lt_trans (a := f x) hxy hyz)
No Element in List is Strictly Smaller Than argmin's Result Under $f$
Informal description
For any function $f : \alpha \to \beta$ and list $l$ of elements in $\alpha$, if $a$ is an element of $l$ and $m$ is an element returned by $\text{argmin}\, f\, l$, then it is not the case that $f(a) < f(m)$. In other words, no element in the list has a strictly smaller value under $f$ than the minimal element found by $\text{argmin}$.
List.argmax_concat theorem
(f : α → β) (a : α) (l : List α) : argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c
Full source 
theorem argmax_concat (f : α → β) (a : α) (l : List α) :
    argmax f (l ++ [a]) =
      Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c := by
  rw [argmax, argmax]; simp [argAux]
Update Rule for `argmax` When Appending an Element
Informal description
Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ an element, and $l$ a list of elements of type $\alpha$. Then the `argmax` of $f$ over the concatenated list $l \mathbin{+\!\!+} [a]$ is computed as follows: - If the `argmax` of $f$ over $l$ is `none`, then the result is `some a`. - Otherwise, if the `argmax` of $f$ over $l$ is `some c`, then: - If $f(c) < f(a)$, the result is `some a`. - Otherwise, the result remains `some c$. In other words, when extending a list with a new element $a$, the updated `argmax` either becomes $a$ (if it strictly improves the maximum) or retains the previous maximum from $l$.
List.argmin_concat theorem
(f : α → β) (a : α) (l : List α) : argmin f (l ++ [a]) = Option.casesOn (argmin f l) (some a) fun c => if f a < f c then some a else some c
Full source 
theorem argmin_concat (f : α → β) (a : α) (l : List α) :
    argmin f (l ++ [a]) =
      Option.casesOn (argmin f l) (some a) fun c => if f a < f c then some a else some c :=
  @argmax_concat _ βᵒᵈ _ _ _ _ _
Update Rule for `argmin` When Appending an Element
Informal description
Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ an element, and $l$ a list of elements of type $\alpha$. Then the `argmin` of $f$ over the concatenated list $l \mathbin{+\!\!+} [a]$ is computed as follows: - If the `argmin` of $f$ over $l$ is `none`, then the result is `some a`. - Otherwise, if the `argmin` of $f$ over $l$ is `some c`, then: - If $f(a) < f(c)$, the result is `some a`. - Otherwise, the result remains `some c$. In other words, when extending a list with a new element $a$, the updated `argmin` either becomes $a$ (if it strictly improves the minimum) or retains the previous minimum from $l$.
List.argmax_mem theorem
: ∀ {l : List α} {m : α}, m ∈ argmax f l → m ∈ l
Full source 
theorem argmax_mem : ∀ {l : List α} {m : α}, m ∈ argmax f l → m ∈ l
  | [], m => by simp
  | hd :: tl, m => by simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m
Maximizing Element Belongs to List
Informal description
For any list $l$ of elements of type $\alpha$ and any element $m \in \alpha$, if $m$ is the result of $\text{argmax}\,f\,l$ (i.e., $m$ is an element maximizing $f$ in $l$), then $m$ must be an element of $l$.
List.argmin_mem theorem
: ∀ {l : List α} {m : α}, m ∈ argmin f l → m ∈ l
Full source 
theorem argmin_mem : ∀ {l : List α} {m : α}, m ∈ argmin f l → m ∈ l :=
  @argmax_mem _ βᵒᵈ _ _ _
Minimizing Element Belongs to List
Informal description
For any list $l$ of elements of type $\alpha$ and any element $m \in \alpha$, if $m$ is the result of $\text{argmin}\,f\,l$ (i.e., $m$ is an element minimizing $f$ in $l$), then $m$ must be an element of $l$.
List.argmax_eq_none theorem
: l.argmax f = none ↔ l = []
Full source 
@[simp]
theorem argmax_eq_none : l.argmax f = none ↔ l = [] := by simp [argmax]
Empty List Characterization for Argument Maximum
Informal description
For any list `l` and function `f`, the argument maximum `argmax f l` is `none` if and only if `l` is the empty list. In other words, $\text{argmax}_f(l) = \text{none} \leftrightarrow l = []$.
List.argmin_eq_none theorem
: l.argmin f = none ↔ l = []
Full source 
@[simp]
theorem argmin_eq_none : l.argmin f = none ↔ l = [] :=
  @argmax_eq_none _ βᵒᵈ _ _ _ _
Empty List Characterization for Argument Minimum
Informal description
For any list $l$ and function $f$, the argument minimum $\text{argmin}_f(l)$ is `none` if and only if $l$ is the empty list. In other words, $\text{argmin}_f(l) = \text{none} \leftrightarrow l = []$.
List.le_of_mem_argmax theorem
: a ∈ l → m ∈ argmax f l → f a ≤ f m
Full source 
theorem le_of_mem_argmax : a ∈ l → m ∈ argmax f l → f a ≤ f m := fun ha hm =>
  le_of_not_lt <| not_lt_of_mem_argmax ha hm
Maximal Elements Dominate All Others in List with Respect to Function $f$
Informal description
For any list $l$ of elements of type $\alpha$ and function $f : \alpha \to \beta$, if an element $a$ belongs to $l$ and $m$ is a maximal element of $l$ with respect to $f$ (i.e., $m \in \text{argmax}\, f\, l$), then $f(a) \leq f(m)$.
List.le_of_mem_argmin theorem
: a ∈ l → m ∈ argmin f l → f m ≤ f a
Full source 
theorem le_of_mem_argmin : a ∈ l → m ∈ argmin f l → f m ≤ f a :=
  @le_of_mem_argmax _ βᵒᵈ _ _ _ _ _
Minimal Elements Dominate All Others in List with Respect to Function $f$
Informal description
For any list $l$ of elements of type $\alpha$ and function $f : \alpha \to \beta$, if an element $a$ belongs to $l$ and $m$ is a minimal element of $l$ with respect to $f$ (i.e., $m \in \text{argmin}\, f\, l$), then $f(m) \leq f(a)$.
List.argmax_cons theorem
(f : α → β) (a : α) (l : List α) : argmax f (a :: l) = Option.casesOn (argmax f l) (some a) fun c => if f a < f c then some c else some a
Full source 
theorem argmax_cons (f : α → β) (a : α) (l : List α) :
    argmax f (a :: l) =
      Option.casesOn (argmax f l) (some a) fun c => if f a < f c then some c else some a :=
  List.reverseRecOn l rfl fun hd tl ih => by
    rw [← cons_append, argmax_concat, ih, argmax_concat]
    rcases h : argmax f hd with - | m
    · simp [h]
    dsimp
    rw [← apply_ite, ← apply_ite]
    dsimp
    split_ifs <;> try rfl
    · exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›
    · cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›
Update Rule for `argmax` When Prepending an Element
Informal description
Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ an element, and $l$ a list of elements of type $\alpha$. Then the `argmax` of $f$ over the list $a :: l$ is computed as follows: - If the `argmax` of $f$ over $l$ is `none`, then the result is `some a`. - Otherwise, if the `argmax` of $f$ over $l$ is `some c`, then: - If $f(a) < f(c)$, the result is `some c`. - Otherwise, the result is `some a`.
List.argmin_cons theorem
(f : α → β) (a : α) (l : List α) : argmin f (a :: l) = Option.casesOn (argmin f l) (some a) fun c => if f c < f a then some c else some a
Full source 
theorem argmin_cons (f : α → β) (a : α) (l : List α) :
    argmin f (a :: l) =
      Option.casesOn (argmin f l) (some a) fun c => if f c < f a then some c else some a :=
  @argmax_cons α βᵒᵈ _ _ _ _
Update Rule for `argmin` When Prepending an Element
Informal description
Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ an element, and $l$ a list of elements of type $\alpha$. Then the `argmin` of $f$ over the list $a :: l$ is computed as follows: - If the `argmin` of $f$ over $l$ is `none`, then the result is `some a`. - Otherwise, if the `argmin` of $f$ over $l$ is `some c`, then: - If $f(c) < f(a)$, the result is `some c`. - Otherwise, the result is `some a$.
List.index_of_argmax theorem
: ∀ {l : List α} {m : α}, m ∈ argmax f l → ∀ {a}, a ∈ l → f m ≤ f a → l.idxOf m ≤ l.idxOf a
Full source 
theorem index_of_argmax :
    ∀ {l : List α} {m : α}, m ∈ argmax f l → ∀ {a}, a ∈ l → f m ≤ f a → l.idxOf m ≤ l.idxOf a
  | [], m, _, _, _, _ => by simp
  | hd :: tl, m, hm, a, ha, ham => by
    simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢
    cases h : argmax f tl
    · rw [h] at hm
      simp_all
    rw [h] at hm
    dsimp only at hm
    simp only [cond_eq_if, beq_iff_eq]
    obtain ha | ha := ha <;> split_ifs at hm <;> injection hm with hm <;> subst hm
    · cases not_le_of_lt ‹_› ‹_›
    · rw [if_pos rfl]
    · rw [if_neg, if_neg]
      · exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
      · exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
      · exact ne_of_apply_ne _ ‹f hd < f _›.ne
    · rw [if_pos rfl]
      exact Nat.zero_le _
Index of Maximal Element is Minimal Among Equally Large Elements
Informal description
Let $l$ be a list of elements of type $\alpha$, and let $f : \alpha \to \beta$ be a function. If $m$ is an element of $l$ that maximizes $f$ (i.e., $m \in \text{argmax}_f l$), then for any element $a \in l$ such that $f(m) \leq f(a)$, the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.index_of_argmin theorem
: ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a}, a ∈ l → f a ≤ f m → l.idxOf m ≤ l.idxOf a
Full source 
theorem index_of_argmin :
    ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a}, a ∈ l → f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
  @index_of_argmax _ βᵒᵈ _ _ _
Index of Minimal Element is Minimal Among Equally Small Elements
Informal description
For any list $l$ of elements of type $\alpha$ and function $f : \alpha \to \beta$, if $m$ is a minimal element of $l$ with respect to $f$ (i.e., $m \in \text{argmin}_f l$), then for any element $a \in l$ such that $f(a) \leq f(m)$, the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.mem_argmax_iff theorem
: m ∈ argmax f l ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a
Full source 
theorem mem_argmax_iff :
    m ∈ argmax f lm ∈ argmax f l ↔
      m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a :=
  ⟨fun hm => ⟨argmax_mem hm, fun _ ha => le_of_mem_argmax ha hm, fun _ => index_of_argmax hm⟩,
    by
      rintro ⟨hml, ham, hma⟩
      rcases harg : argmax f l with - | n
      · simp_all
      · have :=
          _root_.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
            (index_of_argmax harg hml (ham _ (argmax_mem harg)))
        rw [(idxOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]⟩
Characterization of Maximal Elements in a List via argmax
Informal description
An element $m$ is in the result of $\text{argmax}\,f\,l$ if and only if: 1. $m$ is an element of the list $l$, 2. For all elements $a$ in $l$, $f(a) \leq f(m)$, and 3. For all elements $a$ in $l$, if $f(m) \leq f(a)$, then the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.argmax_eq_some_iff theorem
: argmax f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a
Full source 
theorem argmax_eq_some_iff :
    argmaxargmax f l = some m ↔
      m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a :=
  mem_argmax_iff
Characterization of `argmax` Returning `some m` for a List
Informal description
For a list $l$ of elements of type $\alpha$ and a function $f : \alpha \to \beta$, the following are equivalent: 1. The function `argmax f l` returns `some m`, where $m$ is an element of $l$. 2. The element $m$ belongs to $l$, satisfies $f(a) \leq f(m)$ for all $a \in l$, and for any $a \in l$ with $f(m) \leq f(a)$, the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.mem_argmin_iff theorem
: m ∈ argmin f l ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a
Full source 
theorem mem_argmin_iff :
    m ∈ argmin f lm ∈ argmin f l ↔
      m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
  @mem_argmax_iff _ βᵒᵈ _ _ _ _ _
Characterization of Minimal Elements in a List via argmin
Informal description
An element $m$ belongs to the result of $\text{argmin}\,f\,l$ if and only if: 1. $m$ is an element of the list $l$, 2. For all elements $a$ in $l$, $f(m) \leq f(a)$, and 3. For all elements $a$ in $l$, if $f(a) \leq f(m)$, then the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.argmin_eq_some_iff theorem
: argmin f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a
Full source 
theorem argmin_eq_some_iff :
    argminargmin f l = some m ↔
      m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
  mem_argmin_iff
Characterization of $\text{argmin}\,f\,l = \text{some}\,m$ for a List
Informal description
For a list $l$ of elements of type $\alpha$ and a function $f : \alpha \to \beta$, the following are equivalent: 1. The function $\text{argmin}\,f\,l$ returns $\text{some}\,m$, where $m$ is an element of $l$. 2. The element $m$ belongs to $l$, satisfies $f(m) \leq f(a)$ for all $a \in l$, and for any $a \in l$ with $f(a) \leq f(m)$, the index of $m$ in $l$ is less than or equal to the index of $a$ in $l$.
List.maximum definition
(l : List α) : WithBot α
Full source 
/-- `maximum l` returns a `WithBot α`, the largest element of `l` for nonempty lists, and `⊥` for
`[]` -/
def maximum (l : List α) : WithBot α :=
  argmax id l
Maximum element of a list
Informal description
The function `maximum` takes a list `l` of elements of type `α` and returns the largest element in `l` as a value in `WithBot α`. If the list is nonempty, it returns the maximal element; if the list is empty, it returns the bottom element `⊥`. The comparison is based on the preorder structure of `α`.
List.minimum definition
(l : List α) : WithTop α
Full source 
/-- `minimum l` returns a `WithTop α`, the smallest element of `l` for nonempty lists, and `⊤` for
`[]` -/
def minimum (l : List α) : WithTop α :=
  argmin id l
Minimum element of a list
Informal description
The function `minimum` takes a list `l` of elements of type `α` and returns the smallest element in `l` as a value in `WithTop α`. If the list is nonempty, it returns the minimal element; if the list is empty, it returns the top element `⊤`. The comparison is based on the preorder structure of `α`.
List.maximum_nil theorem
: maximum ([] : List α) = ⊥
Full source 
@[simp]
theorem maximum_nil : maximum ([] : List α) = ⊥ :=
  rfl
Maximum of Empty List is Bottom Element
Informal description
For any type $\alpha$ with a preorder, the maximum of the empty list is the bottom element $\bot$ in the type $\alpha$ extended with a bottom element, i.e., $\text{maximum}([]) = \bot$.
List.minimum_nil theorem
: minimum ([] : List α) = ⊤
Full source 
@[simp]
theorem minimum_nil : minimum ([] : List α) = ⊤ :=
  rfl
Minimum of Empty List is Top Element
Informal description
For any type $\alpha$ with a preorder, the minimum of the empty list is the top element $\top$ in the type $\alpha$ extended with a top element, i.e., $\text{minimum}([]) = \top$.
List.maximum_singleton theorem
(a : α) : maximum [a] = a
Full source 
@[simp]
theorem maximum_singleton (a : α) : maximum [a] = a :=
  rfl
Maximum of Singleton List is the Element Itself
Informal description
For any element $a$ of a type $\alpha$ with a preorder, the maximum of the singleton list $[a]$ is equal to $a$ itself, i.e., $\text{maximum}([a]) = a$.
List.minimum_singleton theorem
(a : α) : minimum [a] = a
Full source 
@[simp]
theorem minimum_singleton (a : α) : minimum [a] = a :=
  rfl
Minimum of Singleton List is the Element Itself
Informal description
For any element $a$ of a type $\alpha$ with a preorder, the minimum of the singleton list $[a]$ is equal to $a$ itself, i.e., $\text{minimum}([a]) = a$.
List.maximum_mem theorem
{l : List α} {m : α} : (maximum l : WithTop α) = m → m ∈ l
Full source 
theorem maximum_mem {l : List α} {m : α} : (maximum l : WithTop α) = m → m ∈ l :=
  argmax_mem
Membership of Maximum Element in List
Informal description
For any list $l$ of elements of type $\alpha$ and any element $m \in \alpha$, if the maximum element of $l$ (considered in `WithTop α`) is equal to $m$, then $m$ must be an element of $l$.
List.minimum_mem theorem
{l : List α} {m : α} : (minimum l : WithBot α) = m → m ∈ l
Full source 
theorem minimum_mem {l : List α} {m : α} : (minimum l : WithBot α) = m → m ∈ l :=
  argmin_mem
Membership of Minimum Element in List
Informal description
For any list $l$ of elements of type $\alpha$ with a preorder and any element $m \in \alpha$, if the minimum element of $l$ (considered in $\text{WithBot}\ \alpha$) is equal to $m$, then $m$ must be an element of $l$.
List.maximum_eq_bot theorem
{l : List α} : l.maximum = ⊥ ↔ l = []
Full source 
@[simp]
theorem maximum_eq_bot {l : List α} : l.maximum = ⊥ ↔ l = [] :=
  argmax_eq_none
Empty List Characterization via Maximum Element
Informal description
For any list $l$ of elements of type $\alpha$, the maximum element of $l$ (considered in `WithBot α`) is equal to the bottom element $\bot$ if and only if $l$ is the empty list. In other words, $\text{maximum}(l) = \bot \leftrightarrow l = []$.
List.minimum_eq_top theorem
{l : List α} : l.minimum = ⊤ ↔ l = []
Full source 
@[simp]
theorem minimum_eq_top {l : List α} : l.minimum = ⊤ ↔ l = [] :=
  argmin_eq_none
Empty List Characterization via Minimum Element
Informal description
For any list $l$ of elements of type $\alpha$, the minimum element of $l$ (considered in $\alpha$ extended with a top element $\top$) is equal to $\top$ if and only if $l$ is the empty list. In other words, $\text{minimum}(l) = \top \leftrightarrow l = []$.
List.not_maximum_lt_of_mem theorem
: a ∈ l → (maximum l : WithBot α) = m → ¬m < a
Full source 
theorem not_maximum_lt_of_mem : a ∈ l → (maximum l : WithBot α) = m → ¬m < a :=
  not_lt_of_mem_argmax
Maximal Element in List is Not Less Than Any Member
Informal description
For any list $l$ of elements of type $\alpha$ with a preorder, if an element $a$ belongs to $l$ and the maximum element of $l$ (considered in `WithBot α`) is equal to $m$, then it is not the case that $m < a$.
List.not_lt_minimum_of_mem theorem
: a ∈ l → (minimum l : WithTop α) = m → ¬a < m
Full source 
theorem not_lt_minimum_of_mem : a ∈ l → (minimum l : WithTop α) = m → ¬a < m :=
  not_lt_of_mem_argmin
No Element in List is Strictly Less Than the Minimum
Informal description
For any element $a$ in a list $l$ of type $\alpha$, if the minimum element of $l$ (considered in $\alpha$ extended with a top element $\top$) is equal to $m$, then it is not the case that $a < m$ under the preorder on $\alpha$.
List.not_maximum_lt_of_mem' theorem
(ha : a ∈ l) : ¬maximum l < (a : WithBot α)
Full source 
theorem not_maximum_lt_of_mem' (ha : a ∈ l) : ¬maximum l < (a : WithBot α) := by
  cases h : l.maximum <;> simp_all [not_maximum_lt_of_mem ha]
Maximum Element in List is Not Less Than Any Member (variant)
Informal description
For any element $a$ in a list $l$ of elements of type $\alpha$ with a preorder, the maximum element of $l$ (considered in `WithBot α`) is not strictly less than $a$.
List.not_lt_minimum_of_mem' theorem
(ha : a ∈ l) : ¬(a : WithTop α) < minimum l
Full source 
theorem not_lt_minimum_of_mem' (ha : a ∈ l) : ¬(a : WithTop α) < minimum l := by
  cases h : l.minimum <;> simp_all [not_lt_minimum_of_mem ha]
No List Element is Strictly Below the Minimum
Informal description
For any element $a$ in a list $l$ of type $\alpha$ with a preorder, the element $a$ (considered in $\alpha$ extended with a top element $\top$) is not strictly less than the minimum element of $l$.
List.maximum_concat theorem
(a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a
Full source 
theorem maximum_concat (a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a := by
  simp only [maximum, argmax_concat, id]
  cases argmax id l
  · exact (max_eq_right bot_le).symm
  · simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]
Maximum of Concatenated List: $\text{maximum}(l \mathbin{+\!\!+} [a]) = \max(\text{maximum}(l), a)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the maximum element of the concatenated list $l \mathbin{+\!\!+} [a]$ is equal to the maximum of the maximum element of $l$ and $a$. In other words, $\text{maximum}(l \mathbin{+\!\!+} [a]) = \max(\text{maximum}(l), a)$.
List.le_maximum_of_mem theorem
: a ∈ l → (maximum l : WithBot α) = m → a ≤ m
Full source 
theorem le_maximum_of_mem : a ∈ l → (maximum l : WithBot α) = m → a ≤ m :=
  le_of_mem_argmax
Elements are Bounded by List Maximum: $a \in l \to \text{maximum}(l) = m \to a \leq m$
Informal description
For any element $a$ in a list $l$ of type $\alpha$, if the maximum element of $l$ (considered in `WithBot α`) is equal to $m$, then $a \leq m$.
List.minimum_le_of_mem theorem
: a ∈ l → (minimum l : WithTop α) = m → m ≤ a
Full source 
theorem minimum_le_of_mem : a ∈ l → (minimum l : WithTop α) = m → m ≤ a :=
  le_of_mem_argmin
Elements Bound the List Minimum: $a \in l \to \text{minimum}(l) = m \to m \leq a$
Informal description
For any element $a$ in a list $l$ of type $\alpha$, if the minimum element of $l$ (considered in $\text{WithTop}\ \alpha$) is equal to $m$, then $m \leq a$.
List.le_maximum_of_mem' theorem
(ha : a ∈ l) : (a : WithBot α) ≤ maximum l
Full source 
theorem le_maximum_of_mem' (ha : a ∈ l) : (a : WithBot α) ≤ maximum l :=
  le_of_not_lt <| not_maximum_lt_of_mem' ha
Elements are Bounded by List Maximum: $a \in l \Rightarrow a \leq \text{maximum}(l)$
Informal description
For any element $a$ in a list $l$ of elements of type $\alpha$ with a linear order, the element $a$ (considered in `WithBot α`) is less than or equal to the maximum element of $l$.
List.minimum_le_of_mem' theorem
(ha : a ∈ l) : minimum l ≤ (a : WithTop α)
Full source 
theorem minimum_le_of_mem' (ha : a ∈ l) : minimum l ≤ (a : WithTop α) :=
  le_of_not_lt <| not_lt_minimum_of_mem' ha
Minimum Element is Less Than or Equal to Any List Member
Informal description
For any element $a$ in a list $l$ of elements of type $\alpha$ with a linear order, the minimum element of $l$ (considered in $\alpha$ extended with a top element $\top$) is less than or equal to $a$.
List.minimum_concat theorem
(a : α) (l : List α) : minimum (l ++ [a]) = min (minimum l) a
Full source 
theorem minimum_concat (a : α) (l : List α) : minimum (l ++ [a]) = min (minimum l) a :=
  @maximum_concat αᵒᵈ _ _ _
Minimum of Concatenated List: $\text{minimum}(l \mathbin{+\!\!+} [a]) = \min(\text{minimum}(l), a)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the minimum element of the concatenated list $l \mathbin{+\!\!+} [a]$ is equal to the minimum of the minimum element of $l$ and $a$. In other words, $\text{minimum}(l \mathbin{+\!\!+} [a]) = \min(\text{minimum}(l), a)$.
List.maximum_cons theorem
(a : α) (l : List α) : maximum (a :: l) = max ↑a (maximum l)
Full source 
theorem maximum_cons (a : α) (l : List α) : maximum (a :: l) = max ↑a (maximum l) :=
  List.reverseRecOn l (by simp [@max_eq_left (WithBot α) _ _ _ bot_le]) fun tl hd ih => by
    rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
Maximum of Cons List: $\text{maximum}(a :: l) = \max(a, \text{maximum}(l))$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the maximum element of the list obtained by prepending $a$ to $l$ is equal to the maximum of $a$ and the maximum element of $l$. In other words, $\text{maximum}(a :: l) = \max(a, \text{maximum}(l))$.
List.minimum_cons theorem
(a : α) (l : List α) : minimum (a :: l) = min ↑a (minimum l)
Full source 
theorem minimum_cons (a : α) (l : List α) : minimum (a :: l) = min ↑a (minimum l) :=
  @maximum_cons αᵒᵈ _ _ _
Minimum of Cons List: $\text{minimum}(a :: l) = \min(a, \text{minimum}(l))$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the minimum element of the list obtained by prepending $a$ to $l$ is equal to the minimum of $a$ and the minimum element of $l$. In other words, $\text{minimum}(a :: l) = \min(a, \text{minimum}(l))$.
List.maximum_append theorem
(l₁ l₂ : List α) : (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum
Full source 
lemma maximum_append (l₁ l₂ : List α) : (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum := by
  induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
Maximum of Concatenated Lists: $\text{maximum}(l_1 ++ l_2) = \max(\text{maximum}(l_1), \text{maximum}(l_2))$
Informal description
For any two lists $l_1$ and $l_2$ of elements of a linearly ordered type $\alpha$, the maximum element of the concatenated list $l_1 ++ l_2$ is equal to the maximum of the maximum elements of $l_1$ and $l_2$ individually, i.e., $\text{maximum}(l_1 ++ l_2) = \max(\text{maximum}(l_1), \text{maximum}(l_2))$.
List.minimum_append theorem
(l₁ l₂ : List α) : (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum
Full source 
lemma minimum_append (l₁ l₂ : List α) : (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum :=
  @maximum_append αᵒᵈ _ _ _
Minimum of Concatenated Lists: $\text{minimum}(l_1 ++ l_2) = \min(\text{minimum}(l_1), \text{minimum}(l_2))$
Informal description
For any two lists $l_1$ and $l_2$ of elements of a linearly ordered type $\alpha$, the minimum element of the concatenated list $l_1 ++ l_2$ is equal to the minimum of the minimum elements of $l_1$ and $l_2$ individually, i.e., $\text{minimum}(l_1 ++ l_2) = \min(\text{minimum}(l_1), \text{minimum}(l_2))$.
List.maximum_le_of_forall_le theorem
{b : WithBot α} (h : ∀ a ∈ l, a ≤ b) : l.maximum ≤ b
Full source 
theorem maximum_le_of_forall_le {b : WithBot α} (h : ∀ a ∈ l, a ≤ b) : l.maximum ≤ b := by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [maximum_cons, max_le_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩
Maximum of List is Bounded by Common Upper Bound
Informal description
For any list $l$ of elements of type $\alpha$ and any upper bound $b$ (in `WithBot α`), if every element $a$ in $l$ satisfies $a \leq b$, then the maximum element of $l$ (computed as `l.maximum`) is also less than or equal to $b$.
List.le_minimum_of_forall_le theorem
{b : WithTop α} (h : ∀ a ∈ l, b ≤ a) : b ≤ l.minimum
Full source 
theorem le_minimum_of_forall_le {b : WithTop α} (h : ∀ a ∈ l, b ≤ a) : b ≤ l.minimum := by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [minimum_cons, le_min_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩
Lower Bound Property of List Minimum: $b \leq \text{minimum}(l)$ if $b \leq a$ for all $a \in l$
Informal description
For any list $l$ of elements of type $\alpha$ and any element $b$ in $\text{WithTop}\ \alpha$, if $b$ is less than or equal to every element $a$ in $l$, then $b$ is less than or equal to the minimum element of $l$.
List.maximum_mono theorem
{l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.maximum ≤ l₂.maximum
Full source 
theorem maximum_mono {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.maximum ≤ l₂.maximum :=
  maximum_le_of_forall_le fun _ ↦ (le_maximum_of_mem' <| h ·)
Monotonicity of List Maximum: $l_1 \subseteq l_2 \Rightarrow \text{maximum}(l_1) \leq \text{maximum}(l_2)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$ with a linear order, if $l_1$ is a sublist of $l_2$ (i.e., every element of $l_1$ is also in $l_2$), then the maximum element of $l_1$ is less than or equal to the maximum element of $l_2$ (both considered in `WithBot α`).
List.minimum_anti theorem
{l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₂.minimum ≤ l₁.minimum
Full source 
theorem minimum_anti {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₂.minimum ≤ l₁.minimum :=
  @maximum_mono αᵒᵈ _ _ _ h
Antitonicity of List Minimum: $l_1 \subseteq l_2 \Rightarrow \text{minimum}(l_2) \leq \text{minimum}(l_1)$
Informal description
For any two lists $l_1$ and $l_2$ of elements of a linearly ordered type $\alpha$, if $l_1$ is a sublist of $l_2$ (i.e., $l_1 \subseteq l_2$), then the minimum element of $l_2$ is less than or equal to the minimum element of $l_1$ (both considered in `WithTop α`).
List.maximum_eq_coe_iff theorem
: maximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m
Full source 
theorem maximum_eq_coe_iff : maximummaximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m := by
  rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
  simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
  intro _ h a hal hma
  rw [_root_.le_antisymm hma (h a hal)]
Characterization of List Maximum: $\text{maximum}(l) = m \leftrightarrow (m \in l \land \forall a \in l, a \leq m)$
Informal description
For a list $l$ of elements in a linearly ordered type $\alpha$ and an element $m \in \alpha$, the maximum of $l$ (as a `WithBot α` value) equals $m$ if and only if $m$ is an element of $l$ and every element $a$ in $l$ satisfies $a \leq m$.
List.minimum_eq_coe_iff theorem
: minimum l = m ↔ m ∈ l ∧ ∀ a ∈ l, m ≤ a
Full source 
theorem minimum_eq_coe_iff : minimumminimum l = m ↔ m ∈ l ∧ ∀ a ∈ l, m ≤ a :=
  @maximum_eq_coe_iff αᵒᵈ _ _ _
Characterization of List Minimum: $\text{minimum}(l) = m \leftrightarrow (m \in l \land \forall a \in l, m \leq a)$
Informal description
For a list $l$ of elements in a linearly ordered type $\alpha$ and an element $m \in \alpha$, the minimum of $l$ (as a `WithTop α` value) equals $m$ if and only if $m$ is an element of $l$ and every element $a$ in $l$ satisfies $m \leq a$.
List.coe_le_maximum_iff theorem
: a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b
Full source 
theorem coe_le_maximum_iff : a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b := by
  induction' l <;> simp [maximum_cons, *]
Characterization of List Maximum: $a \leq \text{maximum}(l) \leftrightarrow \exists b \in l, a \leq b$
Informal description
For any element $a$ of a linearly ordered type $\alpha$ and any list $l$ of elements of $\alpha$, the inequality $a \leq \text{maximum}(l)$ holds if and only if there exists an element $b$ in $l$ such that $a \leq b$.
List.minimum_le_coe_iff theorem
: l.minimum ≤ a ↔ ∃ b, b ∈ l ∧ b ≤ a
Full source 
theorem minimum_le_coe_iff : l.minimum ≤ a ↔ ∃ b, b ∈ l ∧ b ≤ a := by
  induction' l <;> simp [minimum_cons, *]
Characterization of List Minimum: $\text{minimum}(l) \leq a \leftrightarrow \exists b \in l, b \leq a$
Informal description
For any list $l$ of elements of a linearly ordered type $\alpha$ and any element $a \in \alpha$, the minimum element of $l$ (as a value in $\text{WithTop}\ \alpha$) is less than or equal to $a$ if and only if there exists an element $b \in l$ such that $b \leq a$.
List.maximum_ne_bot_of_ne_nil theorem
(h : l ≠ []) : l.maximum ≠ ⊥
Full source 
theorem maximum_ne_bot_of_ne_nil (h : l ≠ []) : l.maximum ≠ ⊥ :=
  match l, h with | _ :: _, _ => by simp [maximum_cons]
Nonempty Lists Have Non-Bottom Maximum
Informal description
For any nonempty list $l$ of elements of a linearly ordered type $\alpha$, the maximum element of $l$ is not the bottom element $\bot$ of `WithBot α`.
List.minimum_ne_top_of_ne_nil theorem
(h : l ≠ []) : l.minimum ≠ ⊤
Full source 
theorem minimum_ne_top_of_ne_nil (h : l ≠ []) : l.minimum ≠ ⊤ :=
  @maximum_ne_bot_of_ne_nil αᵒᵈ _ _ h
Nonempty Lists Have Non-Top Minimum: $l \neq [] \implies \text{minimum}(l) \neq \top$
Informal description
For any nonempty list $l$ of elements of a linearly ordered type $\alpha$, the minimum element of $l$ (considered in `WithTop α`) is not equal to the top element $\top$.
List.maximum_ne_bot_of_length_pos theorem
(h : 0 < l.length) : l.maximum ≠ ⊥
Full source 
theorem maximum_ne_bot_of_length_pos (h : 0 < l.length) : l.maximum ≠ ⊥ :=
  match l, h with | _ :: _, _ => by simp [maximum_cons]
Nonempty Lists Have Non-Bottom Maximum: $\text{length}(l) > 0 \implies \text{maximum}(l) \neq \bot$
Informal description
For any nonempty list $l$ (i.e., a list with length greater than 0), the maximum element of $l$ (considered in `WithBot α`) is not equal to the bottom element $\bot$.
List.minimum_ne_top_of_length_pos theorem
(h : 0 < l.length) : l.minimum ≠ ⊤
Full source 
theorem minimum_ne_top_of_length_pos (h : 0 < l.length) : l.minimum ≠ ⊤ :=
  maximum_ne_bot_of_length_pos (α := αᵒᵈ) h
Nonempty Lists Have Non-Top Minimum: $\text{length}(l) > 0 \implies \text{minimum}(l) \neq \top$
Informal description
For any nonempty list $l$ (i.e., a list with length greater than 0), the minimum element of $l$ (considered in `WithTop α`) is not equal to the top element $\top$.
List.maximum_of_length_pos definition
(h : 0 < l.length) : α
Full source 
/-- The maximum value in a non-empty `List`. -/
def maximum_of_length_pos (h : 0 < l.length) : α :=
  WithBot.unbot l.maximum (maximum_ne_bot_of_length_pos h)
Maximum element of a nonempty list
Informal description
For a nonempty list $l$ (i.e., when $0 < \text{length}(l)$), the function returns the maximum element of $l$ as an element of type $\alpha$. This is obtained by extracting the underlying value from `WithBot α` using the proof that the maximum is not $\bot$ when the list is nonempty.
List.minimum_of_length_pos definition
(h : 0 < l.length) : α
Full source 
/-- The minimum value in a non-empty `List`. -/
def minimum_of_length_pos (h : 0 < l.length) : α :=
  maximum_of_length_pos (α := αᵒᵈ) h
Minimum element of a nonempty list
Informal description
For a nonempty list $l$ (i.e., when $0 < \text{length}(l)$), the function returns the minimum element of $l$ as an element of type $\alpha$. This is obtained by considering the maximum element in the order dual $\alpha^{\text{op}}$, where the order is reversed.
List.coe_maximum_of_length_pos theorem
(h : 0 < l.length) : (l.maximum_of_length_pos h : α) = l.maximum
Full source 
@[simp]
lemma coe_maximum_of_length_pos (h : 0 < l.length) :
    (l.maximum_of_length_pos h : α) = l.maximum :=
  WithBot.coe_unbot _ _
Equality of Maximum Element in Nonempty List and Its `WithBot` Representation
Informal description
For any nonempty list $l$ (i.e., when $0 < \text{length}(l)$), the maximum element of $l$ (as an element of type $\alpha$) is equal to the maximum element of $l$ considered in `WithBot α$. In other words, $(l.\text{maximum\_of\_length\_pos}\ h : \alpha) = l.\text{maximum}$.
List.coe_minimum_of_length_pos theorem
(h : 0 < l.length) : (l.minimum_of_length_pos h : α) = l.minimum
Full source 
@[simp]
lemma coe_minimum_of_length_pos (h : 0 < l.length) :
    (l.minimum_of_length_pos h : α) = l.minimum :=
  WithTop.coe_untop _ _
Equality of Minimum Element in Nonempty List and Its $\text{WithTop}$ Representation
Informal description
For any nonempty list $l$ (i.e., when $0 < \text{length}(l)$), the minimum element of $l$ (as an element of type $\alpha$) is equal to the minimum element of $l$ considered in $\text{WithTop}\ \alpha$. In other words, $(l.\text{minimum\_of\_length\_pos}\ h : \alpha) = l.\text{minimum}$.
List.le_maximum_of_length_pos_iff theorem
{b : α} (h : 0 < l.length) : b ≤ maximum_of_length_pos h ↔ b ≤ l.maximum
Full source 
@[simp]
theorem le_maximum_of_length_pos_iff {b : α} (h : 0 < l.length) :
    b ≤ maximum_of_length_pos h ↔ b ≤ l.maximum :=
  WithBot.le_unbot_iff _
Inequality Characterization for Maximum of Nonempty List
Informal description
For any nonempty list $l$ (i.e., $0 < \text{length}(l)$) and any element $b$ of type $\alpha$, the inequality $b \leq \text{maximum\_of\_length\_pos}(l, h)$ holds if and only if $b \leq \text{maximum}(l)$ holds in `WithBot α`.
List.minimum_of_length_pos_le_iff theorem
{b : α} (h : 0 < l.length) : minimum_of_length_pos h ≤ b ↔ l.minimum ≤ b
Full source 
@[simp]
theorem minimum_of_length_pos_le_iff {b : α} (h : 0 < l.length) :
    minimum_of_length_posminimum_of_length_pos h ≤ b ↔ l.minimum ≤ b :=
  WithTop.untop_le_iff _
Inequality Characterization for Minimum of Nonempty List: $\text{minimum\_of\_length\_pos}(l, h) \leq b \leftrightarrow \text{minimum}(l) \leq b$
Informal description
For any nonempty list $l$ (i.e., $\text{length}(l) > 0$) and any element $b$ of type $\alpha$, the minimum element of $l$ (obtained via $\text{minimum\_of\_length\_pos}$) is less than or equal to $b$ if and only if the minimum element of $l$ (considered in $\text{WithTop}\ \alpha$) is less than or equal to $b$.
List.le_maximum_of_length_pos_of_mem theorem
(h : a ∈ l) (w : 0 < l.length) : a ≤ l.maximum_of_length_pos w
Full source 
theorem le_maximum_of_length_pos_of_mem (h : a ∈ l) (w : 0 < l.length) :
    a ≤ l.maximum_of_length_pos w := by
  simp only [le_maximum_of_length_pos_iff]
  exact le_maximum_of_mem' h
Element in Nonempty List is Bounded by Maximum: $a \in l \Rightarrow a \leq \text{max}(l)$
Informal description
For any element $a$ in a nonempty list $l$ of elements of type $\alpha$ with a linear order, $a$ is less than or equal to the maximum element of $l$.
List.minimum_of_length_pos_le_of_mem theorem
(h : a ∈ l) (w : 0 < l.length) : l.minimum_of_length_pos w ≤ a
Full source 
theorem minimum_of_length_pos_le_of_mem (h : a ∈ l) (w : 0 < l.length) :
    l.minimum_of_length_pos w ≤ a :=
  le_maximum_of_length_pos_of_mem (α := αᵒᵈ) h w
Minimum Element Bounds All Elements in Nonempty List: $\text{min}(l) \leq a$ for $a \in l$
Informal description
For any element $a$ in a nonempty list $l$ (i.e., $0 < \text{length}(l)$) of elements of a linearly ordered type $\alpha$, the minimum element of $l$ is less than or equal to $a$.
List.getD_max?_eq_unbotD_maximum theorem
(l : List α) (d : α) : l.max?.getD d = l.maximum.unbotD d
Full source 
lemma getD_max?_eq_unbotD_maximum (l : List α) (d : α) : l.max?.getD d = l.maximum.unbotD d := by
  cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)
      all_goals simp [le_total]
Equality of Default Maximum Operations: $\text{getD}(\text{max?}(l), d) = \text{unbotD}(\text{maximum}(l), d)$
Informal description
For any list $l$ of elements of type $\alpha$ and any default value $d \in \alpha$, the result of applying `getD` to the optional maximum of $l$ with default $d$ is equal to applying `unbotD` to the maximum of $l$ with the same default $d$. In other words, $\text{getD}(\text{max?}(l), d) = \text{unbotD}(\text{maximum}(l), d)$.
List.getD_min?_eq_untopD_minimum theorem
(l : List α) (d : α) : l.min?.getD d = l.minimum.untopD d
Full source 
lemma getD_min?_eq_untopD_minimum (l : List α) (d : α) : l.min?.getD d = l.minimum.untopD d :=
  getD_max?_eq_unbotD_maximum (α := αᵒᵈ) _ _
Equality of Default Minimum Operations: $\text{getD}(\text{min?}(l), d) = \text{untopD}(\text{minimum}(l), d)$
Informal description
For any list $l$ of elements of type $\alpha$ and any default value $d \in \alpha$, the result of applying `getD` to the optional minimum of $l$ with default $d$ is equal to applying `untopD` to the minimum of $l$ with the same default $d$. In other words, $\text{getD}(\text{min?}(l), d) = \text{untopD}(\text{minimum}(l), d)$.
List.foldr_max_of_ne_nil theorem
(h : l ≠ []) : ↑(l.foldr max ⊥) = l.maximum
Full source 
@[simp]
theorem foldr_max_of_ne_nil (h : l ≠ []) : ↑(l.foldr max ⊥) = l.maximum := by
  induction' l with hd tl IH
  · contradiction
  · rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]
Right Fold Maximum Equals List Maximum for Nonempty Lists
Informal description
For any nonempty list $l$ of elements in a type $\alpha$ with a linear order, the embedding of the right fold of $l$ with the $\max$ operation starting from $\bot$ is equal to the maximum element of $l$ in `WithBot α`. That is, $\uparrow(\text{foldr}\ \max\ \bot\ l) = \text{maximum}(l)$.
List.max_le_of_forall_le theorem
(l : List α) (a : α) (h : ∀ x ∈ l, x ≤ a) : l.foldr max ⊥ ≤ a
Full source 
theorem max_le_of_forall_le (l : List α) (a : α) (h : ∀ x ∈ l, x ≤ a) : l.foldr max ⊥ ≤ a := by
  induction' l with y l IH
  · simp
  · simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx
Maximum of List is Bounded by Common Upper Bound
Informal description
For any list $l$ of elements in a type $\alpha$ with a linear order and a bottom element $\bot$, and for any element $a \in \alpha$, if every element $x$ in $l$ satisfies $x \leq a$, then the maximum of $l$ (computed via a right fold with $\max$ and $\bot$) is also less than or equal to $a$.
List.le_max_of_le theorem
{l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max ⊥
Full source 
theorem le_max_of_le {l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max ⊥ := by
  induction' l with y l IH
  · exact absurd hx not_mem_nil
  · obtain hl | hl := hx
    · simp only [foldr, foldr_cons]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))
Element in List Bounds Maximum
Informal description
For any list $l$ of elements in a linearly ordered type $\alpha$ with a bottom element $\bot$, if an element $x$ belongs to $l$ and $a \leq x$ for some $a \in \alpha$, then $a$ is less than or equal to the maximum of $l$, where the maximum is computed as the right fold of the list with the $\max$ operation starting from $\bot$.
List.foldr_min_of_ne_nil theorem
(h : l ≠ []) : ↑(l.foldr min ⊤) = l.minimum
Full source 
@[simp]
theorem foldr_min_of_ne_nil (h : l ≠ []) : ↑(l.foldr min ⊤) = l.minimum :=
  @foldr_max_of_ne_nil αᵒᵈ _ _ _ h
Right Fold Minimum Equals List Minimum for Nonempty Lists
Informal description
For any nonempty list $l$ of elements in a linearly ordered type $\alpha$ with a top element $\top$, the embedding of the right fold of $l$ with the $\min$ operation starting from $\top$ is equal to the minimum element of $l$ in $\text{WithTop}\ \alpha$. That is, $\uparrow(\text{foldr}\ \min\ \top\ l) = \text{minimum}(l)$.
List.le_min_of_forall_le theorem
(l : List α) (a : α) (h : ∀ x ∈ l, a ≤ x) : a ≤ l.foldr min ⊤
Full source 
theorem le_min_of_forall_le (l : List α) (a : α) (h : ∀ x ∈ l, a ≤ x) : a ≤ l.foldr min ⊤ :=
  @max_le_of_forall_le αᵒᵈ _ _ _ _ h
Lower Bound Property for List Minimum: $a \leq \min(l)$ if $a \leq x$ for all $x \in l$
Informal description
For any list $l$ of elements in a linearly ordered type $\alpha$ with a top element $\top$, and for any element $a \in \alpha$, if every element $x$ in $l$ satisfies $a \leq x$, then $a$ is less than or equal to the minimum of $l$ (computed via a right fold with $\min$ and $\top$).
List.min_le_of_le theorem
(l : List α) (a : α) {x : α} (hx : x ∈ l) (h : x ≤ a) : l.foldr min ⊤ ≤ a
Full source 
theorem min_le_of_le (l : List α) (a : α) {x : α} (hx : x ∈ l) (h : x ≤ a) : l.foldr min ⊤ ≤ a :=
  @le_max_of_le αᵒᵈ _ _ _ _ _ hx h
Minimum of List is Lower Bound for Elements
Informal description
For any list $l$ of elements in a linearly ordered type $\alpha$ with a top element $\top$, if an element $x$ belongs to $l$ and satisfies $x \leq a$ for some $a \in \alpha$, then the minimum of $l$ (computed via a right fold with $\min$ and $\top$) is less than or equal to $a$.
List.le_max_of_le' theorem
{l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : a ≤ x) : a ≤ l.foldr max b
Full source 
/-- If `a ≤ x` for some `x` in the list `l`, and `b : α`, then `a ≤ l.foldr max b`. -/
theorem le_max_of_le' {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : a ≤ x) :
    a ≤ l.foldr max b := by
  induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr, List.foldr_cons]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)
Upper Bound Property for List Maximum via Fold
Informal description
For any list $l$ of elements in a linearly ordered type $\alpha$, if there exists an element $x \in l$ such that $a \leq x$ for some $a \in \alpha$, then for any $b \in \alpha$, we have $a \leq \text{foldr max } b\ l$.
List.min_le_of_le' theorem
{l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : x ≤ a) : l.foldr min b ≤ a
Full source 
theorem min_le_of_le' {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : x ≤ a) : l.foldr min b ≤ a :=
  @le_max_of_le' αᵒᵈ _ _ _ _ _ hx h
Lower Bound Property for List Minimum via Fold
Informal description
For any list $l$ of elements in a linearly ordered type $\alpha$, if there exists an element $x \in l$ such that $x \leq a$ for some $a \in \alpha$, then for any $b \in \alpha$, the minimum of $l$ (computed via $\text{foldr min } b\ l$) is less than or equal to $a$.