nyuuzyou/wikis huggingface dataset:
Points Defined by Adjacent Pairs of Digits of Reciprocal of 7 lie on Ellipse

== Theorem ==
Consider the digits that form the recurring part of the reciprocal of $7$:
:$\dfrac 1 7 = 0 \cdotp \dot 14285 \dot 7$
Take the digits in ordered pairs, and treat them as coordinates of a Cartesian plane.
It will be found that they all lie on an ellipse:
:
== Proof ==
:
Let the points be labelled to simplify:
:$A := \tuple {1, 4}$
:$B := \tuple {2, 8}$
:$C := \tuple {4, 2}$
:$D := \tuple {8, 5}$
:$E := \tuple {7, 1}$
:$F := \tuple {5, 7}$
Let $ABCDEF$ be considered as a hexagon.
We join the opposite points of $ABCDEF$:
:$AF: \tuple {1, 4} \to \tuple {5, 7}$
:$BC: \tuple {2, 8} \to \tuple {4, 2}$
:$BE: \tuple {2, 8} \to \tuple {7, 1}$
:$AD: \tuple {1, 4} \to \tuple {8, 5}$
:$CD: \tuple {4, 2} \to \tuple {8, 5}$
:$EF: \tuple {7, 1} \to \tuple {5, 7}$
It is to be shown that the intersections of:
:$AF$ and $BC$
:$BE$ and $AD$
:$CD$ and $EF$
all lie on the same straight line.
The result then follows from Pascal's Mystic Hexagram.
From Two-Point Form of Equation of Straight Line in Plane:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
Thus:
Evaluate the intersection of $AF$ and $BC$:
So $AF$ and $BC$ intersect at $\paren {\dfrac {43} {15}, \dfrac {27} 5}$.
Evaluate the intersection of $BE$ and $AD$:
So $BE$ and $AD$ intersect at $\paren {\dfrac 9 2, \dfrac 9 2}$.
Evaluate the intersection of $CD$ and $EF$:
So $CD$ and $EF$ intersect at $\paren {\dfrac {92} {15}, \dfrac {18} 5}$.
It remains to be shown that those points of intersection:
:$\paren {\dfrac {43} {15}, \dfrac {27} 5}$, $\paren {\dfrac 9 2, \dfrac 9 2}$, $\paren {\dfrac {92} {15}, \dfrac {18} 5}$
all lie on the same straight line.
From Two-Point Form of Equation of Straight Line in Plane:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
Thus:
It remains to demonstrate that $\paren {\dfrac 9 2, \dfrac 9 2}$ lies on this line:
Bingo.
== Sources ==
* 
* : $142,857$
Category:Ellipses
Category:7
Points are Path-Connected iff Contained in Path-Connected Set

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $x, y \in S$
Then:
:$x, y$ are path-connected points in $T$ there exists a path-connected set of $T$ containing $x$ and $y$.
== Proof ==
=== Necessary Condition ===
Let $x, y$ be path-connected points in $T$.
Let $\gamma: \closedint 0 1 \to T$ be a path from $x$ to $y$.
From Image of Path is Path-Connected Set, $\Img \gamma$ is a path-connected set of $T$ containing $x$ and $y$.
The result follows.
=== Sufficient Condition ===
Let $B$ be a path-connected set of $T$ containing $x$ and $y$.
Then there exists a path $\gamma: \closedint 0 1 \to B$ from $x$ to $y$.
Let $i_B: B \to S$ be the inclusion mapping from $B$ into $S$.
From Composite of Continuous Mappings is Continuous, $i_B \circ g: \closedint 0 1 \to T$ is continuous.
Hence $i_B \circ g$ is a path from $x$ to $y$ in $T$.
Category:Path-Connected Spaces
Points in Product Spaces are Near Open Sets

