Partial order on `FunLike`

Stream: maths

[Yury G. Kudryashov]

What do you think about introducing a generic [FunLike F α β] [∀ a, PartialOrder (β a)] : PartialOrder F instance with f ≤ g defined as ∀ x, f x ≤ g x?

[Yury G. Kudryashov]

(more precisely, we'll need LE/Preorder/PartialOrder)

[Yury G. Kudryashov]

Is there a FunLike with a different order?

[Yaël Dillies]

I don't know of any other order, no.

[Eric Wieser]

Is Lex F (where F is FunLike) Funlike?

[Yaël Dillies]

Not yet, but it could be made to be

[Antoine Chambert-Loir]

Yaël Dillies said:

I don't know of any other order, no.

If alpha is Fin n, or the like, then there is also the lexicographic order with all its variants.

[Anatole Dedecker]

I don't know any case where that would cause a diamond in current mathlib, but instinctively that sounds like a bad idea :sweat_smile: