Proof of The Sets Where a Function Is at Least 1/n Form a Sequence of Measurable Sets

Each set is measurable. Let $n\in\mathbb{N}$. The function $f:X\to[0,\infty]$ is $\mathcal{F}/\mathcal{B}([0,\infty])$-measurable (Nonnegative Measurable Maps and Their Lebesgue Integral (i), Measurable Map, and the Set of Measurable Maps (vi)). As $1/n\in\mathbb{R}$, the set $R_{n}=\{y\in[0,\infty]:y\ge1/n\}$ belongs to $\mathcal{B}([0,\infty])$ by Borel Subsets of [0,∞]: Rays, the Point ∞, and Traces on ℝ (i) with $a=1/n$, so $f^{-1}(R_{n})\in\mathcal{F}$ (Measurable Map, and the Set of Measurable Maps (i)). Since $f(x)\in[0,\infty]$ for every $x\in X$, and $y\ge1/n$ means $1/n\le y$ (The Extended Real Line, Its Order, and [0,∞] (iii)), $x\in f^{-1}(R_{n})$ holds if and only if $x\in X$ and $1/n\le f(x)$ (The Image and the Preimage of a Class under a Class (ii)). Hence $\{x\in X:1/n\le f(x)\}=f^{-1}(R_{n})\in\mathcal{F}$.

The term $1/i$. Take $k=0$ in Conditions Expressed by a Predicative Formula, and Guards (i), let $\gamma$ be the guard $\mathbb{N}=\mathbb{N}$, which every assignment satisfies, and let $i$ be a set variable. $\mathbb{R}$, with $+$, $\cdot$, $0$ and $1$, is a field by The Structure of ℝ as a Field and an Ordered Ring (i), hence a commutative ring (Fields (i)), so by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (ii) there is a function $\iota:\mathbb{N}_{0}\to\mathbb{R}$ with $\iota(n)=n_{\mathbb{R}}$, the image of $n$ in $\mathbb{R}$, for every $n\in\mathbb{N}_{0}$; $n_{\mathbb{R}}$ is the real number that $n$ denotes (Commutative Rings, Fields and Ordered Fields: Standard Notation (iv)). The parameters are $\mathbb{N}$, $\mathbb{R}$ with its operations, order, $0$ and $1$, the function $\iota$, $X$, $\mathcal{F}$ and $f$. Under the guard $\gamma\wedge i\in\mathbb{N}$ for the variable $i$, $i$ is a term of type $\mathbb{N}_{0}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), as $\mathbb{N}\subseteq\mathbb{N}_{0}$ (Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (i)), so $\iota(i)$ is a term of type $\mathbb{R}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii). Let $1/i$ be the term whose value, when $n\in\mathbb{N}$ is assigned to $i$, is the reciprocal $\iota(n)^{-1}=(n_{\mathbb{R}})^{-1}=1/n$ in the field $\mathbb{R}$. Its value lies in $\mathbb{R}$, as shown before the clause (i). For a set variable $z$ other than $i$, the condition $\gamma\wedge i\in\mathbb{N}\wedge z=1/i$ is expressed by the predicative formula $\gamma\wedge i\in\mathbb{N}\wedge\exists y\,((i,y)\in\iota\wedge\psi)$, where $\psi$ expresses $y\in\mathbb{R}\wedge y\neq0\wedge z=y^{-1}$ by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (vii) for the ordered field $\mathbb{R}$ (The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i)), by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i), since $i\in\operatorname{dom}\iota$ and $\iota(i)\neq0$ for $i\in\mathbb{N}$. Hence $1/i$ is a term of type $\mathbb{R}$ under $\gamma\wedge i\in\mathbb{N}$ (Terms and Typed Terms under a Guard (ii)).

The term $\{f\ge1/i\}$. The parameter $f$ lies in $[0,\infty]^{X}$ (Measurable Map, and the Set of Measurable Maps (ii)), so it is a term of type $[0,\infty]^{X}$ under $\gamma\wedge i\in\mathbb{N}$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (ii)). By Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (v) with $C=[0,\infty]$, $C'=\mathbb{R}$, $u=f$ and $a=1/i$, the term $\{f\ge1/i\}$ is a term of type $\mathcal{P}(X)$ under $\gamma\wedge i\in\mathbb{N}$, and its value when $n$ is assigned to $i$ is $\{x\in X:f(x)\ge1/n\}=\{x\in X:1/n\le f(x)\}$. By the first step this value lies in $\mathcal{F}$; and condition Terms and Typed Terms under a Guard (iv) of Terms and Typed Terms under a Guard (ii) does not involve the type, so it holds as for the type $\mathcal{P}(X)$. Hence $\{f\ge1/i\}$ is a term of type $\mathcal{F}$ under $\gamma\wedge i\in\mathbb{N}$.

The sequence. $\mathbb{N}$ is a set, and so is $\mathcal{F}$ (σ-Algebra and Measurable Space (i)). By Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi) with $D=\mathbb{N}$, $C=\mathcal{F}$ and $t=\{f\ge1/i\}$, there is a function $h:\mathbb{N}\to\mathcal{F}$ with $h(n)=\{x\in X:1/n\le f(x)\}$ for every $n\in\mathbb{N}$. This function is a sequence $(A_{n})_{n\in\mathbb{N}}$ in $\mathcal{F}$ (Sequences (i)) with $A_{n}=h(n)$, which proves (i).