psigma.lex_wf

Stream: mathlib4

[Yaël Dillies]

Does anybody know where docs3#psigma.lex_wf is gone? It doesn't seem to be aligned anywhere and Init.WF (where I would expect the lemma to live) contains a bunch of lemmas that are misnamed, suggesting that maybe the lemma is somewhere but under an obscure name.

[Yaël Dillies]

My other thought for what might have happened is that lemmas of the form WellFounded (r : α → α → Prop) → WellFounded (s : β → β → Prop) got turned into a WellFoundedRelation α → WellFoundedRelation β instance. In that case, docs#PSigma.instWellFoundedRelationPSigma is the instance corresponding to psigma.lex_wf.

[Eric Wieser]

I would guess that init.data.sigma.lex has not been ported

[Yaël Dillies]

So much for the port being over :upside_down:

[Eric Wieser]

mathport has a copy here

[Eric Wieser]

Since the main page of the dashboard is now useless anyway, I'm going to merge https://github.com/leanprover-community/mathlib-port-status/pull/21

[Eric Wieser]

Bye-bye, "goals accomplished :tada:"

[Yaël Dillies]

Hmm, how do you actually see the file on Github? I only see this
image.png

[Eric Wieser]

Whoops, I sent an edit link; fixed

[Eric Wieser]

init.data.sigma.lex is now on the #port-dashboard