[Merged by Bors] - feat: add lemmas about List.Sorted
#2311
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
List.Sorted.le_of_lt
andList.Sorted.lt_of_le
(new).List.Sorted.rel_get_of_lt
andList.Sorted.rel_get_of_le
(get
versions ofnthLe
lemmas).List.sorted_ofFn_iff
,List.sorted_lt_ofFn_iff
, andList.sorted_le_ofFn_iff
(new).List.monotone_iff_ofFn_sorted
in favor ofList.sorted_le_ofFn_iff
.List.Monotone.ofFn_sorted
toMonotone.ofFn_sorted
. In Lean 3, dot notationhf.of_fn_sorted
usedlift.monotone.of_fn_sorted
if thelist
namespace is open. This is no longer the case in Lean 4.