mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min'

Open adomani opened this issue 3 years ago • 2 comments

The six lemmas in this PR show that

  • finset.max and finset.max' coincide (when and how they can);
  • the finset.max' of s.erase x is not x;
  • the finset.max of s.erase x is not x;

and their @[to_dual] analogues.

Open in Gitpod

adomani avatar Aug 10 '22 14:08 adomani

You should prove the corresponding lemmas about min too.

vihdzp avatar Aug 10 '22 21:08 vihdzp

I've got this down to a single lemma that is still missing a one-line proof: any golfing suggestions? :smile:

adomani avatar Aug 12 '22 03:08 adomani

:v: adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Aug 15 '22 15:08 bors[bot]

bors r+

adomani avatar Aug 15 '22 15:08 adomani

bors r+

adomani avatar Aug 16 '22 07:08 adomani

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 16 '22 13:08 bors[bot]