Scott Domains

Stream: Is there code for X?

[jthulhu]

I have searched mathlib for Scott domains, but I have not found any relevant definition. More specifically, I am looking for fixpoint theorems, ie. theorems that state that, for instance, there exists a domain D such that

$$D = D + [D → D] + 1$$

where + is the reduced sum, and [D → D] is the domain of continuous maps from D to itself.

[Shreyas Srinivas]

There is something called docs#ScottContinuous