avewright/proofwiki-math huggingface dataset:
Theorem: Mappings in Product of Sets are Surjections/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be an indexed family of sets.
Let $\struct {P, \family {\phi_i} _{i \mathop \in I} }$ be a product of $S$ and $T$.
Then for all $i \in I$, $\phi_i$ is a surjection.

Proof:
From the definition:
:For all sets $X$ and all indexed families $\family {f_i}_{i \mathop \in I}$ of mappings $f_i: X \to S_i$ there exists a unique mapping $h: X \to P$ such that:
::$\forall i \in I: \phi_i \circ h = f_i$
Let:
:$i \in I$
:$X = S_i$
:$f_i = I_{S_i}$
where $I_{S_i}$ is the identity mapping on $S_i$.
Then we have:
:$\phi_i \circ h = I_{S_i}$
From Identity Mapping is Surjection:
:$I_{S_i}$ is a surjection.
From Surjection if Composite is Surjection:
:$\phi_i$ is a surjection.
$i \in I$ is arbitrary so the argument applies whatever its value.
Hence the result.
{{qed}}
Theorem: Cartesian Product is Set Product/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets.
For all $j \in I$, let $\pr_i: \ds \prod_{j \mathop \in I} \family {S_j} \to S_i$ be the $i$th projection from $\ds \prod_{j \mathop \in I} \family {S_j}$ to $S_i$.
Then $\struct {\ds \prod_{j \mathop \in I} \family {S_j}, \family {\pr_i}_{i \mathop \in I} }$ is a set product.

Proof:
Let $i \in I$.
Consider any set $X$ and any indexed family of mappings $\family {f_i: X \to S_i}_{i \mathop \in I}$.
Define $h: X \to \ds \prod_{j \mathop \in I} \family {S_j}$ by:
:$\forall x \in X: \map h x = \family {\map {f_i} x}_{i \mathop \in I}$
Then for all $x \in X$ and $i \in I$ we have:
:$\map {\paren {\pr_i \mathop \circ h} } x = \map {\pr_i} {\family {\map {f_i} x}_{i \mathop \in I} } = \map {f_i} x$
So:
:$\pr_i \mathop \circ h = f_i$
Thus $h$ is shown to exist.
Suppose there exists a mapping $k: X \to \ds \prod_{j \mathop \in I} \family {S_j}$ such that:
:$\forall i \in I: \pr_1 \mathop \circ k = f_i$
Let $x \in X$ and let:
:$\map k x = \family {s_j}_{j \mathop \in I}$
for some $\family {s_j}_{j \mathop \in I} \in \ds \prod_{j \mathop \in I} \family {S_j}$.
Then:
:$\map {f_i} x = \map {\paren {\pr_i \mathop \circ k} } x = \map {\pr_i} {\family {s_j}_{j \mathop \in I} } = s_i$
and so:
:$\map k x = \family {s_j}_{j \mathop \in I} = \family {\map {f_i} x}_{i \mathop \in I} = \map h x$
and so $k = h$.
So $h$ is unique.
Hence the result.
{{qed}}
Theorem: Cauchy-Bunyakovsky-Schwarz Inequality/Lebesgue 2-Space

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \R$ be $\mu$-square integrable functions, that is $f, g \in \map {\LL^2} \mu$, Lebesgue $2$-space.
Then:
:$\ds \int \size {f g} \rd \mu \le \norm f_2^2 \cdot \norm g_2^2$
where $\norm {\, \cdot \,}_2$ is the $2$-norm.

Proof:
Follows directly from Hölder's Inequality for Integrals with $p = q = 2$.
{{qed}}
Theorem: Preimage of Intersection under Relation/General Result

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T \subseteq \powerset T$.
Then:
:$\ds \RR^{-1} \sqbrk {\bigcap \mathbb T} \subseteq \bigcap_{X \mathop \in \mathbb T} \RR^{-1} \sqbrk X$

Proof:
This follows from Image of Intersection under Relation: General Result, and the fact that $\RR^{-1}$ is itself a relation, and therefore obeys the same rules.
{{qed}}
Category:Relation Theory
Category:Set Intersection
4un5yucfff5xfy12bhj1clb6tbhxpt5
Theorem: Image of Union under Relation/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {S_i}_{i \mathop \in I}$ be a family of subsets of $S$.
Let $\RR \subseteq S \times T$ be a relation.
Then:
:$\ds \RR \sqbrk {\bigcup_{i \mathop \in I} S_i} = \bigcup_{i \mathop \in I} \RR \sqbrk {S_i}$
where $\ds \bigcup_{i \mathop \in I} S_i$ denotes the union of $\family {S_i}_{i \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = t
      | o = \in
      | r = \RR \sqbrk {\bigcup_{i \mathop \in I} S_i}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists s \in \bigcup_{i \mathop \in I} S_i
      | l = t
      | o = \in
      | r = \map \RR s
      | c = Image of Subset under Relation equals Union of Images of Elements
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I: \exists s \in S_i
      | l = t
      | o = \in
      | r = \map \RR s
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = t
      | o = \in
      | r = \RR \sqbrk {S_i}
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = t
      | o = \in
      | r = \bigcup_{i \mathop \in I} \RR \sqbrk {S_i}
      | c = {{Defof|Union of Family}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Image of Intersection under Relation/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {S_i}_{i \mathop \in I}$ be a family of subsets of $S$.
Let $\RR \subseteq S \times T$ be a relation.
Then:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} S_i} \subseteq \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}$
where $\ds \bigcap_{i \mathop \in I} S_i$ denotes the intersection of $\family {S_i}_{i \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall i \in I
      | l = \bigcap_{j \mathop \in I} S_j
      | o = \subseteq
      | r = S_i
      | c = Intersection is Subset: Family of Sets
}}
{{eqn | ll= \leadsto
      | q = \forall i \in I
      | l = \RR \sqbrk {\bigcap_{j \mathop \in I} S_j}
      | o = \subseteq
      | r = \RR \sqbrk {S_i}
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {\bigcap_{i \mathop \in I} S_i}
      | o = \subseteq
      | r = \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}
      | c = Intersection is Largest Subset: Family of Sets
}}
{{end-eqn}}
{{qed}}
Theorem: Preimage of Union under Relation/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $\RR \subseteq S \times T$ be a relation.
Then:
:$\ds \RR^{-1} \sqbrk {\bigcup_{i \mathop \in I} T_i} = \bigcup_{i \mathop \in I} \RR^{-1} \sqbrk {T_i}$
where:
:$\ds \bigcup_{i \mathop \in I} T_i$ denotes the union of $\family {T_i}_{i \mathop \in I}$
:$\RR^{-1} \left[{T_i}\right]$ denotes the preimage of $T_i$ under $\RR$.

Proof:
We have that $\RR^{-1}$ is itself a relation.
The result follows from Image of Union under Relation: Family of Sets.
{{qed}}
Category:Preimage of Union under Relation
Category:Indexed Families
g0l0paaenfqviok39mbmorxlo0x50lg
Theorem: Preimage of Intersection under Relation/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $\RR \subseteq S \times T$ be a relation.
Then:
:$\ds \RR^{-1} \sqbrk {\bigcap_{i \mathop \in I} T_i} \subseteq \bigcap_{i \mathop \in I} \RR^{-1} \sqbrk {T_i}$
where $\ds \bigcap_{i \mathop \in I} T_i$ denotes the intersection of $\family {T_i}_{i \mathop \in I}$.

Proof:
This follows from Image of Intersection under Relation: Family of Sets, and the fact that $\RR^{-1}$ is itself a relation, and therefore obeys the same rules.
{{qed}}
Category:Relation Theory
Category:Set Intersection
ay5y7m74ej87s8gd6b8vmfa30p39edj
Theorem: Image of Intersection under Injection/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {S_i}_{i \mathop \in I}$ be a family of subsets of $S$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f \sqbrk {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} f \sqbrk {S_i}$
{{iff}} $f$ is an injection.
This can be expressed in the language and notation of direct image mappings as:
:$\ds \map {f^\to} {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} \map {f^\to} {S_i}$

Proof:
An injection is a type of one-to-one relation, and therefore also a one-to-many relation.
Therefore Image of Intersection under One-to-Many Relation: Family of Sets applies:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}$
{{iff}} $\RR$ is a one-to-many relation.
We have that $f$ is a mapping and therefore a many-to-one relation.
So $f$ is a one-to-many relation {{iff}} $f$ is also an injection.
It follows that:
:$\ds f \sqbrk {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} f \sqbrk {S_i}$
{{iff}} $f$ is an injection.
{{qed}}
Theorem: Image of Intersection under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {S_i}_{i \mathop \in I}$ be a family of subsets of $S$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f \sqbrk {\bigcap_{i \mathop \in I} S_i} \subseteq \bigcap_{i \mathop \in I} f \sqbrk {S_i}$
where $\ds \bigcap_{i \mathop \in I} S_i$ denotes the intersection of $\family {S_i}_{i \mathop \in I}$.

Proof:
As $f$, being a mapping, is also a relation, we can apply Image of Intersection under Relation: Family of Sets:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} S_i} \subseteq \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}$
{{qed}}
Theorem: Image of Union under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {S_i}_{i \mathop \in I}$ be a family of subsets of $S$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f \sqbrk {\bigcup_{i \mathop \in I} S_i} = \bigcup_{i \mathop \in I} f \sqbrk {S_i}$
where $\ds \bigcup_{i \mathop \in I} S_i$ denotes the union of $\family {S_i}_{i \mathop \in I}$.
This can be expressed in the language and notation of direct image mappings as:
:$\ds \map {f^\to} {\bigcup_{i \mathop \in I} S_i} = \bigcup_{i \mathop \in I} \map {f^\to} {S_i}$

Proof:
As $f$, being a mapping, is also a relation, we can apply Image of Union under Relation: Family of Sets:
:$\ds \RR \sqbrk {\bigcup_{i \mathop \in I} S_i} = \bigcup_{i \mathop \in I} \RR \sqbrk {S_i}$
{{qed}}
Theorem: Minkowski's Inequality/Lebesgue Spaces

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p \in \closedint 1 \infty$. 
Let $f, g: X \to \R$ be $p$-integrable, that is, elements of Lebesgue $p$-space $\map {\LL^p} \mu$.
Then their pointwise sum $f + g: X \to \R$ is also $p$-integrable, and:
:$\norm {f + g}_p \le \norm f_p + \norm g_p$
where $\norm {\, \cdot \, }_p$ denotes the $p$-seminorm.

Proof:
We split into three cases.
Theorem: Lebesgue Space is Vector Space

Let $\struct {X, \Sigma, \mu}$ be a measure space and let $p \in \closedint 1 \infty$.
Let $\map {\LL^p} {X, \Sigma, \mu}$ be Lebesgue $p$-space on $\struct {X, \Sigma, \mu}$.
Then $\map {\LL^p} {X, \Sigma, \mu}$ is a vector subspace of $\map \MM {X, \Sigma, \R}$, the space of real-valued $\Sigma$-measurable functions on $X$.
In particular, it is a vector space over $\R$.

Proof:
From Space of Real-Valued Measurable Functions is Vector Space: 
:$\map \MM {X, \Sigma, \R}$ forms a vector space with pointwise addition and pointwise scalar multiplication.
From construction, we have: 
:$\map {\LL^p} {X, \Sigma, \mu} \subseteq \map \MM {X, \Sigma, \R}$
Since $0 \in \map {\LL^p} {X, \Sigma, \mu}$, we have $\map {\LL^p} {X, \Sigma, \mu} \ne \O$.
From the One-Step Vector Subspace Test, it suffices to show that for each $f, g \in \map {\LL^p} {X, \Sigma, \mu}$ and $\lambda \in \R$ we have: 
:$f + \lambda g \in \map {\LL^p} {X, \Sigma, \mu}$
Theorem: Riesz-Fischer Theorem

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p \in \R$, $p \ge 1$.
The Lebesgue $p$-space $\map {\LL^p} \mu$, endowed with the $p$-norm $\norm {\cdot}_p$, is a Banach space.