== Theorem ==
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of topological spaces, where $I$ is an arbitrary index set.
Let $X = \ds \prod_{i \mathop \in I} X_i$ be the product space of $\family {X_i}_{i \mathop \in I}$.
Let $U$ be nonempty open subset of $X$.
Let $x$ be a point in $X$.
For each point $y$ in $X$, let $\map K y = \set {i \in I : y_i \ne x_i}$.
Then there exists a point $u$ in $U$ such that $\map K u$ is finite.
== Proof ==
Let $q$ be any point in $U$.
The topology on the product space $X$ is the product topology which has the natural basis as a (synthetic) basis.
Then:
:$\exists Q \in \BB : q \in Q \subseteq U$
where $\BB$ is the natural basis for product topology on $X$.
From Natural Basis of Product Topology:
:$\ds Q = \prod_{i \mathop \in I} Q_i$ where:
::for all $i \in I : Q_i$ is open in $X_i$
::$J = \set {i \in I : Q_i \ne X_i}$ is finite
Let $u$ be the point defined by:
:$u_i = \begin {cases} q_i & i \in J \\ x_i & i \notin J \end {cases}$
By definition of $u$:
:$\forall i \in I : u_i \in Q_i$
By definition of the Cartesian product:
:$u \in Q \subseteq U$
By definition of $u$:
:$\forall i \in I: i \notin J \implies u_i = x_i$
So by Rule of Transposition:
:$\forall i \in I: u_i \ne x_i \implies i \in J$
Thus:
:$\map K u \subseteq J$ 
From Subset of Finite Set is Finite, and because $J$ is finite, $\map K u$ is also finite.
Category:Product Topology
Points of Riemannian Manifold are Contained in Geodesically Convex Geodesic Balls

== Theorem ==
Let $\struct {M, g}$ be a Riemannian manifold.
Let $\epsilon_0 \in \R_{> 0}$.
Then for all $p \in M$ there exists a closed geodesic ball or open geodesic ball centered at $p \in M$ of radius $\epsilon \le \epsilon_0$ which is also geodesically convex.
== Proof ==
== Sources ==
* : $\S 6$: Geodesics and Distance. Uniformly Normal Neighborhoods
Category:Riemannian Manifolds
Pointwise Addition is Associative

== Theorem ==
Let $S$ be a non-empty set.
Let $\mathbb F$ be one of the standard number sets: $\Z, \Q, \R$ or $\C$.
Let $f, g, h: S \to \mathbb F$ be functions.
Let $f + g: S \to \mathbb F$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition is associative.
== Proof ==
== Specific Contexts ==
This result can be applied and proved in the context of the various standard number sets:
=== Pointwise Addition on Integer-Valued Functions is Associative ===
=== Pointwise Addition on Rational-Valued Functions is Associative ===
=== Pointwise Addition on Real-Valued Functions is Associative ===
=== Pointwise Addition on Complex-Valued Functions is Associative ===
Category:Pointwise Addition
Category:Examples of Associative Operations‎
Category:Pointwise Addition is Associative
Pointwise Addition is Commutative

== Theorem ==
Let $S$ be a non-empty set.
Let $\mathbb F$ be one of the standard number sets: $\Z, \Q, \R$ or $\C$.
Let $f, g: S \to \mathbb F$ be functions.
Let $f + g: S \to \mathbb F$ denote the pointwise sum of $f$ and $g$.
Then:
:$f + g = g + f$
</onlyinclude>
That is, pointwise addition is commutative.
== Proof ==
== Specific Contexts ==
This result can be applied and proved in the context of the various standard number sets:
=== Pointwise Addition on Integer-Valued Functions is Commutative ===
=== Pointwise Addition on Rational-Valued Functions is Commutative ===
=== Pointwise Addition on Real-Valued Functions is Commutative ===
=== Pointwise Addition on Complex-Valued Functions is Commutative ===
Category:Pointwise Addition
Category:Examples of Commutative Operations
Category:Pointwise Addition is Commutative
Pointwise Addition on Complex-Valued Functions is Associative

== Theorem ==
Let $S$ be a set.
Let $f, g, h: S \to \C$ be complex-valued functions.
Let $f + g: S \to \C$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition on complex-valued functions is associative.
== Proof ==
Category:Pointwise Addition is Associative
Category:Complex Addition
Pointwise Addition on Complex-Valued Functions is Commutative

== Definition ==
Let $S$ be a set.
Let $f, g: S \to \C$ be complex-valued functions.
Let $f + g: S \to \C$ denote the pointwise sum of $f$ and $g$.
Then:
:$f + g = g + f$
That is, pointwise addition of complex-valued functions is commutative.
== Proof ==
Category:Pointwise Addition is Commutative
Category:Complex Addition
Pointwise Addition on Continuous Real Functions forms Group

