$E_1\subset E_2\subset...$ are subsets of $\mathbb{R}$
The limit is defined iff lim sup$E_n$ = lim inf$E_n$.
Here is what I did to prove the double inclusion of the two lim sup and inf:
- $\liminf\subset\limsup$ (always true):
Let $x$ be in $\liminf E_n$
$x$ belongs to all $E_n$ except for at most a finite number of them. But $\mathbb{N}\backslash\{i_1,...,i_k\}$ is infinite for a finite $k$ so $x$ belongs to an infinite number of $E_n$ which is an alternative/"intuitive" definition of $\limsup$.
- $\limsup\subset\liminf$ (in this particular case):
Let $x$ be in $\limsup E_n$
If $x\notin\bigcup\limits_{n=1}^{\infty}\bigcap\limits_{m\geq n}E_m$ then $\ x\notin\bigcap\limits_{m\geq n}E_m\ \forall n\geq1$ but $\bigcap\limits_{m\geq n}E_m=E_n$ because of how $E_n\subset E_{n+1}\ \forall n$ So $x\notin E_n\ \forall n\in\mathbb{N}\implies x\in\emptyset$
Now I want to prove that mes(lim $E_n$) = lim mes($E_n$) where mes(.) is the measure defined on subsets of $\mathbb{R}$ as $\inf \{\sum\limits_{n=1}^{\infty}(b_n-a_n)\ :\ E\subset\bigcup\limits_{n=1}^{\infty}(a_n,b_n)\}$but I'm not sure how...
For pairwise disjunct measurable sets $A_n$ you know that $\rm{mes} (\cup_{m=1}^\infty A_m) = \sum_{m=1}^\infty \rm{mes}(A_m)$ by definition of a measure. An alternative discription of this property is that for any sequence $(E_n)_{n \in \mathbb{N}} \subset \mathcal{A}$ of measurable sets with $E_n \uparrow$, i.e. $E_n \subset E_{n+1}$, one has $\rm{mes}(\cup_{m=1}^\infty E_m) =\lim_{m \rightarrow \infty} \rm{mes}(E_m)$.
The proof can be found in any book on measure theory: Define inductively $A_1 = E_1$ and $A_n = E_n \setminus A_{n-1}$. Then $(A_n)_{n \mathbb{N}}$ are pairwise disjunct, $E_n = \cup_{m=1}^n A_m$, $\cup_{n=1}^\infty E_n = \cup_{m=1}^\infty A_m$, and thus $$ \rm{mes}(\cup_{m=1}^\infty E_m) = \rm{mes}(\cup_{m=1}^\infty A_m) = \sum_{m=1}^\infty \rm{mes}(A_m) = \lim_{n \rightarrow \infty} \sum_{m=1}^n \rm{mes}(A_m) = \lim_{n \rightarrow \infty} \rm{mes}(E_n).$$