Proposition 4.2.252733CF927914

Proof. By example 3.4.15, the function $w\mapsto \log |w|$ is subharmonic on $\mathbb C$. Hence $z\mapsto \log |z_1|$, a function of the first two real coordinates, is subharmonic on $\mathbb R^{2n}$ by lemma 4.2.7; it is finite off $H$ and equals $-\infty $ on $H$. Thus $H$ is polar, and proposition 4.2.6 shows that the classical fine topology induces the discrete topology on $H$.

Now let $x\in H$, and let $N'$ be a neighborhood of $x$ for $\tau $. As in subsection 4.2.1, upper semicontinuity turns every condition of the form $u<b$ into a Euclidean open condition, and restrictions to smaller open sets preserve the complex-line condition; hence $N'$ contains a set

where $V$ is a Euclidean open neighborhood of $x$, the $u_ i$ are upper semicontinuous functions on $V$ satisfying the complex-line condition in the statement, and $u_ i(x)>a_ i$. Choose an affine complex line $\ell \subset H$ through $x$, which is possible since $n\geq 2$, and identify $\ell $ with $\mathbb C$. On the connected component of $\ell \cap V$ containing $x$, each restriction $u_ i|_\ell $ is subharmonic and is not identically $-\infty $, because $u_ i(x)$ is finite. Hence $\{ u_ i|_\ell >a_ i\} $ is open in the planar fine topology, and the intersection of these sets with that component is a planar fine neighborhood of $x$ contained in $N\cap \ell $. By proposition 4.2.5, applied in the plane, it contains points other than $x$. These points lie in $H\cap N'$, so $x$ is not isolated in $H$. $\square$