== Theorem ==
Let $C$ be the set of all continuous real functions on the set of real numbers $\R$.
Let $f, g \in C$.
Let $f + g$ be the pointwise sum of $f$ and $g$:
:$\forall x \in R: \map {\paren {f + g} } x = \map f x + \map g x$
Then $\struct {C, +}$, the algebraic structure on $C$ induced by $+$, forms a group.
== Proof ==
Taking the group axioms in turn:
=== ===
From the Sum Rule for Continuous Real Functions, if $f$ and $g$ are continuous real functions then so is $f + g$.
Thus closure is demonstrated.
=== ===
Pointwise Addition is Associative.
=== ===
The constant function $f_0$ defined as:
:$\forall x \in \R: \map {f_0} x = 0$
fulfils the role of the Identity:
:$\forall x \in \R: \map {f_0} x + \map f x = 0 + \map f x = \map f x = \map f x + 0 = \map f x = \map {f_0} x$
Note that $f_0 \in C$ as the Constant Function is Uniformly Continuous, and hence continuous.
=== ===
From the Multiple Rule for Continuous Real Functions, if $\map f x$ is continuous then so is $\map g x$ where:
:$\forall x \in \R: \map g x = -\map f x$.
Then we note that:
:$\forall x \in \R: \map f x + \paren {-\map f x} = 0 = \paren {-\map f x} + \map f x$
So every element has an inverse.
All the group axioms are satisfied, hence the result.
== Sources ==
* : Chapter $\text{II}$: Groups: Exercise $\text{U}$
Category:Real Analysis
Category:Examples of Groups
Category:Pointwise Addition
Pointwise Addition on Continuous Real Functions on Closed Unit Interval forms Group

== Theorem ==
Let $J \subseteq \R$ denote the closed unit interval $\closedint 0 1$.
Let $\map {\mathscr C} J$ denote the set of all continuous real functions from $J$ to $\R$.
Let $\R^J$ denote the set of all mappings from $J$ to $\R$.
Let $\struct {\R^J, +}$ denote the algebraic structure on $\R^J$ induced by addition:
:$\forall f, g \in \R^J: \map {\paren {f + g} } x = \map f x + \map g x$
Then $\struct {\map {\mathscr C} J, +}$ is a subgroup of $\struct {\R^J, +}$.
== Proof ==
Taking the group axioms in turn:
=== ===
From the Sum Rule for Continuous Real Functions, if $f$ and $g$ are continuous real functions then so is $f + g$.
Thus closure is demonstrated.
=== ===
Pointwise Addition is Associative.
=== ===
The constant function $f_0$ defined as:
:$\forall x \in \R: \map {f_0} x = 0$
fulfils the role of the Identity:
:$\forall x \in \R: \map {f_0} x + \map f x = 0 + \map f x = \map f x = \map f x + 0 = \map f x = \map {f_0} x$
From Constant Real Function is Continuous $f_0$ is continuous.
Hence $f_0 \in \mathscr C$.
=== ===
From the Multiple Rule for Continuous Real Functions, if $\map f x$ is continuous then so is $\map g x$ where:
:$\forall x \in \R: \map g x = -\map f x$.
Then we note that:
:$\forall x \in \R: \map f x + \paren {-\map f x} = 0 = \paren {-\map f x} + \map f x$
So every element has an inverse.
All the group axioms are satisfied, hence the result.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Exercise $13.17 \ \text {(a)}$
Category:Examples of Groups
Category:Pointwise Addition
Category:Continuous Real Functions
Pointwise Addition on Differentiable Real Functions on Closed Unit Interval forms Group