Proof:
From Absolutely Convergent Series in Normed Vector Space is Convergent iff Space is Banach, to prove $\map {\LL^p} \mu$ is complete, it suffices to prove that every absolutely summable sequence in $\map {\LL^p} \mu$ is summable.
{{explain|Provide supporting information as to why this proves the result.}}
Let $\sequence {f_n}$ be an absolutely summable sequence in $\map {\LL^p} \mu$.
Define:
:$\ds \sum_{k \mathop = 1}^\infty \norm {f_k}_p =: B < \infty$
Also define:
:$\ds G_n := \sum_{k \mathop = 1}^n \size {f_k}$
and:
:$\ds G = \sum_{k \mathop = 1}^\infty \size {f_k}$
It is clear that the conditions of the Monotone Convergence Theorem (Measure Theory) hold, so that:
:$\ds \int_X G^p = \lim_{n \mathop \to \infty} \int_X G_n^p$
By observing that:
{{begin-eqn}}
{{eqn | l = \norm {G_n}_p
      | o = \le
      | r = \sum_{k \mathop = 1}^n \norm {f_n}_p
      | c = Minkowski's Inequality on Lebesgue Space
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^\infty \norm {f_k}_p
}}
{{eqn | o = \le
      | r = B
      | c = Definition of $B$
}}
{{eqn | o = <
      | r = \infty
}}
{{end-eqn}}
we can also say that:
:$\ds \int_X \size {G_n}^p \le B^p$
and therefore:
:$\ds \lim_{n \mathop \to \infty} \int_X \size {G_n}^p \le B^p$
Therefore we have that:
:$\ds \int_X G^p \le B^p < \infty$
This confirms:
:$G \in \map {\LL^p} \mu$
In particular:
:$G \in \map {\LL^p} \mu$
entails that:
:$G < \infty$ a.e.
So $\sequence {f_k}$ is absolutely summable a.e..
By Absolutely Convergent Real Series is Convergent:
:$\ds F = \sum_{k \mathop = 1}^\infty f_k$
converges a.e.
Because $\size F \le G$:
:$F \in \map {\LL^p} \mu$
It only remains to show that:
:$\ds \sum_{k \mathop = 1}^n f_k \to F$ in $\norm {\cdot}_p$
which we can accomplish by Lebesgue's Dominated Convergence Theorem.
{{ExtractTheorem|extract the part of proof below into a page for a theorem: Dominated Pointwise Convergence implies Convergence in Lp as proved in [https://math.stackexchange.com/a/1515346/745350 StackExchange]}}
Because $\ds \size {F - \sum_{k \mathop = 1}^n f_k}^p \le \paren {2 G}^p \in \map{\LL^1}\mu$, the theorem applies.
We infer:
:$\ds \norm {F - \sum_{k \mathop = 1}^n f_k}_p^p = \int_X \size {F - \sum_{k \mathop = 1}^n f_k}^p \to 0$
Therefore, by definition of $L^p$ norm in $\map {\LL^p} \mu$, we have that $\ds \sum_{k \mathop = 1}^\infty f_k$ converges in $\map {\LL^p} \mu$.
This shows that $\sequence {f_k}$ is summable, as we were to prove.  
{{qed}}
{{Namedfor|Frigyes Riesz|name2 = Ernst Sigismund Fischer|cat = Riesz F|cat2 = Fischer}}
Theorem: Pointwise Convergent Bounded Sequence in Lebesgue Space Converges in Norm

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p \in \R_{\ge 1}$.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n: X \to \R$ be a sequence in Lebesgue $p$-space $\map {\LL^p} \mu$.
Suppose that the pointwise limit $f := \ds \lim_{n \mathop \to \infty} f_n$ exists $\mu$-almost everywhere.
Suppose that for some $g \in \map {\LL^p} \mu$, the pointwise inequality $\size {f_n} \le g$ holds for all $n \in \N$.
Then $f \in \map {\LL^p} \mu$, and:
:$\ds \lim_{n \mathop \to \infty} \norm {f - f_n}_p = 0$
where $\norm {\, \cdot \,}_p$ denotes the $p$-seminorm.

Proof:
Since:
:$\ds \size f = \lim _{n \mathop \to \infty} \size {f_n} \le g$
$\mu$-almost everywhere, we have:
:$\ds \int \size f^p \rd \mu \le \int g^p \rd \mu < + \infty$
Thus:
:$f \in \map {\LL^p} \mu$
Furthermore, since:
:$\size {f_n - f} \le \size {f_n} + \size f \le 2 \size g$
we have:
:$\size {f_n - f}^p \le 2^p \size g^p$
Since $2^p \size g^p$ is $\mu$-integrable:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \int \size {f_n - f}^p \rd \mu
      | r = \int \lim_{n \mathop \to \infty} \size {f_n - f}^p \rd \mu
      | c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn | r = \int 0 \rd \mu
      | c = since $f = \ds \lim_{n \mathop \to \infty} f_n$ $\mu$-almost everywhere
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Riesz's Convergence Theorem

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p \in \R$, $p \ge 1$.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n: X \to \R$ be a sequence in Lebesgue $p$-space $\map {\LL^p} \mu$.
Suppose that the pointwise limit $f := \ds \lim_{n \mathop \to \infty} f_n$ exists $\mu$-almost everywhere, and that $f \in \map {\LL^p} \mu$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\ds \lim_{n \mathop \to \infty} \norm {f - f_n}_p {{=}} 0$}}
{{item|(2):|$\ds \lim_{n \mathop \to \infty} \norm {f_n}_p {{=}} \norm f_p$}}
{{end-itemize}}
where $\norm {\, \cdot \,}_p$ denotes the $p$-seminorm.

Proof:
=== From $(1)$ to $(2)$ ===
This follows from the reverse triangle inequality:
:$\size {\norm f_p - \norm {f_n}_p} \le \norm {f - f_n}_p$
{{qed|lemma}}
Theorem: Preimage of Union under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f^{-1} \sqbrk {\bigcup_{i \mathop \in I} T_i} = \bigcup_{i \mathop \in I} f^{-1} \sqbrk {T_i}$
where:
:$\ds \bigcup_{i \mathop \in I} T_i$ denotes the union of $\family {T_i}_{i \mathop \in I}$
:$f^{-1} \sqbrk {T_i}$ denotes the preimage of $T_i$ under $f$.

Proof:
As $f$, being a mapping, is also a relation, we can apply Preimage of Union under Relation: Family of Sets:
:$\ds \RR^{-1} \sqbrk {\bigcup_{i \mathop \in I} T_i} = \bigcup_{i \mathop \in I} \RR^{-1} \sqbrk {T_i}$
where $\RR^{-1} \sqbrk {T_i}$ denotes the preimage of $T_i$ under $\RR^{-1}$.
{{qed}}
Theorem: Preimage of Union under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f^{-1} \sqbrk {\bigcup_{i \mathop \in I} T_i} = \bigcup_{i \mathop \in I} f^{-1} \sqbrk {T_i}$
where:
:$\ds \bigcup_{i \mathop \in I} T_i$ denotes the union of $\family {T_i}_{i \mathop \in I}$
:$f^{-1} \sqbrk {T_i}$ denotes the preimage of $T_i$ under $f$.

Proof:
We have that $f$ is a mapping, and so also a relation.
Thus its inverse $f^{-1}$ is also a relation.
Hence we can apply Image of Union under Relation: Family of Sets:
:$\ds \RR \sqbrk {\bigcup_{i \mathop \in I} T_i} = \bigcup_{i \mathop \in I} \RR \sqbrk {T_i}$
where $\RR \sqbrk {T_i}$ denotes the image of $T_i$ under $\RR$.
{{qed}}
Theorem: Image of Intersection under One-to-Many Relation/Family of Sets

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Then $\RR$ is a one-to-many relation {{iff}}:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}$ 
where $\family {S_i}_{i \mathop \in I}$ is ''any'' family of subsets of $S$.

