Let $I \subset \mathbb{R}$ be some fixed interval and $\left(f_m\right)_{m=1}^\infty$ be a sequence of non-negative functions defined on $I$. Define the sets $A^k_n = \{x \in I:\inf_{m\geq n}f_m(x) \geq 1/k\}$ and $A^k = \{x \in I:\lim\inf_{m\to \infty}f_m(x) \geq 1/k\}$ for $k \in \mathbb{N}$. I am trying to show rigorously that $\bigcup_{m=1}^\infty A_n^k = A^k$. I have already shown that $\bigcup_{n=1}^\infty A_n^k \subset A^k$ and that any $x \in A^k$ with $\lim\inf_{m\to\infty}f_m(x) > 1/k$ also belongs to $\bigcup_{n=1}^\infty A_n^k$ by using the definition of limit inferior. Currently I am stuck with the case $\lim\inf_{m\to\infty}f_m(x) = 1/k$. Intuitively it makes sense to me that such an $x$ should also belong to $\bigcup_{n=1}^\infty A_n^k$ since we may take arbitrarily large starting index $N \in \mathbb{N}$ to reduce the possible discrepancy between $\inf_{m\geq N}f_m(x)$ and $\lim\inf_{m\to\infty}f_m(x)$ by an arbitrary amount (as $\lim\inf_{m\to\infty}f_m(x) \geq \inf_{m\geq N}f_m(x)$).
What I am struggling with is to write this idea down rigorously. To be more specific, I am not that comfortable with set theoretical limits and somehow pulling out (and putting back in) set constructor predicates, which is most likely what is needed in this case.