Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-23 15:22 cff886bb

View on Github →

feat(data/finset): max and min

Estimated changes

Modified data/finset.lean

added theorem finset.le_max_of_mem

added theorem finset.le_min_of_mem

added theorem finset.max_empty

added theorem finset.max_insert

added theorem finset.max_of_mem

added theorem finset.max_singleton

added theorem finset.mem_of_max

added theorem finset.mem_of_min

added theorem finset.min_empty

added theorem finset.min_insert

added theorem finset.min_of_mem

added theorem finset.min_singleton

Modified data/option.lean

added theorem option.lift_or_get_choice

deleted theorem option.lift_or_get_is_some_left

deleted theorem option.lift_or_get_is_some_right

Modified logic/basic.lean

added theorem if_choice

added theorem max_choice

added theorem min_choice

Modified order/lattice.lean