avewright/proofwiki-math huggingface dataset:
Theorem: Restriction of Non-Connected Relation is Not Necessarily Non-Connected

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a non-connected relation on $S$.
Let $T \subseteq S$ be a subset of $S$.
Let $\RR {\restriction_T} \subseteq T \times T$ be the restriction of $\RR$ to $T$.
Then $\RR {\restriction_T}$ is not necessarily a non-connected relation on $T$.

Proof:
Proof by Counterexample:
Let $S = \set {a, b}$.
Let $\RR = \set {\tuple {a, a}, \tuple {b, b} }$.
$\RR$ is a non-connected relation, as can be seen by definition: neither $a \mathrel \RR b$ nor $b \mathrel \RR a$.
Now let $T = \set a$.
Then $\RR {\restriction_T} = \set {\tuple {a, a} }$.
Then $\RR {\restriction_T}$ is trivially connected on $T$.
{{qed}}
Theorem: Duals of Isomorphic Ordered Sets are Isomorphic

Let $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ be ordered sets.
Let $\struct {S, \succcurlyeq_1}$ and $\struct {T, \succcurlyeq_2}$ be the dual ordered sets of $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ respectively.
Let $f: \struct {S, \preccurlyeq_1} \to \struct {T, \preccurlyeq_2}$ be an order isomorphism.
Then $f: \struct {S, \succcurlyeq_1} \to \struct {T, \succcurlyeq_2} $ is also an order isomorphism.