Proof:
=== Sufficient Condition ===
Suppose:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} S_i} = \bigcap_{i \mathop \in I} \RR \sqbrk {S_i}$ 
where $\family {S_i}_{i \mathop \in I}$ is ''any'' family of subsets of $S$.
Then by definition of $\family {S_i}_{i \mathop \in I}$:
:$\forall i, j \in I: \RR \sqbrk {S_i \cap S_j} = \RR \sqbrk {S_i} \cap \RR \sqbrk {S_j}$
and the sufficient condition applies for Image of Intersection under One-to-Many Relation.
So $\RR$ is one-to-many.
{{qed|lemma}}
Theorem: Preimage of Intersection under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f^{-1} \sqbrk {\bigcap_{i \mathop \in I} T_i} = \bigcap_{i \mathop \in I} f^{-1} \sqbrk {T_i}$
where:
:$\ds \bigcap_{i \mathop \in I} T_i$ denotes the intersection of $\family {T_i}_{i \mathop \in I}$.
:$f^{-1} \sqbrk {T_i}$ denotes the preimage of $T_i$ under $f$.

Proof:
As $f$ is a mapping, it is by definition also a many-to-one relation.
It follows from Inverse of Many-to-One Relation is One-to-Many that its inverse $f^{-1}$ is a one-to-many relation.
Thus Image of Intersection under One-to-Many Relation: Family of Sets can be applied for $\RR = f^{-1}$:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} T_i} = \bigcap_{i \mathop \in I} \RR \sqbrk {T_i}$
where $\RR \sqbrk {T_i}$ denotes the image of $T_i$ under $\RR$.
{{Qed}}
Theorem: Preimage of Intersection under Mapping/Family of Sets

