Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-05 06:11 901bdbf4

View on Github →

feat(data/list/min_max): minimum and maximum over list (#884)

  • feat(data/list/min_max): minimum and maximum over list
  • Update min_max.lean
  • replace semicolons

Estimated changes

added theorem list.le_maximum_of_mem
added theorem list.le_of_foldl_max
added theorem list.le_of_foldr_max
added def list.maximum
added def list.maximum_aux
added theorem list.mem_foldl_max
added theorem list.mem_foldr_max
added theorem list.mem_maximum
added theorem list.mem_maximum_aux