Commit 2023-01-05 18:26 5ab0ee8e

View on Github →

feat port: Data.List.MinMax (#1352)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/MinMax.lean

added def List.argAux

added theorem List.arg_aux_self

added def List.argmax

added theorem List.argmax_concat

added theorem List.argmax_cons

added theorem List.argmax_eq_none

added theorem List.argmax_eq_some_iff

added theorem List.argmax_mem

added theorem List.argmax_nil

added theorem List.argmax_singleton

added def List.argmin

added theorem List.argmin_concat

added theorem List.argmin_cons

added theorem List.argmin_eq_none

added theorem List.argmin_eq_some_iff

added theorem List.argmin_mem

added theorem List.argmin_nil

added theorem List.argmin_singleton

added theorem List.foldl_argAux_eq_none

added theorem List.foldr_max_of_ne_nil

added theorem List.foldr_min_of_ne_nil

added theorem List.index_of_argmax

added theorem List.index_of_argmin

added theorem List.le_max_of_le

added theorem List.le_maximum_of_mem'

added theorem List.le_maximum_of_mem

added theorem List.le_min_of_forall_le

added theorem List.le_minimum_of_mem'

added theorem List.le_of_mem_argmax

added theorem List.le_of_mem_argmin

added theorem List.max_le_of_forall_le

added def List.maximum

added theorem List.maximum_concat

added theorem List.maximum_cons

added theorem List.maximum_eq_coe_iff

added theorem List.maximum_eq_none

added theorem List.maximum_mem

added theorem List.maximum_nil

added theorem List.maximum_singleton

added theorem List.mem_argmax_iff

added theorem List.mem_argmin_iff

added theorem List.min_le_of_le

added def List.minimum

added theorem List.minimum_concat

added theorem List.minimum_cons

added theorem List.minimum_eq_coe_iff

added theorem List.minimum_eq_none

added theorem List.minimum_le_of_mem

added theorem List.minimum_mem

added theorem List.minimum_nil

added theorem List.minimum_not_lt_of_mem

added theorem List.minimum_singleton

added theorem List.not_lt_maximum_of_mem'

added theorem List.not_lt_maximum_of_mem

added theorem List.not_lt_minimum_of_mem'

added theorem List.not_lt_of_mem_argmax

added theorem List.not_lt_of_mem_argmin

added theorem List.not_of_mem_foldl_argAux