Urysohn function from closure-nested open sets
= Urysohn function from closure-nested open sets
{c}
{title2=$f(x)=\inf\{t:x\in U_t\}$}
Let <open sets> $U_t$ be indexed by a <dense subset> of $[0,1]$, with $\overline{U_s}\subseteq U_t$ for $s<t$. Taking the infimum of membership indices, with value one outside their <union>, gives a <continuous function>. The strict sublevel <sets> are <unions> of $U_t$; strict superlevel <sets> are <unions> of <complements> of $\overline{U_t}$. These identities prove <continuity>.