== Theorem ==
Let $J \subseteq \R$ denote the closed unit interval $\closedint 0 1$.
Let $\map {\mathscr D} J$ denote the set of all differentiable real functions from $J$ to $\R$.
Let $\R^J$ denote the set of all mappings from $J$ to $\R$.
Let $\struct {\R^J, +}$ denote the algebraic structure on $\R^J$ induced by addition:
:$\forall f, g \in \R^J: \map {\paren {f + g} } x = \map f x + \map g x$
Then $\struct {\map {\mathscr D} J, +}$ is a subgroup of $\struct {\R^J, +}$.
== Proof ==
Taking the group axioms in turn:
=== ===
From the Sum Rule for Derivatives, if $f$ and $g$ are differentiable real functions then so is $f + g$.
Thus closure is demonstrated.
=== ===
Pointwise Addition is Associative.
=== ===
The constant function $f_0$ defined as:
:$\forall x \in \R: \map {f_0} x = 0$
fulfils the role of the Identity:
:$\forall x \in \R: \map {f_0} x + \map f x = 0 + \map f x = \map f x = \map f x + 0 = \map f x = \map {f_0} x$
From Derivative of Constant $f_0$ is differentiable.
Hence $f_0 \in \mathscr D$.
=== ===
From the Derivative of Constant Multiple, if $\map f x$ is continuous then so is $\map g x$ where:
:$\forall x \in \R: \map g x = -\map f x$.
Then we note that:
:$\forall x \in \R: \map f x + \paren {-\map f x} = 0 = \paren {-\map f x} + \map f x$
So every element has an inverse.
All the group axioms are satisfied, hence the result.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Exercise $13.17 \ \text {(a)}$
Category:Examples of Groups
Category:Pointwise Addition
Category:Differentiable Real Functions
Pointwise Addition on Integer-Valued Functions is Associative

== Theorem ==
Let $S$ be a set.
Let $f, g, h: S \to \Z$ be integer-valued functions.
Let $f + g: S \to \Z$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition on integer-valued functions is associative.
== Proof ==
Category:Pointwise Addition is Associative
Category:Integer Addition
Pointwise Addition on Integer-Valued Functions is Commutative

== Definition ==
Let $S$ be a set.
Let $f, g: S \to \Z$ be integer-valued functions.
Let $f + g: S \to \Z$ denote the pointwise sum of $f$ and $g$.
Then:
:$f + g = g + f$
That is, pointwise addition of integer-valued functions is commutative.
== Proof ==
Category:Pointwise Addition is Commutative
Category:Integer Addition
Pointwise Addition on Rational-Valued Functions is Associative

== Theorem ==
Let $S$ be a set.
Let $f, g, h: S \to \Q$ be rational-valued functions.
Let $f + g: S \to \Q$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition on rational-valued functions is associative.
== Proof ==
Category:Pointwise Addition is Associative
Category:Rational Addition
Pointwise Addition on Rational-Valued Functions is Commutative

== Definition ==
Let $S$ be a set.
Let $f, g: S \to \Q$ be rational-valued functions.
Let $f + g: S \to \Q$ denote the pointwise sum of $f$ and $g$.
Then:
:$f + g = g + f$
That is, pointwise addition of rational-valued functions is commutative.
== Proof ==
Category:Rational Addition
Category:Pointwise Addition is Commutative
Pointwise Addition on Real-Valued Functions is Associative

== Theorem ==
Let $S$ be a set.
Let $f, g, h: S \to \R$ be real-valued functions.
Let $f + g: S \to \R$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition on real-valued functions is associative.
== Proof ==
Category:Pointwise Addition is Associative
Category:Real Addition
Pointwise Addition on Real-Valued Functions is Commutative

