doc-next-gen

Init.Data.List.MinMax

Module docstring

{"# Lemmas about List.min? and `List.max?. ","## Minima and maxima ","### min? ","### max? "}

List.min?_nil theorem
[Min α] : ([] : List α).min? = none
Full source 
@[simp] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
Minimum of Empty List is None
Informal description
For any type $\alpha$ with a minimum operation `Min α`, the minimum of the empty list `[]` is `none`.
List.min?_cons' theorem
[Min α] {xs : List α} : (x :: xs).min? = foldl min x xs
Full source 
theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = foldl min x xs := rfl
Minimum of Non-Empty List via Left Fold
Informal description
For any type $\alpha$ with a minimum operation and any non-empty list $x :: \text{xs}$ of elements of type $\alpha$, the minimum of the list is equal to the left fold of the `min` operation over the list starting with the initial value $x$.
List.min?_cons theorem
[Min α] [Std.Associative (min : α → α → α)] {xs : List α} : (x :: xs).min? = some (xs.min?.elim x (min x))
Full source 
@[simp] theorem min?_cons [Min α] [Std.Associative (min : α → α → α)] {xs : List α} :
    (x :: xs).min? = some (xs.min?.elim x (min x)) := by
  cases xs <;> simp [min?_cons', foldl_assoc]
Minimum of Non-Empty List via Associative Operation
Informal description
For any type $\alpha$ with a minimum operation `min` that is associative, and for any non-empty list $x :: \text{xs}$ of elements of type $\alpha$, the minimum of the list is equal to `some` applied to the minimum of $x$ and the minimum of $\text{xs}$ (with $x$ as the default value if $\text{xs}$ is empty). In symbols: $$ \text{min?}(x :: \text{xs}) = \text{some}\left(\text{min?}(\text{xs}).\text{elim}\ x\ (\text{min}\ x)\right) $$
List.min?_eq_none_iff theorem
{xs : List α} [Min α] : xs.min? = none ↔ xs = []
Full source 
@[simp] theorem min?_eq_none_iff {xs : List α} [Min α] : xs.min? = none ↔ xs = [] := by
  cases xs <;> simp [min?]
Minimum of Empty List is None
Informal description
For any list `xs` of elements of type `α` with a minimum operation, the minimum value of `xs` is `none` if and only if `xs` is the empty list.
List.isSome_min?_of_mem theorem
{l : List α} [Min α] {a : α} (h : a ∈ l) : l.min?.isSome
Full source 
theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
    l.min?.isSome := by
  cases l <;> simp_all [min?_cons']
Non-emptiness of Minimum Option for Non-empty Lists
Informal description
For any list $l$ of elements of type $\alpha$ with a minimum operation, if an element $a \in \alpha$ is a member of $l$, then the optional minimum value of $l$ is non-empty (i.e., `l.min?.isSome` is true).
List.min?_eq_head? theorem
{α : Type u} [Min α] {l : List α} (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head?
Full source 
theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
    (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head? := by
  cases l with
  | nil => rfl
  | cons x l =>
    rw [head?_cons, min?_cons', Option.some.injEq]
    induction l generalizing x with
    | nil => simp
    | cons y l ih =>
      have hx : min x y = x := rel_of_pairwise_cons h mem_cons_self
      rw [foldl_cons, ih _ (hx.symm ▸ h.sublist (by simp)), hx]
Minimum of Pairwise Ordered List Equals Head
Informal description
For any type $\alpha$ with a minimum operation and any list $l$ of elements of type $\alpha$, if $l$ is pairwise ordered such that for any two elements $a$ and $b$ in $l$, the minimum $\min(a, b) = a$, then the minimum value of $l$ is equal to the head of $l$ (i.e., $\text{min?}(l) = \text{head?}(l)$).
List.min?_mem theorem
[Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) : {xs : List α} → xs.min? = some a → a ∈ xs
Full source 
theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, minmin a b = a ∨ min a b = b) :
    {xs : List α} → xs.min? = some a → a ∈ xs := by
  intro xs
  match xs with
  | nil => simp
  | x :: xs =>
    simp only [min?_cons', Option.some.injEq, mem_cons]
    intro eq
    induction xs generalizing x with
    | nil =>
      simp at eq
      simp [eq]
    | cons y xs ind =>
      simp at eq
      have p := ind _ eq
      cases p with
      | inl p =>
        cases min_eq_or x y with | _ q => simp [p, q]
      | inr p => simp [p, mem_cons]
Minimum Element Belongs to List
Informal description
For any type $\alpha$ with a minimum operation `min` satisfying the property that for all $a, b \in \alpha$, either $\min(a, b) = a$ or $\min(a, b) = b$, and for any list $xs$ of elements of type $\alpha$, if the minimum value of $xs$ is `some a`, then $a$ is an element of $xs$.
List.le_min?_iff theorem
[Min α] [LE α] (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) : {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
Full source 
theorem le_min?_iff [Min α] [LE α]
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
    {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
  | nil => by simp
  | cons x xs => by
    rw [min?]
    intro eq y
    simp only [Option.some.injEq] at eq
    induction xs generalizing x with
    | nil =>
      simp at eq
      simp [eq]
    | cons z xs ih =>
      simp at eq
      simp [ih _ eq, le_min_iff, and_assoc]
Characterization of Minimum Element in List via Universal Bound
Informal description
Let $\alpha$ be a type equipped with a minimum operation `min` and a less-than-or-equal relation `≤`. Suppose that for all $a, b, c \in \alpha$, the inequality $a \leq \min(b, c)$ holds if and only if both $a \leq b$ and $a \leq c$ hold. For any list `xs` of elements of $\alpha$, if the minimum element of `xs` exists and is equal to some $a \in \alpha$, then for any $x \in \alpha$, the following are equivalent: 1. $x \leq a$ 2. For all $b \in \text{xs}$, $x \leq b$.
List.min?_replicate theorem
[Min α] {n : Nat} {a : α} (w : min a a = a) : (replicate n a).min? = if n = 0 then none else some a
Full source 
theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
    (replicate n a).min? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons']
Minimum of Replicated List: $\text{min?}(\text{replicate}(n, a)) = \text{if } n = 0 \text{ then none else some }a$
Informal description
For any type $\alpha$ with a minimum operation $\min$ satisfying $\min(a, a) = a$ for all $a \in \alpha$, and for any natural number $n$ and element $a \in \alpha$, the minimum element of the list $\text{replicate}(n, a)$ (a list containing $n$ copies of $a$) is $\text{some }a$ if $n > 0$, and $\text{none}$ if $n = 0$.
List.min?_replicate_of_pos theorem
[Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : (replicate n a).min? = some a
Full source 
@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
    (replicate n a).min? = some a := by
  simp [min?_replicate, Nat.ne_of_gt h, w]
Minimum of Nonempty Replicated List is Some $a$
Informal description
For any type $\alpha$ with a minimum operation $\min$ satisfying $\min(a, a) = a$ for all $a \in \alpha$, and for any natural number $n > 0$ and element $a \in \alpha$, the minimum element of the list consisting of $n$ copies of $a$ is $\text{some }a$.
List.foldl_min theorem
[Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)] {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a)
Full source 
theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
    {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
  cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]
Left Fold of Minimum Operation on Lists Equals Minimum of Initial Value and List Minimum
Informal description
Let $\alpha$ be a type equipped with a minimum operation $\min$ that is associative and idempotent. For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the left fold of $l$ with operation $\min$ and initial value $a$ equals the minimum of $a$ and the minimum element of $l$ (with $a$ as the default value if $l$ is empty). In symbols: $$ \text{foldl}(\min, a, l) = \min(a, \text{min?}(l).\text{getD}(a)) $$ where $\text{min?}(l)$ returns the minimum element of $l$ as an $\text{Option }\alpha$ (or $\text{none}$ if $l$ is empty), and $\text{getD}$ returns the default value $a$ when $\text{min?}(l) = \text{none}$.
List.max?_nil theorem
[Max α] : ([] : List α).max? = none
Full source 
@[simp] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
Maximum of Empty List is None
Informal description
For any type $\alpha$ with a maximum operation, the maximum value of the empty list is `none`, i.e., $\text{max?}(\text{[]}) = \text{none}$.
List.max?_cons' theorem
[Max α] {xs : List α} : (x :: xs).max? = foldl max x xs
Full source 
theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = foldl max x xs := rfl
Maximum of Non-Empty List via Left Fold
Informal description
For any type $\alpha$ with a maximum operation and any non-empty list $x :: xs$ of elements of type $\alpha$, the maximum value of the list is equal to the left fold of the `max` operation over the list with initial value $x$.
List.max?_cons theorem
[Max α] [Std.Associative (max : α → α → α)] {xs : List α} : (x :: xs).max? = some (xs.max?.elim x (max x))
Full source 
@[simp] theorem max?_cons [Max α] [Std.Associative (max : α → α → α)] {xs : List α} :
    (x :: xs).max? = some (xs.max?.elim x (max x)) := by
  cases xs <;> simp [max?_cons', foldl_assoc]
Maximum of Non-Empty List via Associative Operation
Informal description
For any type $\alpha$ with an associative maximum operation $\max : \alpha \to \alpha \to \alpha$ and any non-empty list $x :: xs$ of elements of type $\alpha$, the maximum value of the list is given by $\text{some } (f(x, \text{max?}(xs)))$, where $f(a, \text{none}) = a$ and $f(a, \text{some } b) = \max(a, b)$.
List.max?_eq_none_iff theorem
{xs : List α} [Max α] : xs.max? = none ↔ xs = []
Full source 
@[simp] theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = [] := by
  cases xs <;> simp [max?]
Empty List Condition for Maximum Option: `xs.max? = none ↔ xs = []`
Informal description
For any list `xs` of elements of type `α` with a maximum operation `Max α`, the optional maximum value `xs.max?` is `none` if and only if the list `xs` is empty.
List.isSome_max?_of_mem theorem
{l : List α} [Max α] {a : α} (h : a ∈ l) : l.max?.isSome
Full source 
theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
    l.max?.isSome := by
  cases l <;> simp_all [max?_cons']
Non-emptiness of Maximum Option for List Members
Informal description
For any list `l` of elements of type `α` with a maximum operation `Max α`, and for any element `a ∈ l`, the optional value `l.max?` is non-empty (i.e., `l.max?.isSome` is true).
List.max?_mem theorem
[Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) : {xs : List α} → xs.max? = some a → a ∈ xs
Full source 
theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, maxmax a b = a ∨ max a b = b) :
    {xs : List α} → xs.max? = some a → a ∈ xs
  | nil => by simp
  | cons x xs => by
    rw [max?]; rintro ⟨⟩
    induction xs generalizing x with simp at *
    | cons y xs ih =>
      rcases ih (max x y) with h | h <;> simp [h]
      simp [← or_assoc, min_eq_or x y]
Maximum Element Belongs to List
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ such that for any $a, b \in \alpha$, either $\max(a, b) = a$ or $\max(a, b) = b$. For any list $xs$ of elements of $\alpha$, if the maximum element of $xs$ exists and is equal to $a$ (i.e., $xs.\text{max?} = \text{some } a$), then $a$ is an element of $xs$.
List.max?_le_iff theorem
[Max α] [LE α] (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) : {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
Full source 
theorem max?_le_iff [Max α] [LE α]
    (max_le_iff : ∀ a b c : α, maxmax b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
  | nil => by simp
  | cons x xs => by
    rw [max?]; rintro ⟨⟩ y
    induction xs generalizing x with
    | nil => simp
    | cons y xs ih => simp [ih, max_le_iff, and_assoc]
Characterization of Maximum Element in List via Universal Upper Bound: $a \leq x \leftrightarrow \forall b \in xs, b \leq x$
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ and a less-than-or-equal relation $\leq$, such that for all $a, b, c \in \alpha$, the equivalence $\max(b, c) \leq a \leftrightarrow b \leq a \land c \leq a$ holds. For any list $xs$ of elements of $\alpha$, if the maximum element of $xs$ exists and is equal to $a$ (i.e., $xs.\text{max?} = \text{some } a$), then for any $x \in \alpha$, we have $a \leq x$ if and only if every element $b$ in $xs$ satisfies $b \leq x$.
List.max?_eq_some_iff theorem
[Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)] (le_refl : ∀ a : α, a ≤ a) (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
Full source 
theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (max_eq_or : ∀ a b : α, maxmax a b = a ∨ max a b = b)
    (max_le_iff : ∀ a b c : α, maxmax b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
  refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
  intro ⟨h₁, h₂⟩
  cases xs with
  | nil => simp at h₁
  | cons x xs =>
    exact congrArg some <| anti.1 _ _
      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
Characterization of Maximum Element in List: Existence and Dominance
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$, a less-than-or-equal relation $\leq$, and an antisymmetric relation (where $a \leq b$ and $b \leq a$ implies $a = b$). Assume the following properties hold: 1. Reflexivity: $\forall a \in \alpha, a \leq a$. 2. Maximum property: $\forall a, b \in \alpha, \max(a, b) = a \lor \max(a, b) = b$. 3. Maximum characterization: $\forall a, b, c \in \alpha, \max(b, c) \leq a \leftrightarrow b \leq a \land c \leq a$. Then for any list $xs$ of elements of $\alpha$, the maximum element of $xs$ exists and equals $a$ (i.e., $xs.\text{max?} = \text{some } a$) if and only if $a$ is an element of $xs$ and every element $b$ in $xs$ satisfies $b \leq a$.
List.max?_replicate theorem
[Max α] {n : Nat} {a : α} (w : max a a = a) : (replicate n a).max? = if n = 0 then none else some a
Full source 
theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
    (replicate n a).max? = if n = 0 then none else some a := by
  induction n with
  | zero => rfl
  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons']
Maximum of Replicated List: $\text{max?}(\text{replicate } n a) = \text{if } n = 0 \text{ then none else some } a$
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ such that $\max(a, a) = a$ for any $a \in \alpha$. For any natural number $n$ and any element $a \in \alpha$, the maximum element of the list obtained by replicating $a$ $n$ times is: - $\text{none}$ if $n = 0$ (the list is empty) - $\text{some } a$ otherwise
List.max?_replicate_of_pos theorem
[Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : (replicate n a).max? = some a
Full source 
@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
    (replicate n a).max? = some a := by
  simp [max?_replicate, Nat.ne_of_gt h, w]
Maximum of Nonempty Replicated List: $\text{max?}(\text{replicate } n a) = \text{some } a$ for $n > 0$
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ satisfying $\max(a, a) = a$ for any $a \in \alpha$. For any positive natural number $n > 0$ and any element $a \in \alpha$, the maximum element of the list obtained by replicating $a$ $n$ times is $\text{some } a$.
List.foldl_max theorem
[Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)] {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a)
Full source 
theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
    {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
  cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]
Left Fold of Maximum Operation on Lists Equals Maximum of Initial Value and List Maximum
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max : \alpha \to \alpha \to \alpha$ that is associative and idempotent. For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the left fold of $l$ with operation $\max$ and initial value $a$ equals the maximum of $a$ and the maximum element of $l$ (with $a$ as the default value if $l$ is empty). In symbols: $$ \text{foldl}(\max, a, l) = \max(a, \text{max?}(l).\text{getD}(a)) $$
List.minimum?_nil abbrev
Full source 
@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
Minimum of Empty List is None
Informal description
For any type $\alpha$ with a minimum operation, the minimum of the empty list is `none`.
List.minimum?_cons abbrev
Full source 
@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
Minimum of Non-Empty List via Associative Operation
Informal description
For any type $\alpha$ with a minimum operation `min` that is associative, and for any non-empty list $x :: \text{xs}$ of elements of type $\alpha$, the minimum of the list is equal to the minimum of $x$ and the minimum of $\text{xs}$ (with $x$ as the default value if $\text{xs}$ is empty). In symbols: $$ \text{min?}(x :: \text{xs}) = \text{min}(x, \text{min?}(\text{xs}).\text{getOrElse}(x)) $$
List.mininmum?_eq_none_iff abbrev
Full source 
@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff
Minimum of List is None if and only if List is Empty
Informal description
For any list `xs` of elements of type `α` with a minimum operation, the minimum value of `xs` is `none` if and only if `xs` is the empty list. In other words, $\text{min?}(xs) = \text{none} \leftrightarrow xs = []$.
List.minimum?_mem abbrev
Full source 
@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem
Minimum Element of a List Belongs to the List
Informal description
For any type $\alpha$ equipped with a minimum operation $\min$ satisfying the property that for all $a, b \in \alpha$, either $\min(a, b) = a$ or $\min(a, b) = b$, and for any list $xs$ of elements of type $\alpha$, if the minimum value of $xs$ is `some a` (i.e., the list has a minimum element $a$), then $a$ is an element of $xs$.
List.le_minimum?_iff abbrev
Full source 
@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff
Characterization of List Minimum via Universal Bound
Informal description
Let $\alpha$ be a type with a minimum operation $\min$ and a relation $\leq$ such that for all $a, b, c \in \alpha$, we have $a \leq \min(b, c)$ if and only if $a \leq b$ and $a \leq c$. For any list $xs$ of elements of $\alpha$ with a minimum element $a$ (i.e., $\text{min?}(xs) = \text{some } a$), and for any $x \in \alpha$, the following are equivalent: 1. $x \leq a$ 2. For all $b \in xs$, $x \leq b$.
List.minimum?_eq_some_iff abbrev
Full source 
@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff
Characterization of Minimum Element in a List
Informal description
For a list $xs$ of elements of type $\alpha$ with a minimum operation $\min$ and a relation $\leq$, the following are equivalent: 1. The minimum of $xs$ exists and is equal to some element $a$. 2. There exists an element $a \in xs$ such that for all $b \in xs$, $a \leq b$.
List.minimum?_replicate abbrev
Full source 
@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate
Minimum of Replicated List: $\text{min?}(\text{replicate}(n, a)) = \text{if } n = 0 \text{ then none else some }a$
Informal description
For any type $\alpha$ with a minimum operation $\min$ satisfying $\min(a, a) = a$ for all $a \in \alpha$, and for any natural number $n$ and element $a \in \alpha$, the minimum element of the list consisting of $n$ copies of $a$ is $\text{some }a$ if $n > 0$, and $\text{none}$ if $n = 0$.
List.minimum?_replicate_of_pos abbrev
Full source 
@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos
Minimum of Nonempty Replicated List is Some $a$
Informal description
For any type $\alpha$ with a minimum operation $\min$ satisfying $\min(a, a) = a$ for all $a \in \alpha$, and for any positive natural number $n > 0$ and element $a \in \alpha$, the minimum element of the list consisting of $n$ copies of $a$ is $\text{some }a$.
List.maximum?_nil abbrev
Full source 
@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil
Empty List Has No Maximum
Informal description
For any type $\alpha$ equipped with a maximum operation, the maximum value of the empty list is `none`, i.e., $\text{max?}(\text{[]}) = \text{none}$.
List.maximum?_cons abbrev
Full source 
@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons
Maximum of Non-Empty List via Associative Operation
Informal description
For any type $\alpha$ with an associative maximum operation $\max : \alpha \to \alpha \to \alpha$ and any non-empty list $x :: xs$ of elements of type $\alpha$, the maximum value of the list is given by $\text{some } (f(x, \text{max?}(xs)))$, where $f(a, \text{none}) = a$ and $f(a, \text{some } b) = \max(a, b)$.
List.maximum?_eq_none_iff abbrev
Full source 
@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff
Empty List Condition for Maximum Option: $xs.\text{max?} = \text{none} \leftrightarrow xs = []$
Informal description
For any list $xs$ of elements of type $\alpha$ with a maximum operation, the optional maximum value $xs.\text{max?}$ is `none` if and only if the list $xs$ is empty.
List.maximum?_mem abbrev
Full source 
@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem
Maximum Element of List Belongs to List
Informal description
Let $\alpha$ be a type with a maximum operation $\max$ such that for any $a, b \in \alpha$, either $\max(a, b) = a$ or $\max(a, b) = b$. For any list $xs$ of elements of $\alpha$, if the maximum element of $xs$ exists and is equal to $a$ (i.e., $\text{max?}(xs) = \text{some } a$), then $a$ is an element of $xs$.
List.maximum?_le_iff abbrev
Full source 
@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff
Characterization of List Maximum via Universal Upper Bound: $a \leq x \leftrightarrow \forall b \in xs, b \leq x$
Informal description
Let $\alpha$ be a type with a maximum operation $\max$ and a less-than-or-equal relation $\leq$, such that for all $a, b, c \in \alpha$, the equivalence $\max(b, c) \leq a \leftrightarrow b \leq a \land c \leq a$ holds. For any list $xs$ of elements of $\alpha$, if the maximum element of $xs$ exists and is equal to $a$ (i.e., $xs.\text{max?} = \text{some } a$), then for any $x \in \alpha$, we have $a \leq x$ if and only if every element $b$ in $xs$ satisfies $b \leq x$.
List.maximum?_eq_some_iff abbrev
Full source 
@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff
Characterization of List Maximum: Existence and Dominance
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$, a reflexive and antisymmetric relation $\leq$, and satisfying the following properties: 1. For any $a, b \in \alpha$, either $\max(a, b) = a$ or $\max(a, b) = b$. 2. For any $a, b, c \in \alpha$, $\max(b, c) \leq a$ if and only if $b \leq a$ and $c \leq a$. Then for any list $xs$ of elements of $\alpha$ and any $a \in \alpha$, the following are equivalent: - The maximum element of $xs$ exists and equals $a$ (i.e., $\text{max?}(xs) = \text{some } a$). - The element $a$ belongs to $xs$ and is greater than or equal to every element in $xs$ (i.e., $a \in xs$ and $\forall b \in xs, b \leq a$).
List.maximum?_replicate abbrev
Full source 
@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate
Maximum of Replicated List: $\text{max?}(\text{replicate } n a) = \text{if } n = 0 \text{ then none else some } a$
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ such that $\max(a, a) = a$ for any $a \in \alpha$. For any natural number $n$ and any element $a \in \alpha$, the maximum element of the list obtained by replicating $a$ $n$ times is: - $\text{none}$ if $n = 0$ (the list is empty) - $\text{some } a$ otherwise. In other words, if $xs = \text{replicate } n a$, then $\text{max?}(xs) = \begin{cases} \text{none} & \text{if } n = 0 \\ \text{some } a & \text{otherwise} \end{cases}$.
List.maximum?_replicate_of_pos abbrev
Full source 
@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos
Maximum of Nonempty Replicated List: $\text{max?}(\text{replicate } n a) = \text{some } a$ for $n > 0$
Informal description
Let $\alpha$ be a type equipped with a maximum operation $\max$ satisfying $\max(a, a) = a$ for any $a \in \alpha$. For any positive natural number $n > 0$ and any element $a \in \alpha$, the maximum element of the list obtained by replicating $a$ $n$ times is $\text{some } a$.