In "A domain theoretic account of Picard's theorem" (<http://www.doc.ic.ac.uk/~dirk/Publications/icalp2004.pdf>), the authors assert the following.


Let $\mathbb{IR}$ be the interval domain $\lbrace [a^-,a⁺] | a^- \leq a^+, a^-, a^+ \in \mathbb{R} \rbrace \cup \lbrace \mathbb{R} \rbrace$.


Suppose $f = [f^-,f^+] : [-a,a] \rightarrow \mathbb{IR}$ is Scott continuous. Then $f^-$ and $f^+$ are measurable.


Their proof consists in asserting that $f⁻$ and $f⁺$ are lower (resp. upper) semi-continuous, which I have tried without success to establish. Can anyone help with either an explanation or a reference that proves it?



If $f : [-a,a] \rightarrow \mathbb{IR}$ is Scott continuous, why are $f^-$ and $f^+$ measurable?
First, we note that $\mathbb{IR}$ is ordered by $[a,b] \sqsubseteq [c,d]$ iff $[c,d] \subseteq [a,b]$, which makes $\mathbb{IR}$ into a domain. Now suppose $f: [-a,a]\to \mathbb{IR}$ is Scott-continuous (that is, $f$ preserves all directed suprema).


We want to prove that $f^-$ as defined in the comment above is lower semi-continuous. Let $(x\_n)$ be an increasing sequence in $[-a, a]$. So $(x\_n) \to s$ where $s = \sup\{x\_n:n\in\mathbb{N}\} \in [-a, a]$. We want to show that $\lim\_{n\to\infty} f^-(x\_n) = f^-(s)$.


The set $$D:=\{x\_n: n\in \mathbb{N}\}$$ is a directed subset of the domain $[-a,a]$ (with the ordering inherited from $\mathbb{R}$), and we have $s=\bigsqcup D$.


For $n\in \mathbb{N}$ we have $f(x\_n)\supseteq f(x\_{n+1})$ since $f$ is order-preserving (which is implied by $f$ being Scott-continuous). The fact that $f$ is Scott-continuous means that $$[f^-(s), f^+(s)] = f(s)=f(\bigsqcup D) = \bigsqcup f(D) = \bigcap 
\{ [f^-(x\_n), f^+(x\_n)]:n\in\mathbb{N}\}.$$


So $(f^-(x\_n))\_{n\in\mathbb{N}}$ is an increasing sequence in $\mathbb{R}$ and it is bounded by $f^+(x\_1)$, so it converges. The equations above imply that $\lim\_{n\to\infty} f^-(x\_n) = f^-(s)$, so $f^-: [-a,a]\to \mathbb{R}$ is lower semi-continuous. A similar argument shows that $f^+$ is upper semi-continuous.


