Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-19 19:01 9eefd40e

View on Github →

refactor(data/list/min_max): use with_top for maximum and define argmax (#1320)

  • refactor(data/list/min_max): use option for maximum and define argmax
  • prove minimum_singleton
  • fix build
  • use with_bot for maximum
  • update comments

Estimated changes

added def list.argmax
added theorem list.argmax_concat
added theorem list.argmax_cons
added theorem list.argmax_eq_none
added theorem list.argmax_mem
added theorem list.argmax_nil
added theorem list.argmax_singleton
added theorem list.argmax_two_self
added def list.argmax₂
added def list.argmin
added theorem list.argmin_concat
added theorem list.argmin_cons
added theorem list.argmin_eq_none
added theorem list.argmin_le_of_mem
added theorem list.argmin_mem
added theorem list.argmin_nil
added theorem list.argmin_singleton
added theorem list.index_of_argmax
added theorem list.index_of_argmin
added theorem list.le_argmax_of_mem
modified theorem list.le_maximum_of_mem
deleted theorem list.le_minimum_of_mem
deleted theorem list.le_of_foldl_max
deleted theorem list.le_of_foldl_min
deleted theorem list.le_of_foldr_max
deleted theorem list.le_of_foldr_min
modified def list.maximum
deleted def list.maximum_aux
added theorem list.maximum_concat
added theorem list.maximum_cons
deleted def list.maximum_cons
added theorem list.maximum_eq_none
modified 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
deleted theorem list.mem_foldl_max
deleted theorem list.mem_foldl_min
deleted theorem list.mem_foldr_max
deleted theorem list.mem_foldr_min
deleted theorem list.mem_maximum_aux
deleted theorem list.mem_minimum_aux
modified def list.minimum
deleted def list.minimum_aux
added theorem list.minimum_concat
added theorem list.minimum_cons
deleted def list.minimum_cons
added theorem list.minimum_eq_none
added theorem list.minimum_le_of_mem
modified theorem list.minimum_mem
added theorem list.minimum_nil
added theorem list.minimum_singleton