Let $S$ and $T$ be sets.
Let $\family {T_i}_{i \mathop \in I}$ be a family of subsets of $T$.
Let $f: S \to T$ be a mapping.
Then:
:$\ds f^{-1} \sqbrk {\bigcap_{i \mathop \in I} T_i} = \bigcap_{i \mathop \in I} f^{-1} \sqbrk {T_i}$
where:
:$\ds \bigcap_{i \mathop \in I} T_i$ denotes the intersection of $\family {T_i}_{i \mathop \in I}$.
:$f^{-1} \sqbrk {T_i}$ denotes the preimage of $T_i$ under $f$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = f^{-1} \sqbrk {\bigcap_{i \mathop \in I} T_i}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f x
      | o = \in
      | r = \bigcap_{i \mathop \in I} T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = \map f x
      | o = \in
      | r = T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = f^{-1} \sqbrk {T_i}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} f^{-1} \sqbrk {T_i}
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Space of Simple P-Integrable Functions is Everywhere Dense in Lebesgue Space

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p \in \R$, $p \ge 1$.
Let $\map {\LL^p} \mu$ be Lebesgue $p$-space for $\mu$.
Let $\map \EE \Sigma \cap \map {\LL^p} \mu$ be the space of $\Sigma$-simple, $p$-integrable functions.
Then $\map \EE \Sigma \cap \map {\LL^p} \mu$ is everywhere dense in $\map {\LL^p} \mu$ with respect to the seminorm topology generated by the singleton $\set {\norm {\; \cdot \;}_p }$.
That is, for all $f \in  \map {\LL^p} \mu$ and $\epsilon > 0$ there exists a $g \in \map \EE \Sigma \cap \map {\LL^p} \mu$ such that:
:$\norm {f - g}_p < \epsilon$
{{DefinitionWanted|Definition:Seminorm Topology and Definition:Locally Convex Topological Vector Space}}

