Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-18 14:08 2c2d515a

View on Github →

refactor(data/list/min_max): Generalise list.argmin/list.argmax to preorders (#13221) This PR generalises the contents of the data/list/min_max file from a linear_order down to a preorder with decidable <. Note that for this to work out, I have had to change the structure of the auxiliary function argmax₂ to now mean option.cases_on a (some b) (λ c, if f c < f b then some b else some c). This is because in the case of a preorder, argmax₂ would perform the swap in the absence of the ≤ relation, which would result in a semi-random shuffle that doesn't look very maximal.

Estimated changes

added def list.arg_aux
added theorem list.arg_aux_self
modified def list.argmax
modified theorem list.argmax_eq_none
modified theorem list.argmax_eq_some_iff
modified theorem list.argmax_mem
modified theorem list.argmax_singleton
deleted theorem list.argmax_two_self
deleted def list.argmax₂
modified def list.argmin
modified theorem list.argmin_eq_none
modified theorem list.argmin_eq_some_iff
deleted theorem list.argmin_le_of_mem
modified theorem list.argmin_mem
modified theorem list.index_of_argmax
modified theorem list.index_of_argmin
deleted theorem list.le_argmax_of_mem
modified theorem list.le_maximum_of_mem'
modified theorem list.le_maximum_of_mem
deleted theorem list.le_min_of_le_forall
modified theorem list.le_minimum_of_mem'
added theorem list.le_of_mem_argmax
added theorem list.le_of_mem_argmin
modified theorem list.max_le_of_forall_le
modified theorem list.maximum_eq_coe_iff
modified theorem list.mem_argmax_iff
modified theorem list.mem_argmin_iff
modified theorem list.minimum_eq_coe_iff
modified theorem list.minimum_le_of_mem