WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Maximum and minimum

Revision #2329 → #2609 · back to history

modifiedFinite chains have max and min10e2d8231c55
FieldFrom #2329To #2609
mathlib.declSet.Finite.exists_max_imageSet.exists_max_image
provenanceaiai-moderated