== Definition ==
Let $S$ be a set.
Let $f, g: S \to \R$ be real-valued functions.
Let $f + g: S \to \R$ denote the pointwise sum of $f$ and $g$.
Then:
:$f + g = g + f$
That is, pointwise addition of real-valued functions is commutative.
== Proof ==
Category:Real Addition
Category:Pointwise Addition is Commutative
Pointwise Addition on Space of Real-Valued Measurable Functions Identified by A.E. Equality is Well-Defined

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\mathcal M} {X, \Sigma, \R}$ be the set of real-valued $\Sigma$-measurable functions on $X$. 
Let $\sim$ be the almost-everywhere equality relation on $\map {\mathcal M} {X, \Sigma, \R}$.
Let $\map {\mathcal M} {X, \Sigma, \R}/\sim$ be the space of real-valued measurable functions identified by $\mu$-A.E. equality. 
Then pointwise addition on $\map {\mathcal M} {X, \Sigma, \R}/\sim$ is well-defined.
== Proof ==
Let $E_1, E_2 \in \map {\mathcal M} {X, \Sigma, \R}/\sim$.
First, we show that if $E_1 = \eqclass f \sim$ and $E_2 = \eqclass g \sim$, that $\eqclass {f + g} \sim$ is well-understood. 
This follows from Pointwise Sum of Measurable Functions is Measurable.
We now need to show that $E_1 + E_2$ is independent of the choice of representative for $E_1$ and $E_2$.
Suppose that: 
:$\eqclass f \sim = \eqclass F \sim = E_1$
and:
:$\eqclass g \sim = \eqclass G \sim = E_2$
From Equivalence Class Equivalent Statements, we have: 
:$f \sim F$
and:
:$g \sim G$
From Pointwise Addition preserves A.E. Equality, we have: 
:$f + g \sim F + G$
That is, from Equivalence Class Equivalent Statements:
:$\eqclass {f + g} \sim = \eqclass {F + G} \sim$ 
which is what we aimed to show.
Category:Space of Real-Valued Measurable Functions Identified by A.E. Equality
Pointwise Addition preserves A.E. Equality

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g, F, G : X \to \overline \R$ be functions with: 
:$f = F$ $\mu$-almost everywhere
and:
:$g = G$ $\mu$-almost everywhere
and the pointwise sums $f + g$ and $F + G$ well-defined.
Then: 
:$f + g = F + G$ $\mu$-almost everywhere.
== Proof ==
Since:
:$f = F$ $\mu$-almost everywhere
there exists a $\mu$-null set $N_1 \subseteq X$ such that: 
:if $x \in X$ has $\map f x \ne \map F x$ then $x \in N_1$.
Since: 
:$g = G$ $\mu$-almost everywhere
there exists a $\mu$-null set $N_2 \subseteq X$ such that: 
:if $x \in X$ has $\map G x \ne \map G x$ then $x \in N_2$ 
Note that if $x \in X$ is such that: 
:$\map f x = \map F x$
and:
:$\map g x = \map G x$ 
then: 
:$\map f x + \map g x = \map F x + \map G x$
whenever this sum is well-defined.
By the Rule of Transposition, we therefore have: 
:if $x \in X$ has $\map f x + \map g x \ne \map F x + \map G x$ then $\map f x \ne \map F x$ or $\map g x \ne \map G x$.
That is, whenever $x \in X$ has $\map f x + \map g x \ne \map F x + \map G x$, we have: 
:$x \in N_1 \cup N_2$
From Null Sets Closed under Countable Union, we have: 
:$N_1 \cup N_2$ is $\mu$-null.
So:
:$f + g = F + G$ $\mu$-almost everywhere.
Category:Almost-Everywhere Equality Relation
Pointwise Convergence Implies Convergence in Measure on Finite Measure Space

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a finite measure space.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n : X \to \R$ be a sequence of measurable functions.
Also, let $f: X \to \R$ be a measurable function.
Suppose that $f$ is the pointwise limit of the $f_n$ $\mu$-almost everywhere.
Then $f_n$ converges in measure to $f$ (in $\mu$).
That is:
:$\ds \lim_{n \mathop \to \infty} \map {f_n} x \stackrel {a.e.} {=} \map f x \implies \operatorname {\mu-\!\lim\,} \limits_{n \mathop \to \infty} f_n = f$
== Proof ==
Since $\sequence {f_n}_{n \mathop \in \N}$ converges almost everywhere, we have: 
:$\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x}$ is a $\mu$-null set.
We aim to deduce that: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } = 0$
for each $\epsilon > 0$. 
Let $\epsilon > 0$.
For each $n \in \N$, define: 
:$A_n = \set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon}$
Also define: 
:$\ds B_n = \bigcup_{k \mathop = n}^\infty A_n$
for each $n \in \N$. 
Then $\sequence {B_n}_{n \mathop \in \N}$ is a decreasing sequence. 
Since $\mu$ is finite, $\map \mu {B_1} < \infty$.
So, from Measure of Limit of Decreasing Sequence of Measurable Sets, we have: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty B_n} = \lim_{n \mathop \to \infty} \map \mu {B_n}$
Note that if:
:$\ds x \in \bigcap_{n \mathop = 1}^\infty B_n$
We have: 
:$\size {\map {f_n} x - \map f x} > \epsilon$ for each $n \in \N$.
So:
:$\sequence {\map {f_n} x}_{n \mathop \in \N}$ does not converge to $\map f x$. 
So:
:$\ds \bigcap_{n \mathop = 1}^\infty B_n \subseteq \set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x}$
So, from Null Sets Closed under Subset, we have: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty B_n} = 0$
and so:
:$\ds \lim_{n \mathop \to \infty} \map \mu {B_n} = 0$ 
That is:
:$\ds \lim_{n \mathop \to \infty} \map \mu {\bigcup_{k \mathop = n}^\infty A_k} = 0$
From Set is Subset of Union, we have: 
:$\ds A_n \subseteq \bigcup_{k \mathop = n}^\infty A_k$ 
So from Measure is Monotone, we have: 
:$\ds 0 \le \map \mu {A_n} \le \map \mu {B_n}$ for each $n \in \N$.
Then, from the Squeeze Theorem for Real Sequences, we have: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {A_n} = 0$
That is: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } = 0$
Since $\epsilon > 0$ was arbitrary, we have:
:$f_n \stackrel \mu \longrightarrow f$
== Also see ==
* Pointwise Convergence may not imply Convergence in Measure shows that if $\mu$ is not a finite measure, the implication may not hold
== Sources ==
* : $16.4 \ \text{(ii)}$
Category:Convergence in Measure
Pointwise Convergence implies Convergence Almost Everywhere

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $f : X \to \R$ be a $\Sigma$-measurable function.
For each $n \mathop \in \N$, let $f_n : X \to \R$ be a $\Sigma$-measurable function.
Then:
:if $\sequence {f_n}_{n \mathop \in \N}$ converges pointwise to $f$, it converges almost everywhere to $f$. 
== Proof ==
If $\sequence {f_n}_{n \mathop \in \N}$ converges pointwise to $f$, then: 
:$\sequence {\map {f_n} x}_{n \mathop \in \N}$ converges to $\map f x$ for each $x \in X$. 
So:
:$\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x} = \O$
From Measure of Empty Set is Zero, we have: 
:$\map \mu \O = 0$
So:
:$\map \mu {\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x} } = 0$
So:
:$\sequence {f_n}_{n \mathop \in \N}$ converges almost everywhere to $f$.
Category:Convergence Almost Everywhere
Pointwise Convergent Bounded Sequence in Lebesgue Space Converges in Norm

