Kim Morrison d3781bb787 fix: definition of Min (Option α), and basic lemmas (#7255) ... This PR fixes the definition of `Min (Option α)`. This is a breaking change. This treats `none` as the least element, so `min none x = min x none = none` for all `x : Option α`. Prior to nightly-2025-02-27, we instead had `min none (some x) = min (some x) none = some x`. Also adds basic lemmas relating `min`, `max`, `≤` and `<` on `Option`.		2025-02-27 10:44:44 +00:00
..
Attach.lean	chore: cleanup duplicate theorems (#7113)	2025-02-18 01:46:12 +00:00
Basic.lean	fix: definition of Min (Option α), and basic lemmas (#7255)	2025-02-27 10:44:44 +00:00
BasicAux.lean	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
Instances.lean	feat: lemmas about for loops over Option (#6316)	2024-12-05 05:09:07 +00:00
Lemmas.lean	fix: definition of Min (Option α), and basic lemmas (#7255)	2025-02-27 10:44:44 +00:00
List.lean	feat: tree map data structures and operations (#6914)	2025-02-11 14:47:47 +00:00
Monadic.lean	feat: lemmas about lexicographic order on Array and Vector (#6399)	2024-12-19 10:36:50 +00:00