Commit 2023-08-03 16:32 1f78f7fc
View on Github →feat: Finite maximality/minimality (#6337)
This PR slightly tidies the proof of Set.Finite.exists_maximal_wrt, and adds a minimality version.
It also adds primed versions of both that alter the finiteness hypothesis to a weaker hypothesis where only the image is finite.