Well-foundedness of product orders?

Stream: Is there code for X?

[Michael Stoll]

Do we have a version of the following?

import Mathlib.Tactic

instance {α β : Type*} [Fintype α] [Preorder β] [IsWellFounded β (· < ·)] :
    IsWellFounded (α → β) (· < ·) := sorry

(In fact, this should hold more generally:

instance {α : Type*} {β : α → Type*} [Fintype α] [∀ a, Preorder (β a)] [∀ a, IsWellFounded (β a) (· < ·)] :
    IsWellFounded ((a : α) → β a) (· < ·) := sorry

)

[Anatole Dedecker]

docs#Pi.wellFoundedLT ?

[Anatole Dedecker]

It's in a weird file though

[Anatole Dedecker]

Oh nevermind, it actually does use DFinsupp in the proof :mind_blown:

[Michael Stoll]

So I was missing this non-obvious import...

[Alex J. Best]

Michael Stoll said:

So I was missing this non-obvious import...

It's actually not so bad these days to develop using import Mathlib or to have a scratch file with that in for the purposes of #synth or apply? queries

[Scott Morrison]

I've been caught by this exact same non-obvious import.

[Scott Morrison]

I think we should move this result to its own better-named file!

[Michael Stoll]

Alex J. Best said:

Michael Stoll said:

So I was missing this non-obvious import...

It's actually not so bad these days to develop using import Mathlib or to have a scratch file with that in for the purposes of #synth or apply? queries

True, but it takes a while to get used to that.