Documentation

Mathlib.Data.List.MinMax

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 []

def List.argAux {α : Type u_1} (r : ααProp) [DecidableRel r] (a : Option α) (b : α) :

Auxiliary definition for argmax and argmin.

Equations
Instances For
    @[simp]
    theorem List.foldl_argAux_eq_none {α : Type u_1} (r : ααProp) [DecidableRel r] {l : List α} {o : Option α} :
    List.foldl (List.argAux r) o l = none l = [] o = none
    @[simp]
    theorem List.argAux_self {α : Type u_1} (r : ααProp) [DecidableRel r] (hr₀ : Irreflexive r) (a : α) :
    theorem List.not_of_mem_foldl_argAux {α : Type u_1} (r : ααProp) [DecidableRel r] {l : List α} (hr₀ : Irreflexive r) (hr₁ : Transitive r) {a : α} {m : α} {o : Option α} :
    a lm List.foldl (List.argAux r) o l¬r a m
    def List.argmax {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) (l : List α) :

    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.

    Equations
    Instances For
      def List.argmin {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) (l : List α) :

      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.

      Equations
      Instances For
        @[simp]
        theorem List.argmax_nil {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) :
        List.argmax f [] = none
        @[simp]
        theorem List.argmin_nil {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) :
        List.argmin f [] = none
        @[simp]
        theorem List.argmax_singleton {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {a : α} :
        @[simp]
        theorem List.argmin_singleton {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {a : α} :
        theorem List.not_lt_of_mem_argmax {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} {a : α} {m : α} :
        a lm List.argmax f l¬f m < f a
        theorem List.not_lt_of_mem_argmin {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} {a : α} {m : α} :
        a lm List.argmin f l¬f a < f m
        theorem List.argmax_concat {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) (a : α) (l : List α) :
        List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun (c : α) => if f c < f a then some a else some c
        theorem List.argmin_concat {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : αβ) (a : α) (l : List α) :
        List.argmin f (l ++ [a]) = Option.casesOn (List.argmin f l) (some a) fun (c : α) => if f a < f c then some a else some c
        theorem List.argmax_mem {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} {m : α} :
        m List.argmax f lm l
        theorem List.argmin_mem {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} {m : α} :
        m List.argmin f lm l
        @[simp]
        theorem List.argmax_eq_none {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} :
        List.argmax f l = none l = []
        @[simp]
        theorem List.argmin_eq_none {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] {f : αβ} {l : List α} :
        List.argmin f l = none l = []
        theorem List.le_of_mem_argmax {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {a : α} {m : α} :
        a lm List.argmax f lf a f m
        theorem List.le_of_mem_argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {a : α} {m : α} :
        a lm List.argmin f lf m f a
        theorem List.argmax_cons {α : Type u_1} {β : Type u_2} [LinearOrder β] (f : αβ) (a : α) (l : List α) :
        List.argmax f (a :: l) = Option.casesOn (List.argmax f l) (some a) fun (c : α) => if f a < f c then some c else some a
        theorem List.argmin_cons {α : Type u_1} {β : Type u_2} [LinearOrder β] (f : αβ) (a : α) (l : List α) :
        List.argmin f (a :: l) = Option.casesOn (List.argmin f l) (some a) fun (c : α) => if f c < f a then some c else some a
        theorem List.index_of_argmax {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} [DecidableEq α] {l : List α} {m : α} :
        m List.argmax f l∀ {a : α}, a lf m f aList.indexOf m l List.indexOf a l
        theorem List.index_of_argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} [DecidableEq α] {l : List α} {m : α} :
        m List.argmin f l∀ {a : α}, a lf a f mList.indexOf m l List.indexOf a l
        theorem List.mem_argmax_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {m : α} [DecidableEq α] :
        m List.argmax f l m l (∀ (a : α), a lf a f m) ∀ (a : α), a lf m f aList.indexOf m l List.indexOf a l
        theorem List.argmax_eq_some_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {m : α} [DecidableEq α] :
        List.argmax f l = some m m l (∀ (a : α), a lf a f m) ∀ (a : α), a lf m f aList.indexOf m l List.indexOf a l
        theorem List.mem_argmin_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {m : α} [DecidableEq α] :
        m List.argmin f l m l (∀ (a : α), a lf m f a) ∀ (a : α), a lf a f mList.indexOf m l List.indexOf a l
        theorem List.argmin_eq_some_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : αβ} {l : List α} {m : α} [DecidableEq α] :
        List.argmin f l = some m m l (∀ (a : α), a lf m f a) ∀ (a : α), a lf a f mList.indexOf m l List.indexOf a l
        def List.maximum {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (l : List α) :

        maximum l returns a WithBot α, the largest element of l for nonempty lists, and for []

        Equations
        Instances For
          def List.minimum {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (l : List α) :

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

          Equations
          Instances For
            @[simp]
            theorem List.maximum_nil {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
            [].maximum =
            @[simp]
            theorem List.minimum_nil {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
            [].minimum =
            @[simp]
            theorem List.maximum_singleton {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (a : α) :
            [a].maximum = a
            @[simp]
            theorem List.minimum_singleton {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (a : α) :
            [a].minimum = a
            theorem List.maximum_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {m : α} :
            l.maximum = mm l
            theorem List.minimum_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {m : α} :
            l.minimum = mm l
            @[simp]
            theorem List.maximum_eq_bot {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} :
            l.maximum = l = []
            @[simp, deprecated List.maximum_eq_bot]
            theorem List.maximum_eq_none {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} :
            l.maximum = none l = []
            @[simp]
            theorem List.minimum_eq_top {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} :
            l.minimum = l = []
            @[simp, deprecated List.minimum_eq_top]
            theorem List.minimum_eq_none {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} :
            l.minimum = none l = []
            theorem List.not_lt_maximum_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {a : α} {m : α} :
            a ll.maximum = m¬m < a
            theorem List.minimum_not_lt_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {a : α} {m : α} :
            a ll.minimum = m¬a < m
            theorem List.not_lt_maximum_of_mem' {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {a : α} (ha : a l) :
            ¬l.maximum < a
            theorem List.not_lt_minimum_of_mem' {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {l : List α} {a : α} (ha : a l) :
            ¬a < l.minimum
            theorem List.maximum_concat {α : Type u_1} [LinearOrder α] (a : α) (l : List α) :
            (l ++ [a]).maximum = max l.maximum a
            theorem List.le_maximum_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} {m : α} :
            a ll.maximum = ma m
            theorem List.minimum_le_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} {m : α} :
            a ll.minimum = mm a
            theorem List.le_maximum_of_mem' {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (ha : a l) :
            a l.maximum
            theorem List.minimum_le_of_mem' {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (ha : a l) :
            l.minimum a
            theorem List.minimum_concat {α : Type u_1} [LinearOrder α] (a : α) (l : List α) :
            (l ++ [a]).minimum = min l.minimum a
            theorem List.maximum_cons {α : Type u_1} [LinearOrder α] (a : α) (l : List α) :
            (a :: l).maximum = max (↑a) l.maximum
            theorem List.minimum_cons {α : Type u_1} [LinearOrder α] (a : α) (l : List α) :
            (a :: l).minimum = min (↑a) l.minimum
            theorem List.maximum_le_of_forall_le {α : Type u_1} [LinearOrder α] {l : List α} {b : WithBot α} (h : ∀ (a : α), a la b) :
            l.maximum b
            theorem List.le_minimum_of_forall_le {α : Type u_1} [LinearOrder α] {l : List α} {b : WithTop α} (h : ∀ (a : α), a lb a) :
            b l.minimum
            theorem List.maximum_eq_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {m : α} :
            l.maximum = m m l ∀ (a : α), a la m
            theorem List.minimum_eq_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {m : α} :
            l.minimum = m m l ∀ (a : α), a lm a
            theorem List.coe_le_maximum_iff {α : Type u_1} [LinearOrder α] {l : List α} {a : α} :
            a l.maximum ∃ (b : α), b l a b
            theorem List.minimum_le_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {a : α} :
            l.minimum a ∃ (b : α), b l b a
            theorem List.maximum_ne_bot_of_ne_nil {α : Type u_1} [LinearOrder α] {l : List α} (h : l []) :
            l.maximum
            theorem List.minimum_ne_top_of_ne_nil {α : Type u_1} [LinearOrder α] {l : List α} (h : l []) :
            l.minimum
            theorem List.maximum_ne_bot_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
            l.maximum
            theorem List.minimum_ne_top_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
            l.minimum
            def List.maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
            α

            The maximum value in a non-empty List.

            Equations
            Instances For
              def List.minimum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
              α

              The minimum value in a non-empty List.

              Equations
              Instances For
                @[simp]
                theorem List.coe_maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
                (List.maximum_of_length_pos h) = l.maximum
                @[simp]
                theorem List.coe_minimum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
                (List.minimum_of_length_pos h) = l.minimum
                @[simp]
                theorem List.le_maximum_of_length_pos_iff {α : Type u_1} [LinearOrder α] {l : List α} {b : α} (h : 0 < l.length) :
                @[simp]
                theorem List.minimum_of_length_pos_le_iff {α : Type u_1} [LinearOrder α] {l : List α} {b : α} (h : 0 < l.length) :
                theorem List.maximum_of_length_pos_mem {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
                theorem List.minimum_of_length_pos_mem {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) :
                theorem List.le_maximum_of_length_pos_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (h : a l) (w : 0 < l.length) :
                theorem List.minimum_of_length_pos_le_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (h : a l) (w : 0 < l.length) :
                theorem List.getElem_le_maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} {i : } (w : i < l.length) (h : optParam (0 < l.length) ) :
                theorem List.minimum_of_length_pos_le_getElem {α : Type u_1} [LinearOrder α] {l : List α} {i : } (w : i < l.length) (h : optParam (0 < l.length) ) :
                theorem List.getD_max?_eq_unbot'_maximum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) :
                l.max?.getD d = WithBot.unbot' d l.maximum
                @[deprecated List.getD_max?_eq_unbot'_maximum]
                theorem List.getD_maximum?_eq_unbot'_maximum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) :
                l.max?.getD d = WithBot.unbot' d l.maximum

                Alias of List.getD_max?_eq_unbot'_maximum.

                theorem List.getD_min?_eq_untop'_minimum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) :
                l.min?.getD d = WithTop.untop' d l.minimum
                @[deprecated List.getD_min?_eq_untop'_minimum]
                theorem List.getD_minimum?_eq_untop'_minimum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) :
                l.min?.getD d = WithTop.untop' d l.minimum

                Alias of List.getD_min?_eq_untop'_minimum.

                @[simp]
                theorem List.foldr_max_of_ne_nil {α : Type u_1} [LinearOrder α] [OrderBot α] {l : List α} (h : l []) :
                (List.foldr max l) = l.maximum
                theorem List.max_le_of_forall_le {α : Type u_1} [LinearOrder α] [OrderBot α] (l : List α) (a : α) (h : ∀ (x : α), x lx a) :
                theorem List.le_max_of_le {α : Type u_1} [LinearOrder α] [OrderBot α] {l : List α} {a : α} {x : α} (hx : x l) (h : a x) :
                @[simp]
                theorem List.foldr_min_of_ne_nil {α : Type u_1} [LinearOrder α] [OrderTop α] {l : List α} (h : l []) :
                (List.foldr min l) = l.minimum
                theorem List.le_min_of_forall_le {α : Type u_1} [LinearOrder α] [OrderTop α] (l : List α) (a : α) (h : ∀ (x : α), x la x) :
                theorem List.min_le_of_le {α : Type u_1} [LinearOrder α] [OrderTop α] (l : List α) (a : α) {x : α} (hx : x l) (h : x a) :