Proof:
{{begin-eqn}}
{{eqn | q =\forall x, y \in S
      | l = x
      | o = \succcurlyeq_1
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \preccurlyeq_1
      | r = x
      | c = {{Defof|Dual Ordering}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f y
      | o = \preccurlyeq_2
      | r = \map f x
      | c = {{Defof|Order Isomorphism}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f x
      | o = \succcurlyeq_2
      | r = \map f y
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pushforward Measure is Measure

Let $\struct {X, \Sigma}$ and $\struct {X', \Sigma'}$ be measurable spaces.
Let $\mu$ be a measure on $\struct {X, \Sigma}$.
Let $f: X \to X'$ be a $\Sigma \, / \, \Sigma'$-measurable mapping.
Then the pushforward measure $f_* \mu: \Sigma' \to \overline \R$ is a measure.

Proof:
To show that $f_* \mu$ is a measure, it will suffice to check the axioms $(1)$, $(2)$ and $(3')$ for a measure.
Theorem: Lebesgue Measure Invariant under Orthogonal Group

Let $M \in \map {\mathrm O} {n, \R}$ be an orthogonal matrix.
Let $\lambda^n$ be $n$-dimensional Lebesgue measure.
Then the pushforward measure $M_* \lambda^n$ equals $\lambda^n$.

Proof:
By Orthogonal Group is Subgroup of General Linear Group, $M \in \GL {n, \R}$.
From Pushforward of Lebesgue Measure under General Linear Group, it follows that:
:$M_* \lambda^n = \size {\det M^{-1} } \lambda^n$
Since $M^{-1} \in \map {\mathrm O} {n, \R}$ by Orthogonal Group is Group, Determinant of Orthogonal Matrix applies to yield:
:$\size {\det M^{-1} } = 1$
Hence the result.
{{qed}}
{{wtd|In order to avoid circularity (through Pushforward of Lebesgue Measure under General Linear Group and Determinant as Volume of Parallelotope) the direct proof Schilling produces also needs to be covered}}
Theorem: Pushforward of Lebesgue Measure under General Linear Group

Let $M \in \GL {n, \R}$ be a nonsingular matrix.
Let $\lambda^n$ be $n$-dimensional Lebesgue measure.
Then the pushforward measure $M_* \lambda^n$ satisfies:
:$M_* \lambda^n = \size {\det M^{-1} } \cdot \lambda^n$

Proof:
From Linear Transformation on Euclidean Space is Continuous, $M^{-1}$ is a continuous mapping.
Thus from Continuous Mapping is Measurable, it is measurable, and so $M_* \lambda^n$ is defined.
Now let $B \in \map \BB {\R^n}$ be a Borel measurable set, and let $\mathbf x \in \R^n$.
Then:
{{begin-eqn}}
{{eqn | l = \map {M_* \lambda^n} {\mathbf x + B}
      | r = \map {\lambda^n} {\map {M^{-1} } {\mathbf x + B} }
      | c = {{Defof|Pushforward Measure}}
}}
{{eqn | r = \map {\lambda^n} {\map {M^{-1} } {\mathbf x} + \map {M^{-1} } B}
      | c = $M^{-1}$ is linear
}}
{{eqn | r = \map {\lambda^n} {\map {M^{-1} } B}
      | c = Lebesgue Measure is Translation Invariant
}}
{{eqn | r = \map {M_* \lambda^n} B
      | c = {{Defof|Pushforward Measure}}
}}
{{end-eqn}}
Thus $M_* \lambda^n$ is a translation invariant measure.
From Translation Invariant Measure on Euclidean Space is Multiple of Lebesgue Measure, it follows that:
:$M_* \lambda^n = \map {M_* \lambda^n} {\openint 0 1^n} \cdot \lambda^n$
Lastly, using Determinant as Volume of Parallelotope it follows that:
:$\map {M_* \lambda^n} {\openint 0 1^n} = \map {\lambda^n} {\map {M^{-1} } {\openint 0 1^n} } = \size {\det M^{-1} }$
Hence the result.
{{qed}}
Theorem: Pre-Image Sigma-Algebra on Domain is Generated by Mapping

Let $X, X'$ be sets, and let $f: X \to X'$ be a mapping.
Let $\Sigma'$ be a $\sigma$-algebra on $X'$.
Let $f: X \to X'$ be a mapping.
Then:
:$\map \sigma f = \map {f^{-1} } {\Sigma'}$
where
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$
:$\map {f^{-1} } {\Sigma'}$ denotes the pre-image $\sigma$-algebra under $f$

Proof:
By Characterization of Sigma-Algebra Generated by Collection of Mappings:
:$\map \sigma f = \map \sigma {\map {f^{-1} } {\Sigma'} }$
where the latter $\sigma$ denotes a $\sigma$-algebra generated by a collection of subsets.
By Pre-Image Sigma-Algebra on Domain is Sigma-Algebra, $\map {f^{-1} } {\Sigma'}$ is a $\sigma$-algebra.
Hence:
:$\map \sigma {\map {f^{-1} } {\Sigma'} } = \map {f^{-1} } {\Sigma'}$
{{qed}}
Theorem: Mapping between Euclidean Spaces Measurable iff Components Measurable

Let $\R^n$ and $\R^m$ be Euclidean spaces.
Denote by $\BB^n$ and $\BB^m$ their respective Borel $\sigma$-algebras.
Denote with $\BB$ the Borel $\sigma$-algebra on $\R$.
Let $f: \R^n \to \R^m$ be a mapping, and write:
:$\map f {\mathbf x} = \begin{bmatrix} \map {f_1} {\mathbf x} \\ \vdots \\ \map {f_m} {\mathbf x} \end{bmatrix}$
with, for $1 \le i \le m$, $f_i: \R^n \to \R$.
Then $f$ is $\BB^n \, / \, \BB^m$-measurable {{iff}}:
:$\forall i: f_i: \R^n \to \R$ is $\BB^n \, / \, \BB$-measurable

Proof:
=== Necessary Condition ===
Suppose that $f$ is $\BB^n \, / \, \BB^m$-measurable.
It is to be shown that for $1 \le i \le m$, $f_i: \R^n \to \R$ is $\BB^n \, / \, \BB$-measurable.
By Mapping Measurable iff Measurable on Generator and Characterization of Euclidean Borel Sigma-Algebra, it suffices to show that:
:$\map {f_i^{-1} } {\openint a b} \in \BB^n$
for every open real interval $\openint a b$.
Since $\map f {\mathbf x} = \mathbf y$ {{iff}}, for all $i$, $\map {f_i} {\mathbf x} = y_i$, it follows that:
:$\mathbf x \in \map {f^{-1} } {\mathbf y} \iff \forall i: \mathbf x \in \map {f_i^{-1} } {y_i}$
That is, {{iff}} $\ds \mathbf x \in \bigcap_{i \mathop = 1}^m \map {f_i^{-1} } {y_i}$.
By Preimage of Union under Mapping, it follows that for any $B \in \BB^m$:
:$\mathbf x \in \map {f^{-1} } B \iff \exists \mathbf y \in B: \forall i: \mathbf x \in \map {f_i^{-1} } {y_i}$
In particular, consider the open set $B = \set {\mathbf y \in \R^n: y_i \in \openint a b}$.
Then by construction of $B$, $\mathbf x \in \map {f_i^{-1} } {\openint a b}$ {{iff}} $\map f x \in B$.
Therefore, $\map {f_i^{-1} } {\openint a b} = \map {f^{-1} } B$.
Since $B$ is open, it is also measurable by Characterization of Euclidean Borel Sigma-Algebra.
Thus $\map {f_i^{-1} } {\openint a b} \in \BB^n$ as $f$ was assumed $\BB^n \, / \, \BB^m$-measurable.
{{MissingLinks|To appropriate versions of Definition:Preimage}}
{{qed|lemma}}
Theorem: Pre-Image Sigma-Algebra of Generated Sigma-Algebra

Let $f: X \to Y$ be a mapping.
Let $\GG \subseteq \powerset Y$ be a collection of subsets of $Y$.
Then the following equality of $\sigma$-algebras on $X$ holds:
:$f^{-1} \sqbrk {\map \sigma \GG} = \map \sigma {f^{-1} \sqbrk \GG}$
where
:$\sigma$ denotes a generated $\sigma$-algebra
:$f^{-1} \sqbrk {\map \sigma \GG}$ denotes the pre-image $\sigma$-algebra
:$f^{-1} \sqbrk \GG$ is the preimage of $\GG$ under $f$

Proof:
Since $\GG \subseteq \map \sigma \GG$, it follows immediately that:
:$f^{-1} \sqbrk \GG \subseteq f^{-1} \sqbrk {\map \sigma \GG}$
By Pre-Image Sigma-Algebra on Domain is Sigma-Algebra, the latter is a $\sigma$-algebra, and so by Generated Sigma-Algebra Preserves Subset, it follows that:
:$\map \sigma {f^{-1} \sqbrk \GG} \subseteq f^{-1} \sqbrk {\map \sigma \GG}$
Conversely, by definition of generated $\sigma$-algebra, we have:
:$f^{-1} \sqbrk \GG \subseteq \map \sigma {f^{-1} \sqbrk \GG}$
Hence from Mapping Measurable iff Measurable on Generator, it follows that $f$ is $\map \sigma {f^{-1} \sqbrk \GG} \, / \, \map \sigma \GG$-measurable.
But this by definition of measurable mapping means that:
:$f^{-1} \sqbrk {\map \sigma \GG} \subseteq \map \sigma {f^{-1} \sqbrk \GG}$
Hence the result, by definition of set equality.
{{qed}}
Theorem: Stieltjes Function of Measure is Stieltjes Function

Let $\mu$ be a measure on $\R$ with the Borel $\sigma$-algebra $\map \BB \R$.
Suppose that for every $n \in \N$:
:$\map \mu {\closedint {-n} n} < +\infty$
Then $F_\mu: \R \to \overline \R$, the Stieltjes function of $\mu$, is a Stieltjes function.

Proof:
By definition, $F_\mu$ is a Stieltjes function {{iff}} it is increasing and left-continuous.
Theorem: Chain Rule for Real-Valued Functions

Let $f: \R^n \to \R, \mathbf x \mapsto z$ be a differentiable real-valued function.
Let $\mathbf x = \begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix} \in \R^n$.
Further, let every element $x_i: 1 \le i \le n$ represent an implicitly defined differentiable real function of $t$.
Then $z$ is itself differentiable {{WRT|Differentiation}} $t$ and:
{{begin-eqn}}
{{eqn | l = \frac {\d z} {\d t}
      | r = \sum_{k \mathop = 1}^n \frac {\partial z} {\partial x_i} \frac {\d x_i} {\d t}
}}
{{end-eqn}}
where $\dfrac {\partial z} {\partial x_i}$ is the partial derivative of $z$ {{WRT|Differentiation}} $x_i$.

Proof:
$f$ is {{hypothesis}} differentiable.
From Characterization of Differentiability:
{{begin-eqn}}
{{eqn | l = \Delta z
      | r = \sum_{i \mathop = 1}^n \frac {\partial z} {\partial x_i} \Delta x_i + \sum_{i \mathop = 1}^n \epsilon_i \Delta x_i
      | c = $\forall i: 1 \le i \le n: \epsilon_i \to 0$ as $\Delta x_i \to 0$
}}
{{end-eqn}}
Let $\Delta t \ne 0$ and divide both sides of the equation by $\Delta t$:
{{begin-eqn}}
{{eqn | l = \frac {\Delta z} {\Delta t}
      | r = \sum_{i \mathop = 1}^n \frac {\partial z} {\partial x_i} \frac {\Delta x_i} {\Delta t} + \sum_{i \mathop = 1}^n \epsilon_i \frac {\Delta x_i} {\Delta t}
      | c = $\forall i: 1 \le i \le n: \epsilon_i \to 0$ as $\Delta x_i \to 0$
}}
{{end-eqn}}
Recall that each $x_i$ was defined to be differentiable {{WRT|Differentiation}} $t$, that is, that each $\dfrac {\d x_i} {\d t}$ exists.
Then $\Delta x_i \to 0$ as $\Delta t \to 0$.
Therefore:
{{begin-eqn}}
{{eqn | l = \frac {\d z} {\d t}
      | r = \sum_{i \mathop = 1}^n \frac {\partial z} {\partial x_i} \frac {\d x_i} {\d t} + \sum_{i \mathop = 1}^n 0 \frac {\d x_i} {\d t}
}}
{{eqn | r = \sum_{i \mathop = 1}^n \frac {\partial z} {\partial x_i} \frac {\d x_i} {\d t}
      | c = as $\Delta t \to 0$
}}
{{end-eqn}}
{{qed}}
{{proofread}}
Theorem: Totally Ordered Set is Well-Ordered iff Subsets Contain Infima

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Then $\struct {S, \preccurlyeq}$ is a well-ordered set {{iff}} every non-empty subset of $T \subseteq S$ has an infimum such that $\map \inf T \in T$.

Proof:
=== Sufficient Condition ===
Let $T \subseteq S$ such that $m := \map \inf T \in T$.
By definition, $m$ is a lower bound of $T$ and so:
:$\forall x \in T: m \preccurlyeq x$
That is:
:$\neg \exists x \in T: x \prec m$
Thus by definition $x$ is a minimal element of $T$.
Thus by definition $S$ is well-founded and so is a well-ordered set.
{{qed|lemma}}
Theorem: Pre-Measure of Finite Stieltjes Function is Pre-Measure

Let $\JJ_{ho}$ denote the collection of half-open intervals in $\R$.
Let $f: \R \to \R$ be a finite Stieltjes function.
Then the pre-measure of $f$, $\mu_f: \JJ_{ho} \to \overline \R_{\ge 0}$ is a pre-measure.
Here, $\overline \R_{\ge 0}$ denotes the set of positive extended real numbers.

Proof:
It is immediate from the definition of $\mu_f$ that:
:$\map {\mu_f} \O = 0$
Now suppose that for some half-open interval $\hointr a b$ one has:
:$\ds \hointr a b = \bigcup_{n \mathop \in \N} \hointr {b_n} {b_{n + 1} }$
where $b_0 = a$ and $\ds \lim_{n \mathop \to \infty} b_n = b$.
Then we compute:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop \in \N} \map {\mu_f} {\hointr {b_n} {b_{n + 1} } }
      | r = \sum_{n \mathop \in \N} \map f {b_{n + 1} } - \map f {b_n}
      | c = {{Defof|Pre-Measure of Finite Stieltjes Function}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map f {b_{n + 1} } - \map f {b_0}
      | c = Telescoping Series
}}
{{eqn | r = \map f b - \map f a
      | c = Definition of $\sequence {b_n}_{n \mathop \in \N}$
}}
{{eqn | r = \map {\mu_f} {\hointr a b}
      | c = {{Defof|Pre-Measure of Finite Stieltjes Function}}
}}
{{end-eqn}}
which verifies the second condition for a pre-measure.
Hence $\mu_f$ is indeed a pre-measure.
{{qed}}
Category:Pre-Measures
Category:Stieltjes Functions
owe6esq5o6d5g4i416yu6fm1wghn32w
Theorem: Pre-Measure of Finite Stieltjes Function Extends to Unique Measure

Let $\JJ_{ho}$ denote the collection of half-open intervals in $\R$.
Let $f: \R \to \R$ be a finite Stieltjes function.
Then the pre-measure of $f$, $\mu_f$, extends uniquely to a measure $\mu$ on $\map \BB \R$, the Borel $\sigma$-algebra on $\R$.
This unique measure $\mu$ is the measure of $f$.

Proof:
We intend to use Carathéodory's Theorem (Measure Theory).
To this end, observe that by Characterization of Euclidean Borel Sigma-Algebra, we have:
:$\map \BB \R = \map \sigma {\JJ_{ho} }$
From Pre-Measure of Finite Stieltjes Function is Pre-Measure, $\mu_f$ is a pre-measure.
Note that for all $n \in \N$, we have:
:$\map {\mu_f} {\hointr {-n} n} = \map f n - \map f {-n} < +\infty$
and $\hointr {-n} n \uparrow \R$ as an increasing sequence of sets.
All these facts combine with Carathéodory's Theorem (Measure Theory) to establish existence and uniqueness of $\mu$.
{{qed}}
Theorem: Stieltjes Function of Measure of Finite Stieltjes Function

Let $f: \R \to \R$ be a finite Stieltjes function.
Let $\mu_f$ be the measure of $f$.
Let $f_{\mu_f}$ be the Stieltjes function of $\mu_f$.
Then $f_{\mu_f} = f$.

Proof:
{{ProofWanted}}
Category:Measure Theory
2av83obmotj1dfnhu3llbfontcqut8d
Theorem: Measure of Stieltjes Function of Measure

Let $\mu$ be a measure on $\map \BB \R$, the Borel $\sigma$-algebra on $\R$.
Suppose that for all $n \in \N$, $\mu$ satisfies:
:$\map \mu {\hointr {-n} n} < +\infty$
Let $f_\mu$ be the Stieltjes function of $\mu$.
Let $\mu_{f_\mu}$ be the measure of $f_\mu$.
Then $\mu_{f_\mu} = \mu$.

Proof:
From Pre-Measure of Finite Stieltjes Function Extends to Unique Measure, it suffices to verify that:
:$\map {\mu_{f_\mu} } {\hointr a b} = \map \mu {\hointr a b}$
for all half-open intervals $\hointr a b$.
Now we have:
{{begin-eqn}}
{{eqn|l = \map {\mu_{f_\mu} } {\hointr a b}
     |r = \map {f_\mu} b - \map {f_\mu} a
     |c = Definition of $\mu_{f_\mu}$
}}
{{end-eqn}}
If either $a = 0$ or $b = 0$, the result follows immediately from the definition of $f_\mu$.
Now suppose that $a < b < 0$.
Then:
{{begin-eqn}}
{{eqn|l = \map {f_\mu} b - \map {f_\mu} a
     |r = \map \mu {\hointr a 0} - \map \mu {\hointr b 0}
     |c = Definition of $f_\mu$
}}
{{eqn|r = \map \mu {\hointr a b}
     |c = Measure of Set Difference with Subset
}}
{{end-eqn}}
Finally, let $0 < a < b$.
Then:
{{begin-eqn}}
{{eqn|l = \map {f_\mu} b - \map {f_\mu} a
     |r = \map \mu {\hointr 0 b} - \map \mu {\hointr 0 a}
     |c = Definition of $f_\mu$
}}
{{eqn|r = \map \mu {\hointr a b}
     |c = Measure of Set Difference with Subset
}}
{{end-eqn}}
The final case $a < 0 < b$ is a trivial consequence of Measure is Finitely Additive Function.
Hence it must be that $\mu_{f_\mu} = \mu$.
{{qed}}
Theorem: Cantor Set has Zero Lebesgue Measure

Let $\CC$ be the Cantor set.
Let $\lambda$ denote the Lebesgue measure on the Borel $\sigma$-algebra $\map \BB \R$ on $\R$.
Then $\CC$ is $\map \BB \R$-measurable, and $\map \lambda \CC = 0$.
That is, $\CC$ is a $\lambda$-null set.

Proof:
Consider the definition of $\CC$ as a limit of a decreasing sequence.
In the notation as introduced there, we see that each $S_n$ is a collection of disjoint closed intervals.
From Closed Set Measurable in Borel Sigma-Algebra, these are measurable sets.
Furthermore, each $S_n$ is finite.
Hence by Sigma-Algebra Closed under Union, it follows that $C_n := \ds \bigcup S_n$ is measurable as well.
Then, as we have:
:$\CC = \ds \bigcap_{n \mathop \in \N} C_n$
it follows from Sigma-Algebra Closed under Countable Intersection that $\CC$ is measurable.
The $C_n$ also form a decreasing sequence of sets with limit $\CC$.
Thus, from Characterization of Measures: $(3')$, it follows that:
:$\map \lambda \CC = \ds \lim_{n \mathop \to \infty} \map \lambda {C_n}$
It is not too hard to show that, for all $n \in \N$:
:$\map \lambda {C_n} = \paren {\dfrac 2 3}^n$
{{finish|yes, I know}}
Now we have by Sequence of Powers of Number less than One that:
:$\ds \lim_{n \mathop \to \infty} \paren {\frac 2 3}^n = 0$
and the result follows.
{{qed}}
Theorem: Factorization Lemma/Real-Valued Function

Then a mapping $g: X \to \R$ is $\map \sigma f \, / \, \map \BB \R$-measurable {{iff}}:
:There exists a $\Sigma \, / \, \map \BB \R$-measurable mapping $\tilde g: Y \to \R$ such that $g = \tilde g \circ f$
where:
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$
:$\map \BB \R$ denotes the Borel $\sigma$-algebra on $\R$

Proof:
=== Necessary Condition ===
Let $g$ be a $\map \sigma f \, / \, \map \BB \R$-measurable function.
We need to construct a measurable $\tilde g$ such that $g = \tilde g \circ f$.
Let us proceed in the following fashion:
:Establish the result for $g$ a characteristic function;
:Establish the result for $g$ a simple function;
:Establish the result for all $g$
So let $g = \chi_E$ be a characteristic function.
By Characteristic Function Measurable iff Set Measurable, it follows that $E$ is $\sigma \left({f}\right)$-measurable.
Thus there exists some $A \in \Sigma$ such that $E = \map {f^{-1} } A$.
Again by Characteristic Function Measurable iff Set Measurable, we have $\chi_A: Y \to \R$ is measurable.
It follows that $\chi_E = \chi_A \circ f$, and $\tilde g := \chi_A$ works.
Now let $g = \ds \sum_{i \mathop = 1}^n a_i \chi_{E_i}$ be a simple function.
Let $A_i$ be associated to $E_i$ as above. Then we have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n a_i \chi_{E_i}
      | r = \sum_{i \mathop = 1}^n a_i \paren {\chi_{A_i} \circ f}
      | c = by the result for characteristic functions
}}
{{eqn | r = \paren {\sum_{i \mathop = 1}^n a_i \chi_{A_i} } \circ f
      | c = Composition of Mappings is Linear
}}
{{end-eqn}}
Now $\ds \sum_{i \mathop = 1}^n a_i \chi_{A_i}$ is a simple function, hence measurable by Simple Function is Measurable.
Therefore, it suffices as a choice for $\tilde g$.
Next, let $g \ge 0$ be a measurable function.
By Measurable Function is Pointwise Limit of Simple Functions, we find simple functions $g_j$ such that:
:$\ds \lim_{j \mathop \to \infty} g_j = g$
Applying the previous step to each $g_j$, we find a sequence of $\tilde g_j$ satisfying:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = g$
From Composition with Pointwise Limit it follows that we have, putting $\tilde g := \ds \lim_{j \mathop \to \infty} \tilde g_j$:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = \tilde g \circ f$
{{explain|Address why (if?!) $\tilde g$ is well defined}}
An application of Pointwise Limit of Measurable Functions is Measurable yields $\tilde g$ measurable.
Thus we have provided a suitable $\tilde g$ for every $g$, such that:
:$g = \tilde g \circ f$
as desired.
{{qed}}
Theorem: Characterization of Measurable Functions

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \overline \R$ be an extended real-valued function.
Then the following are all equivalent:
{{begin-eqn}}
{{eqn | n = 1
      | o = 
      | r = f\) is measurable \(
}}
{{eqn | n = 2
      | o = 
      | r = \forall \alpha \in \R: \set {x \in X: \map f x \le \alpha} \in \Sigma
}}
{{eqn | n = $2'$
      | o = 
      | r = \forall \alpha \in \Q: \set {x \in X: \map f x \le \alpha} \in \Sigma
}}
{{eqn | n = 3
      | o = 
      | r = \forall \alpha \in \R: \set {x \in X: \map f x < \alpha} \in \Sigma
}}
{{eqn | n = $3'$
      | o = 
      | r = \forall \alpha \in \Q: \set {x \in X: \map f x < \alpha} \in \Sigma
}}
{{eqn | n = 4
      | o = 
      | r = \forall \alpha \in \R: \set {x \in X: \map f x \ge \alpha} \in \Sigma
}}
{{eqn | n = $4'$
      | o = 
      | r = \forall \alpha \in \Q: \set {x \in X: \map f x \ge \alpha} \in \Sigma
}}
{{eqn | n = 5
      | o = 
      | r = \forall \alpha \in \R: \set {x \in X: \map f x > \alpha} \in \Sigma
}}
{{eqn | n = $5'$
      | o = 
      | r = \forall \alpha \in \Q: \set {x \in X: \map f x > \alpha} \in \Sigma
}}
{{end-eqn}}

Proof:
Each of $(2)$ up to $(5')$ is equivalent to $(1)$ by combining Mapping Measurable iff Measurable on Generator and Generators for Extended Real Sigma-Algebra.
{{qed}}
Theorem: Characterization of Extended Real Sigma-Algebra

Let $\map \BB \R$ be the Borel $\sigma$-algebra on $\R$.
Let $\overline \BB$ be the extended real $\sigma$-algebra.
Define $\SS := \powerset {\set {-\infty, +\infty} }$, where $\PP$ denotes power set.
Then:
:$\overline \BB = \set {B \cup S: B \in \map \BB \R, S \in \SS}$

Proof:
Let $\overline B \in \overline \BB$.
Then by Extended Real Sigma-Algebra Induces Borel Sigma-Algebra on Reals, we have:
:$\overline B \cap \R \in \map \BB \R$
We also have, by definition of the extended real numbers $\overline \R$, that:
:$\overline \R \setminus \R = \set {-\infty, +\infty}$
and therefore, $\overline B \setminus \R \subseteq \set {-\infty, +\infty}$.
Here, $\setminus$ signifies set difference.
By Set Difference Union Intersection:
:$\overline B = \paren {\overline B \setminus \R} \cup \paren {\overline B \cap \R}$
Therefore, any $\overline B \in \overline \BB$ is of the purported form $B \cup S$ with $B \in \map \BB \R$ and $S \in \SS$.
It remains to show that any such set is in fact an element of $\overline \BB$.
Since any $B \in \map \BB \R$ is naturally also in $\overline \BB$, it suffices to show that:
:$\SS \subseteq \overline \BB$
by applying Sigma-Algebra Closed under Union.
From Closed Set Measurable in Borel Sigma-Algebra, it will now suffice to show that:
:$\O, \set {-\infty}, \set {+\infty}, \set {-\infty, +\infty}$
are all closed sets in $\overline \R$.
That they are follows from Extended Real Number Space is Hausdorff and Finite Subspace of Hausdorff Space is Closed.
{{qed}}
Theorem: Extended Real Sigma-Algebra Induces Borel Sigma-Algebra on Reals

Let $\overline \BB$ be the extended real $\sigma$-algebra.
Let $\map \BB \R$ be the Borel $\sigma$-algebra on $\R$.
Then:
:$\overline \BB_\R = \map \BB \R$
where $\overline \BB_\R$ denotes a trace $\sigma$-algebra.

Proof:
We have Euclidean Space is Subspace of Extended Real Number Space.
The result follows from Borel Sigma-Algebra of Subset is Trace Sigma-Algebra.
{{qed}}
Theorem: Characteristic Function Measurable iff Set Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $E \subseteq X$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$E \in \Sigma$; that is, $E$ is a $\Sigma$-measurable set}}
{{item|(2):|$\chi_E: X \to \set {0, 1}$, the characteristic function of $E$, is $\Sigma$-measurable}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Assume that $E \in \Sigma$.
It is clear that $x \notin \set {0, 1}$ implies $\map {\chi_E^{-1} } x = \O$.
Hence Preimage of Union under Mapping and Characteristic Function Determined by 1-Fiber yield, for any $\alpha \in \R$:
:<nowiki>$\set {x \in X: \map {\chi_E} x \ge \alpha} = \begin{cases} \O & \text{if $1 < \alpha$}\\
E & \text{if } 0 < \alpha \le 1 \\
X & \text{if } \alpha \le 0 \end{cases}$</nowiki>
Since $\Sigma$ is a $\sigma$-algebra, $X \in \Sigma$.
By assumption, also $E \in \Sigma$.
Lastly, Sigma-Algebra Contains Empty Set ensures $\O \in \Sigma$.
This establishes $(4)$ of Characterization of Measurable Functions.
Hence $\chi_E$ is $\Sigma$-measurable.
{{qed|lemma}}