Proof:
For $n \in \N$, we define $D_n : \R_{\ge 0} \to \R_{\ge 0}$ by:
$\quad \map {\Delta _n} y := \begin{cases}
\dfrac k {2^n} & : y \in \hointr {\dfrac k {2^n} } {\dfrac {k + 1} {2^n} }, k = 0, 1, \ldots, 2^{2 n} - 1 \\
0 & : y \ge 2^n
\end{cases}$
Clearly, for all $n \in \N$:
:$(1): \quad \forall y \in \R_{\ge 0} : 0 \le \map {\Delta_n} y \le y$
We also have:
:$(2): \quad \ds \forall y \in \R_{\ge 0} : \lim_{n \mathop \to \infty} \map {\Delta_n} y = y$
since:
:$\forall y \in \hointr 0 {2^n} : 0 \le y - \map {\Delta_n} y \le \dfrac 1 {2^n}$
Let:
:$\map {f_n} x := \map \sgn {\map f x} \map {\Delta_n} {\size {\map f x} }$
where:
:$\map \sgn \cdot$ denotes the signum function
:$\size {\, \cdot \,}$ denotes the absolute value.
By Measurable Function is Simple Function iff Finite Image Set:
:$f_n \in \map \EE \Sigma$
By $(2)$, for all $x \in X$:
:$\ds \lim_{n \mathop \to \infty} \map {f_n} x = \map f x$
In view of $(1)$, we have for all $x \in X$:
:$\size {\map {f_n} x} \le \size {\map f x}$
In particular, $f_n \in \map {\LL^p} \mu$.
Moreover, for all $x \in X$:
:$\size {\map {f_n} x - \map f x} \le \size {\map f x} + \size {\map {f_n} x} \le 2 \size {\map f x}$
Thus, by Lebesgue's Dominated Convergence Theorem:
:$\ds \lim_{n \mathop \to \infty} \norm {f_n - f}_p = \paren {\int \lim_{n \mathop \to \infty} \size {f_n - f}^p \rd \mu }^{1/p} = 0$
{{qed}}
Theorem: Jensen's Inequality (Measure Theory)/Convex Functions

Let $V: \hointr 0 \infty \to \hointr 0 \infty$ be a convex function.
Then for all positive measurable functions $g: X \to \R$, $g \in \map {\MM^+} \Sigma$:
:$\map V {\dfrac {\ds \int g \cdot f \rd \mu} {\ds \int f \rd \mu} } \le \dfrac {\ds \int \paren {V \circ g} \cdot f \rd \mu} {\ds\int f \rd \mu}$
where $\circ$ denotes composition, and $\cdot$ denotes pointwise multiplication.
{{explain|How to interpret if $\int f \rd \mu {{=}} 0$?}}

Proof:
{{MissingLinks}}
Let $\d \map \nu x := \dfrac {\map f x} {\ds \int \map f s \rd \map \mu s} \rd \map \mu x$ be a probability measure.
{{explain|This proof invokes a probability measure. Needs to be for a measure space. Does the proof work for both?}}
Let $\ds x_0 := \int \map g s \rd \map \nu s$.
Then by convexity there exists constants $a, b$ such that:
{{begin-eqn}}
{{eqn | l = \map V {x_0}
      | r = a x_0 + b
}}
{{eqn | q = \forall x \in \R_{\ge 0}
      | l = \map V x
      | o = \ge
      | r = a x + b
}}
{{end-eqn}}
In other words, there is a tangent line at $\tuple {x_0, V_0}$ that falls below the graph of $V$.
Therefore:
{{begin-eqn}}
{{eqn | l = \map V {\map g s}
      | o = \ge
      | r = a \map g s + b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \map V {\map g s} \rd \map \nu s
      | o = \ge
      | r = a \int \map g s \rd \map \nu s + b
      | c = Integration {{WRT|Integration}} $\map \nu s$
}}
{{eqn | r = \map V {x_0}
      | c = 
}}
{{eqn | r = \map V {\int \map g s \rd \map \nu s}
      | c = 
}}
{{end-eqn}}
{{explain|why this does what it purports to}}
Category:Jensen's Inequality
Category:Measure Theory
b02xryataenqzo5i5jcs5a5pxwumu1n