== Theorem ==
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 \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:
== Sources ==
* : $12.9$
Category:Lebesgue Spaces
Pointwise Difference is Pointwise Addition with Negation

== Theorem ==
Let $S$ be a set.
Let $\R$ denote the real number line.
Let $f, g :S \to \R$ be real-valued functions.
Let $f - g$ denote the pointwise difference of $f$ and $g$, that is, $f - g$ is the mapping defined by:
:$\forall s \in S : \map {\paren{f - g} } s = \map f s - \map g s$
Then:
:$f - g = f + \paren{-g}$
where:
:$-g$ denotes the pointwise negation of $g$
:$f + \paren{-g}$ denotes the pointwise addition of $f$ and $-g$
== Proof ==
We have:
By definition of equality of mappings:
:$f - g = f + \paren{-g}$
Category:Real-Valued Functions
Pointwise Difference of Measurable Functions is Measurable

== Theorem ==
Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Assume that the pointwise difference $f - g: X \to \overline \R$ is well-defined.
Then $f - g$ is a $\Sigma$-measurable function.
== Proof ==
We have the apparent identity:
:$f - g = f + \paren {-g}$
By Negative of Measurable Function is Measurable, $-g$ is a measurable function.
Hence so is $f - g$, by Pointwise Sum of Measurable Functions is Measurable.
== Sources ==
* : $8.10$
Category:Measurable Functions
Pointwise Difference of Simple Functions is Simple Function

== Theorem ==
Let $\struct {X, \Sigma}$ be a measurable space.
Let $f,g : X \to \R$ be simple functions.
Let $f - g: X \to \R$ be the pointwise difference of $f$ and $g$:
:$\forall x \in X: \map {\paren {f - g} } x := \map f x - \map g x$
Then $f - g$ is also a simple function.
== Proof ==
By Scalar Multiple of Simple Function is Simple Function, $-g = -1 \cdot g$ is a simple function.
By Pointwise Sum of Simple Functions is Simple Function, so is $f - g$.
Category:Simple Functions