Minimal/IsLeast

Stream: mathlib4

[Violeta Hernández]

How come docs#Minimal uses α → Prop while docs#IsLeast uses Set α?

[Violeta Hernández]

(And on that note, how come docs#Minimal.IsLeast for linear orders doesn't exist?)

[Bhavik Mehta]

Violeta Hernández said:

How come docs#Minimal uses α → Prop while docs#IsLeast uses Set α?

One answer is historical accident, but I think currently Minimal is used more for values which are minimal with respect to a predicate, whereas IsLeast is used more for sets.

[Bhavik Mehta]

Violeta Hernández said:

(And on that note, how come docs#Minimal.IsLeast for linear orders doesn't exist?)

That's just a missing lemma, if you want to add it (and the dual), I'd be happy to merge