On behavioural pseudometrics and closure ordinals

A behavioural pseudometric is often defined as the least fixed point of a monotone function F on a complete lattice of 1-bounded pseudometrics. According to Tarski?s fixed point theorem, this least fixed point can be obtained by (possibly transfinite) iteration of F, starting from the least element ⊥ of the lattice. The smallest ordinal α such that $F^{\alpha }(\perp )=F^{\alpha +1}(\perp )$ is known as the closure ordinal of F. We prove that if F is also continuous with respect to the sup-norm, then its closure ordinal is ω. We also show that our result gives rise to simpler and modular proofs that the closure ordinal is ω.