Lower semicontinuous submeasure is countably subadditive A submeasure is a function $\phi\colon\mathcal P(\mathbb N)\to[0,+\infty]$ that is monotone and subadditive. If, additionally,
$$\phi(A) = \lim\limits_{n\to\infty} \phi(A\cap[1,n])$$
then it is called lower semicontinuous.
I will refer to my other post for a detailed definition and also for explanation how this related to lower semicontinuuity of the function $\phi$ if we view it as a function on $\{0,1\}^{\mathbb N}$ with the product topology: Lower-semicontinuous submeasure on $\mathbb N$ vs. function on Cantor space.
I have noticed that such submeasures are in fact countably subadditive, i.e., for any sets $A_i\subseteq\mathbb N$, $i=1,2,\dots$, we have
$$\phi\left(\bigcup_{i=1}^\infty A_i\right) \le \sum_{i=1}^\infty \phi(A_i).$$
I will post my attempt to show this in an answer. I'll be grateful for any comments or alternative approaches.
One of the reasons I'm asking this question is that in sources about this topic that I have seen, this property was not mentioned. (Although it seems that it is used implicitly in a few places.) One possibility is that the authors consider the result too simple to spend time with additional explanation. But it is also possible that I have overlooked something.
 A: Here is my attempt to prove the claim in the title.

Proof 1. Let $$A=\bigcup\limits_{i=1}^\infty A_i.$$
Fix some $n\in\mathbb N$. Then we clearly have
$$A\cap [1,n] = \bigcup\limits_{i=1}^\infty (A_i\cap [1,n]).$$
However, since $A\cap [1,n]$ is finite, there is a finite set $F$ such that
$$A\cap [1,n] = \bigcup\limits_{i\in F} (A_i\cap [1,n]).$$
Using finite subadditivity we get
$$\phi(A\cap [1,n]) \le \sum\limits_{i\in F} \phi(A_i) \le \sum_{i=1}^\infty \phi(A_i).$$
Since $\phi$ is lower semicontinuous, we also get
$$\phi(A) = \lim\limits_{n\to\infty} \phi (A\cap[1,n]) \le \sum_{i=1}^\infty \phi(A_i).$$

We can also use the fact that $\phi$ is lower semicontinuous are a function on the Cantor cube $\{0,1\}^n$.
For lower semicontinuous functions we have
$$f(p) \le \liminf\limits_{x\to p} f(x)$$
Proof 2. Let
\begin{align*}
B_n&=\bigcup\limits_{i=1}^n A_i\\
A&=\bigcup\limits_{i=1}^\infty A_i
\end{align*}
Notice that in the product topology we have $\lim\limits_{n\to\infty} B_n = A$. (It is an increasing sequence of sets.)
From lower semicontinuity we get
$$\phi(A) \le \liminf_{n\to\infty} \phi(B).$$
At the same time we have
$$\phi(B) \le \sum_{i=1}^n \phi(A_i)$$
which together gives
$$\phi(A) \le \liminf_{n\to\infty} \phi(A_i) = \sum_{i=1}^\infty \phi(A_i).$$
