WellFoundedLT for Fintype?

Stream: Is there code for X?

[Scott Morrison]

Do we have either of:

example [Fintype α] [Preorder α] : WellFoundedLT α := sorry
example [Fintype α] [PartialOrder α] : Nonempty (α ↪o Fin (Fintype.card α)) := sorry

available?

[Damiano Testa]

docs#instInhabitedLinearExtension seems to come close...

[Kyle Miller]

Great, then docs#monoEquivOfFin should give the rest

[Scott Morrison]

Nice, thanks!

[Kyle Miller]

Oh, one other ingredient would be the order embedding from a partial order to its linear extension, which is essentially docs#toLinearExtension

[Scott Morrison]

I guess I don't immediately need these, just noticed they were missing amongst the basic instances for WellFoundedLT. I'll star these messages and try to put together the pieces ... someday!

[Scott Morrison]

Amazingly it seems the Prod instance for WellFoundedLT was missing: #5899. (We already had the Pi instance, but somewhat obscurely in Mathlib.Data.DFinsupp.WellFounded.)

[Scott Morrison]

Perhaps this is already somewhere as a theorem rather than an instance, but I did try exact?.

[Damiano Testa]

Some of these results were useful when Lex orders were being developed. It might be worth scanning some <prefix>.Lex files, maybe...

[Yaël Dillies]

Yes we have your theorem, Scott, but it's stated using Finite

[Yaël Dillies]

Also it will talk about WellFounded, not WellFoundedLT.

[Yaël Dillies]

Oh in fact we have both. finite.preorder.well_founded_lt