[Merged by Bors] - feat(data/finset,order/conditionally_complete_lattice): lemmas about min'/max'
#8782
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.
data/finset/*
finset.nonempty.to_set
;finset.max'_lt_iff
,finset.lt_min'_iff
,finset.max'_eq_sup'
,finset.min'_eq_inf'
;finset.induction_on_max
without usingfinset.card
,move one step to
finset.lt_max'_of_mem_erase_max'
;order/conditionally_complete_lattice
Sup
/Inf
of a nonempty finite set in aconditionally complete lattice to
finset.sup'
/finset.inf'
/finset.max'
/finset.min'
;Sup
/Inf
of a nonempty finite setin a conditionally complete lattice / linear order;
order/filter/at_top_bot
filter.high_scores
.