Tarski Fixed Point Theorem

Stream: Is there code for X?

[Graham Leach-Krouse]

Is there a proof available of the Knaster-Tarski theorem, or anything similar?

[Anatole Dedecker]

Yes we do, see docs#OrderHom.lfp (yes, the name is hard to guess) and the whole Mathlib.Order.FixedPoints file

[Anatole Dedecker]

Ah, more precisely the result is docs#fixedPoints.completeLattice

[Anatole Dedecker]

Wow that is a very old file. I haven't seen a lot of non-core file dating back to 2017!

[Graham Leach-Krouse]

Thank you!

[Kevin Buzzard]

Johannes was a master of complete lattices back in the day :-) The other things which existed were stuff like Data.Finset.Basic (basically written by Mario I think, and I think it was already 2000 lines even then).

[Anatole Dedecker]

Ah yes of course, I meant outside of Data

[Anatole Dedecker]

To be fair this is a pretty important result "morally", because IIRC this is basically the foundation for modeling inductive types in set theory. But of course we already have inductive types, so it turns out we don't need it that often (the only file importing that one is Mathlib.SetTheory.Cardinal.SchroederBernstein)

[Anatole Dedecker]

Well actually it would correspond to inductively defined sets/predicates, but you get the point.