avewright/proofwiki-math huggingface dataset:
Theorem: Pointwise Addition on Complex-Valued Functions is Associative

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}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f + g} + h} } x
      | r = \paren {\map f x + \map g x} + \map h x
      | c = {{Defof|Pointwise Addition of Complex-Valued Functions}}
}}
{{eqn | r = \map f x + \paren {\map g x + \map h x}
      | c = Complex Addition is Associative
}}
{{eqn | r = \map {\paren {f + \paren {g + h} } } x
      | c = {{Defof|Pointwise Addition of Complex-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Addition is Associative
Category:Complex Addition
bjnnobeii5ainc2742y0qpbj94e85y2
Theorem: Pointwise Addition is Commutative

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:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {f + g} } x
      | r = \map f x + \map g x
      | c = {{Defof|Pointwise Addition}}
}}
{{eqn | r = \map g x + \map f x
      | c = Commutative Law of Addition
}}
{{eqn | r = \map {\paren {g + f} } x
      | c = {{Defof|Pointwise Addition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pointwise Multiplication is Associative

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 \times g: S \to \mathbb F$ denote the pointwise product of $f$ and $g$.
Then:
:$\paren {f \times g} \times h = f \times \paren {g \times h}$
That is, pointwise multiplication is associative.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f \times g} \times h} } x
      | r = \paren {\map f x \times \map g x} \times \map h x
      | c = {{Defof|Pointwise Multiplication}}
}}
{{eqn | r = \map f x \times \paren {\map g x \times \map h x}
      | c = Associative Law of Multiplication
}}
{{eqn | r = \map {\paren {f \times \paren {g \times h} } } x
      | c = {{Defof|Pointwise Multiplication}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pointwise Multiplication is Commutative

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 \times g: S \to \mathbb F$ denote the pointwise product of $f$ and $g$.
Then:
:$f \times g = g \times f$
That is, pointwise multiplication is commutative.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {f \times g} } x
      | r = \map f x \times \map g x
      | c = {{Defof|Pointwise Multiplication}}
}}
{{eqn | r = \map g x \times \map f x
      | c = Commutative Law of Multiplication
}}
{{eqn | r = \map {\paren {g \times f} } x
      | c = {{Defof|Pointwise Multiplication}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pointwise Addition on Integer-Valued Functions is Associative

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}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f + g} + h} } x
      | r = \paren {\map f x + \map g x} + \map h x
      | c = {{Defof|Pointwise Addition of Integer-Valued Functions}}
}}
{{eqn | r = \map f x + \paren {\map g x + \map h x}
      | c = Integer Addition is Associative
}}
{{eqn | r = \map {\paren {f + \paren {g + h} } } x
      | c = {{Defof|Pointwise Addition of Integer-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Addition is Associative
Category:Integer Addition
c2plqkdjxw5jb5a15lexngc2pbms92g
Theorem: Pointwise Addition on Rational-Valued Functions is Associative

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}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f + g} + h} } x
      | r = \paren {\map f x + \map g x} + \map h x
      | c = {{Defof|Pointwise Addition of Rational-Valued Functions}}
}}
{{eqn | r = \map f x + \paren {\map g x + \map h x}
      | c = Rational Addition is Associative
}}
{{eqn | r = \map {\paren {f + \paren {g + h} } } x
      | c = {{Defof|Pointwise Addition of Rational-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Addition is Associative
Category:Rational Addition
3kqfplr90igadu7pf4bky1zop7duc5n
Theorem: Pointwise Multiplication on Integer-Valued Functions is Associative

Let $f, g, h: S \to \Z$ be integer-valued functions.
Let $f \times g: S \to \Z$ denote the pointwise product of $f$ and $g$.
Then:
:$\paren {f \times g} \times h = f \times \paren {g \times h}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f \times g} \times h} } x
      | r = \paren {\map f x \times \map g x} \times \map h x
      | c = {{Defof|Pointwise Multiplication of Integer-Valued Functions}}
}}
{{eqn | r = \map f x \times \paren {\map g x \times \map h x}
      | c = Integer Multiplication is Associative
}}
{{eqn | r = \map {\paren {f \times \paren {g \times h} } } x
      | c = {{Defof|Pointwise Multiplication of Integer-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Multiplication is Associative
Category:Integer Multiplication
64bmur3qa01sutp8mnpkgpmoc0w8y0l
Theorem: Pointwise Multiplication on Complex-Valued Functions is Associative

Let $f, g, h: S \to \C$ be complex-valued functions.
Let $f \times g: S \to \C$ denote the pointwise product of $f$ and $g$.
Then:
:$\paren {f \times g} \times h = f \times \paren {g \times h}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f \times g} \times h} } x
      | r = \paren {\map f x \times \map g x} \times \map h c
      | c = {{Defof|Pointwise Multiplication of Complex-Valued Functions}}
}}
{{eqn | r = \map f x \times \paren {\map g x \times \map h x}
      | c = Complex Multiplication is Associative
}}
{{eqn | r = \map {\paren {f \times \paren {g \times h} } } x
      | c = {{Defof|Pointwise Multiplication of Complex-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Multiplication is Associative
Category:Complex Multiplication
is98dl4isa8ns0dom256ni3m09uk6do
Theorem: Pointwise Multiplication on Real-Valued Functions is Associative

Let $f, g, h: S \to \R$ be real-valued functions.
Let $f \times g: S \to \R$ denote the pointwise product of $f$ and $g$.
Then:
:$\paren {f \times g} \times h = f \times \paren {g \times h}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f \times g} \times h} } x
      | r = \paren {\map f x \times \map g x} \times \map h x
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{eqn | r = \map f x \times \paren {\map g x \times \map h x}
      | c = Real Multiplication is Associative
}}
{{eqn | r = \map {\paren {f \times \paren {g \times h} } } x
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Multiplication is Associative
Category:Real Multiplication
n23e3gw9jbaiqwry1k75brfcu5p5hzo
Theorem: Pointwise Multiplication on Rational-Valued Functions is Associative

Let $f, g, h: S \to \Q$ be rational-valued functions.
Let $f \times g: S \to \Q$ denote the pointwise product of $f$ and $g$.
Then:
:$\paren {f \times g} \times h = f \times \paren {g \times h}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f \times g} \times h} } x
      | r = \paren {\map f x \times \map g x} \times \map h x
      | c = {{Defof|Pointwise Multiplication of Rational-Valued Functions}}
}}
{{eqn | r = \map f x \times \paren {\map g x \times \map h x}
      | c = Rational Multiplication is Associative
}}
{{eqn | r = \map {\paren {f \times \paren {g \times h} } } x
      | c = {{Defof|Pointwise Multiplication of Rational-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Multiplication is Associative
Category:Rational Multiplication
dv4vuctquxzmopkm30a6jepcvggazkx
Theorem: Set Equation: Intersection

Let $A$ and $B$ be sets.
Consider the set equation:
:$A \cap X = B$
The solution set of this is:
:$\O$ if $B \nsubseteq A$
:$\set {B \cup Y: A \nsubseteq Y}$ otherwise.

Proof:
{{ProofWanted}}
Category:Set Theory
Category:Set Intersection
p9k3ot62zxrq1wcpmbaq5deehrvs41t
Theorem: Non-Abelian Group has Order Greater than 4

Let $\struct {G, \circ}$ be a non-abelian group.
Then the order of $\struct {G, \circ}$ is greater than $4$.

Proof:
Let $\left({G, \circ}\right)$ be a non-abelian group whose identity is $e$.
For a group $\left({G, \circ}\right)$ to be non-abelian, we require:
: $\exists x, y \in G: x \circ y \ne y \circ x$
Suppose $x \circ y \in \left\{ {x, y, e}\right\}$.
: $x \circ y = e \implies y \circ x = e$
and $\left({G, \circ}\right)$ is abelian.
{{WLOG}}, suppose $x \circ y = x$.
{{begin-eqn}}
{{eqn | l = x \circ y = x
      | o = \implies
      | r = y = e
      | c = 
}}
{{eqn | o = \implies
      | r = y \circ x = x
      | c = 
}}
{{eqn | o = \implies
      | r = x \circ y = y \circ x
      | c = 
}}
{{end-eqn}}
and again, $\left({G, \circ}\right)$ is abelian.
Similarly for $x \circ y = y$.
Again, the same applies if $y \circ x \in \left\{ {x, y, e}\right\}$.
So, if $x \circ y \ne y \circ x$, then;
: $x \circ y$ and $y \circ x$ must be different elements
: $x \circ y$ and $y \circ x$ must both different from $e, x$ and $y$.
Thus, in a non-abelian group, there needs to be at least $5$ elements:
:$e, x, y, x \circ y, y \circ x$
{{qed}}
Theorem: Non-Abelian Group has Order Greater than 4

Let $\struct {G, \circ}$ be a non-abelian group.
Then the order of $\struct {G, \circ}$ is greater than $4$.

Proof:
It follows from Trivial Group is Cyclic Group and Prime Group is Cyclic that groups of order less than $4$ are cyclic.
Therefore, by Cyclic Group is Abelian, all groups of order less than $4$ are abelian.
Let $G$ have order $4$.
From Order of Element Divides Order of Finite Group, every element of $G$ has order that divides $4$.
Therefore any element of $G$ has order $1$, $2$ or $4$.
Let $g \in G$ have order $4$.
Then $G$ is generated by $g$.
Therefore $G$ is cyclic, and therefore abelian by Cyclic Group is Abelian.
Let $G$ be such that it has no element of order $4$.
From Identity is Only Group Element of Order 1, all the elements apart from its identity must have order $2$.
That is, $G$ is a Boolean group.
By Boolean Group is Abelian, $G$ is abelian.
The result follows.
{{qed}}
Theorem: Bayes' Theorem/General Result

Let $\set {B_1, B_2, \ldots}$ be a partition of the event space $\Sigma$.
Then, for any $B_i$ in the partition:
:$\condprob {B_i} A = \dfrac {\condprob A {B_i} \map \Pr {B_i} } {\map \Pr A} = \dfrac {\condprob A {B_i} \map \Pr {B_i} } {\sum_j \condprob A {B_j} \map \Pr {B_j} }$
where $\ds \sum_j$ denotes the sum over $j$.

Proof:
Follows directly from the Total Probability Theorem:
:$\ds \map \Pr A = \sum_i \condprob A {B_i} \map \Pr {B_i}$
and Bayes' Theorem:
:$\condprob {B_i} A = \dfrac {\condprob A {B_i} \map \Pr {B_i} } {\map \Pr A}$
{{qed}}
Theorem: Supremum is Coproduct in Order Category

Let $\mathbf P$ be an order category with ordering $\preceq$.
Let $p, q \in P_0$, and suppose they have some supremum $r = \sup \left\{{p, q}\right\}$.
Then $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.

Proof:
Let $\mathbf P^{\text{op}}$ be the dual category of $\mathbf P$.
From Dual of Order Category, it is the order category corresponding to the dual ordering $\succeq$.
From Dual Pairs (Order Theory), it follows that in $\mathbf P^{\text{op}}$:
:$r = \inf \left\{{p, q}\right\}$
where $\inf$ denotes infimum.
By Infimum is Product in Order Category, $r$ is the product of $p$ and $q$ in $\mathbf P^{\text{op}}$.
By Dual Pairs (Category Theory), $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.
{{qed}}
Theorem: Smooth Homotopy is an Equivalence Relation

Let $X$ and $Y$ be smooth manifolds.
Let $K \subseteq X$ be a (possibly empty) subset of $X$.
Let $\map {\CC^\infty} {X, Y}$ be the set of all smooth mappings from $X$ to $Y$.
Define a relation $\sim$ on $\map \CC {X, Y}$ by $f \sim g$ if $f$ and $g$ are smoothly homotopic relative to $K$.
Then $\sim$ is an equivalence relation.

Proof:
We examine each condition for equivalence.
Theorem: Real Function is Continuous at Isolated Point

Let $A \subseteq \R$ be any subset of the real numbers.
Let $f: A \to \R$ be a real function.
Let $x \in A$ be an isolated point of $A$.
Then $f$ is continuous at $x$.

Proof:
By definition of isolation point:
:$\exists \delta \in \R_{> 0}: \openint {x - \delta} {x + \delta} \cap A = \set x$
Pick any $\epsilon > 0$.
We have that for any $z \in \openint {x - \delta} {x + \delta} \cap A = \set x$:
:$\size {\map f z - \map f x} = \size {\map f x - \map f x} = 0 < \epsilon$.
This satisfies the condition of continuity at $x$,
and the limit in this case is trivially equal to $\map f x$.
{{qed}}
Category:Continuity
Category:Real Functions
d2fk3sfbiu72cv0yiqghjrolfvg95m7
Theorem: Metric Space Continuity by Epsilon-Delta

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping from $A_1$ to $A_2$.
Let $a \in A_1$ be a point in $A_1$.
Then the following definitions of continuity of $f$ at $a$ with respect to $d_1$ and $d_2$ are equivalent:

Proof:
=== Definition by Limits implies $\epsilon$-$\delta$ Definition ===
Suppose that $f$ is $\tuple {d_1, d_2}$-continuous at $a$ in the sense that:
:$(1): \quad$ The limit of $\map f x$ as $x \to a$ exists
:$(2): \quad \ds \lim_{x \mathop \to a} \map f x = \map f a$
Let $\ds \lim_{x \mathop \to a} \map f x$.
Then by the $\epsilon$-$\delta$ definition of limit:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: 0 < \map {d_1} {x, a} < \delta \implies \map {d_2} {\map f x, L} < \epsilon$
By $(2)$: 
:$\ds \lim_{x \mathop \to a} \map f x = \map f a$
that is:
:$\map f a = L$
Then:
:$0 = \map {d_1} {a, a}$
and so:
:$\map {d_2} {\map f a, L} = 0 < \epsilon$
Thus the definition by limits implies the $\epsilon$-$\delta$ definition.
{{qed|lemma}}
Theorem: Equalizer is Monomorphism

Let $\mathbf C$ be a metacategory.
Let $e: E \to C$ be the equalizer of two morphisms $f, g: C \to D$.
Then $e$ is a monomorphism.

Proof:
Suppose that for morphisms $x,y: Z \to E$, it holds that:
:$e \circ y = e \circ x$
Putting $z = e \circ x$, the following commutative diagram applies:
$\quad\quad \begin{xy}\xymatrix{
E
\ar[r]^*{e} 
&
C
\ar[r]<2pt>^*{f}
\ar[r]<-2pt>_*{g} 
&
D 
\\
Z
\ar[u]<2pt>^*{x}
\ar[u]<-2pt>_*{y}
\ar[ur]_*{z}
}\end{xy}$
It follows that $f \circ z = g \circ z$.
Since $e$ is an equalizer, there thus exists a unique $u: Z \to E$ with:
:$z = e \circ u$
Hence $x = u = y$, and it follows that $e$ is a monomorphism.
{{qed}}
Theorem: Metric Space Continuity by Open Ball

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $f: A_1 \to A_2$ be a mapping from $A_1$ to $A_2$.
Let $a \in A_1$ be a point in $A_1$.
{{TFAE|def = Continuous at Point of Metric Space|view = continuity of $f$ at $a$ with respect to $d_1$ and $d_2$}}

Proof:
=== $\epsilon$-$\delta$ Definition implies $\epsilon$-Ball Definition ===
Suppose that $f$ is $\tuple {d_1, d_2}$-continuous at $a$ in the sense that:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall x \in A_1: \map {d_1} {x, a} < \delta \implies \map {d_2} {\map f x, \map f a} < \epsilon$
where $\R_{>0}$ denotes the set of all strictly positive real numbers.
Let $\epsilon \in \R_{>0}$ be arbitrary.
Let $\delta$ be such that:
:$\forall x \in A_1: \map {d_1} {x, a} < \delta \implies \map {d_2} {\map f x, \map f a} < \epsilon$
as is known to exist by hypothesis.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = f \sqbrk {\map {B_\delta} {a; d_1} }
      | c =
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \map {B_\delta} {a; d_1}
      | l = y
      | r = \map f x
      | c = {{Defof|Image of Subset under Mapping|index = 1}}
}}
{{eqn | ll= \leadsto
      | l = \map {d_1} {x, a}
      | o = <
      | r = \delta
      | c = {{Defof|Open Ball}}
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {\map f x, \map f a}
      | o = <
      | r = \epsilon
      | c = by hypothesis
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {y, \map f a}
      | o = <
      | r = \epsilon
      | c = as $y = \map f x$
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \map {B_\epsilon} {\map f a; d_2}
      | c = {{Defof|Open Ball}}
}}
{{eqn | ll= \leadsto
      | l = f \sqbrk {\map {B_\delta} {a; d_1} }
      | o = \subseteq
      | r = \map {B_\epsilon} {\map f a; d_2}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
As $\epsilon$ is arbitrary, it follows that:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: f \sqbrk {\map {B_\delta} {a; d_1} } \subseteq \map {B_\epsilon} {\map f a; d_2}$
{{qed|lemma}}
Theorem: Mapping from Standard Discrete Metric on Real Number Line is Continuous

Let $\R$ be the real number line.
Let $\struct {\R, d_1}$ be the metric space such that $d_1$ be the Euclidean metric on $\R$.
Let $\struct {\R, d_2}$ be the metric space such that $d_2$ be the standard discrete metric on $\R$.
Let $f: \tuple {\R, d_2} \to \tuple {\R, d_1}$ be a real function.
Then $f$ is $\tuple {d_2, d_1}$-continuous on $\R$.

Proof:
Let $\epsilon \in \R: \epsilon > 0$.
Let $\delta = 1$.
Let $x \in \R$.
Let $y \in \R$ such that $\map {d_2} {x, y} < \delta$.
That is, $\map {d_2} {x, y} < 1$.
By the definition of the standard discrete metric on $\R$, that would mean that $\map {d_2} {x, y} = 0$ and so $x = y$.
Thus $\map f x = \map f y$.
By definition of a metric, that means:
:$\map {d_1} {\map f x, \map f y} = 0 < \epsilon$
Thus the conditions for $\tuple {d_2, d_1}$-continuity at a point are fulfilled.
This is true for all $x \in \R$.
So by definition $f$ is $\tuple {d_2, d_1}$-continuous on $\R$.
{{qed}}
Theorem: Properties of Affine Spaces

Let $\EE$ be an affine space with difference space $V$.
Let $0$ denote the zero element of $V$.
Then the following hold for all $p,q,r \in \EE$ and all $u, v \in V$:
:$(1): \quad p - p = 0$
:$(2): \quad p + 0 = p$
:$(3): \quad p + u = p + v \iff u = v$
:$(4): \quad q - p = r - p \iff q = r$

Proof:
=== $(1): \quad p - p = 0$ ===
We have:
{{begin-eqn}}
{{eqn | l = \paren {p - p} + \paren {q - p}
      | r = \paren {p + \paren {q - p} } - p
}}
{{eqn | r = q - p
}}
{{end-eqn}}
From Zero Element is Unique:
:$p - p = 0$
{{qed|lemma}}
Theorem: Surjection from Natural Numbers iff Right Inverse

Let $S$ be a set.
Let $f: \N \to S$ be a mapping, where $\N$ denotes the set of natural numbers.
Then $f$ is a surjection {{iff}} $f$ admits a right inverse.

Proof:
=== Necessary Condition ===
Suppose that $g: S \to \N$ is a right inverse of $f$.
That is, let $f \circ g = I_S$, the identity mapping on $S$.
We have that $I_S$ is a surjection.
By Surjection if Composite is Surjection, it follows that $f$ is a surjection.
{{qed|lemma}}
Theorem: Sum of Squared Deviations from Mean

Let $S = \set {x_1, x_2, \ldots, x_n}$ be a set of real numbers.
Let $\overline x$ denote the arithmetic mean of $S$.
Then: 
:$\ds \sum_{i \mathop = 1}^n \paren {x_i - \overline x}^2 = \sum_{i \mathop = 1}^n \paren { {x_i}^2 - {\overline x}^2}$

Proof:
For brevity, let us write $\ds \sum$ for $\ds \sum_{i \mathop = 1}^n$.
Then:
{{begin-eqn}}
{{eqn | l = \sum \paren {x_i - \overline x}^2
      | r = \sum \paren {x_i - \overline x} \paren {x_i - \overline x}
}}
{{eqn | r = \sum x_i \paren {x_i - \overline x} - \overline x \sum \paren {x_i - \overline x}
      | c = Summation is Linear
}}
{{eqn | r = \sum x_i \paren {x_i - \overline x} - 0
      | c = Sum of Deviations from Mean
}}
{{eqn | r = \sum x_i \paren {x_i - \overline x} + 0
}}
{{eqn | r = \sum x_i \paren {x_i - \overline x} + \overline x \sum \paren {x_i - \overline x}
      | c = Sum of Deviations from Mean
}}
{{eqn | r = \sum \paren {x_i + \overline x} \paren {x_i - \overline x}
      | c = Summation is Linear
}}
{{eqn | r = \sum \paren {x_i^2 - \overline x^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Squared Deviations from Mean

Let $S = \set {x_1, x_2, \ldots, x_n}$ be a set of real numbers.
Let $\overline x$ denote the arithmetic mean of $S$.
Then: 
:$\ds \sum_{i \mathop = 1}^n \paren {x_i - \overline x}^2 = \sum_{i \mathop = 1}^n \paren { {x_i}^2 - {\overline x}^2}$

Proof:
In this context, $x_1, x_2, \ldots, x_n$ are instances of a discrete random variable.
Hence the result Variance as Expectation of Square minus Square of Expectation can be applied:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
which means the same as this but in the language of probability theory.
{{qed}}
Theorem: Surjection from Natural Numbers iff Countable

Let $S$ be a non-empty set.
Then $S$ is countable {{iff}} there exists a surjection $f: \N \to S$.

Proof:
=== Necessary Condition ===
Suppose that $f: \N \to S$ is a surjection.
By Surjection from Natural Numbers iff Right Inverse, $f$ admits a right inverse $g: S \to \N$.
We have that $g$ is an injection by Right Inverse Mapping is Injection.
Hence the result, by the definition of a countable set.
{{qed|lemma}}
Theorem: Sum of Identical Terms

Let $x$ be a number.
Let $n \in \N$ be a natural number such that $n \ge 1$.
Then:
:$\ds \sum_{i \mathop = 1}^n x = n x$
{{explain|Why limit this to $n \ge 1$? It also works for zero.}}

Proof:
{{finish|this could be actually nontrivial; induction on $n$ seems easiest}}
{{expand|generalize to $x$ an element of a vector space, or for that matter, any abelian group}}
Category:Numbers
ibd586ciul8200zlipc2qntxpo013c4
Theorem: Synthetic Sub-Basis and Analytic Sub-Basis are Compatible

Let $\struct {X, \tau}$ be a topological space.
Let $\SS \subseteq \powerset X$, where $\powerset X$ denotes the power set of $X$.
Then $\SS$ is an analytic sub-basis for $\tau$ {{iff}} $\tau$ is the topology on $X$ generated by the synthetic sub-basis $\SS$.

Proof:
=== Necessary Condition ===
Follows directly from the definitions of the generated topology and an analytic sub-basis.
{{qed|lemma}}
Theorem: Analytic Basis is Analytic Sub-Basis

Let $\struct {X, \tau}$ be a topological space.
Let $\BB \subseteq \tau$ be an analytic basis for $\tau$.
Then $\BB$ is an analytic sub-basis for $\tau$.

Proof:
{{ProofWanted}}
Category:Topological Bases
ji3fvxw8xlmd0qk7wbmt0amhqe752sj
Theorem: Continuity Test using Sub-Basis

Let $\struct {X_1, \tau_1}$ and $\struct {X_2, \tau_2}$ be topological spaces.
Let $f: X_1 \to X_2$ be a mapping.
Let $\SS$ be an analytic sub-basis for $\tau_2$.
Suppose that:
:$\forall S \in \SS: f^{-1} \sqbrk S \in \tau_1$
where $f^{-1} \sqbrk S$ denotes the preimage of $S$ under $f$.
Then $f$ is continuous.

Proof:
Define:
:$\ds \BB = \set {\bigcap \AA: \AA \subseteq \SS, \AA \text{ is finite} } \subseteq \powerset {X_2}$
Let $B \in \BB$.
Then there exists a finite subset $\AA \subseteq \SS$ such that:
:$\ds B = \bigcap \AA$
Hence:
{{begin-eqn}}
{{eqn | l = f^{-1} \sqbrk B
      | r = f^{-1} \sqbrk {\bigcap \AA}
}}
{{eqn | r = \bigcap_{S \mathop \in \AA} f^{-1} \sqbrk S
      | c = Preimage of Intersection under Mapping: General Result
}}
{{eqn | o = \in
      | r = \tau_1
      | c = General Intersection Property of Topological Space
}}
{{end-eqn}}
Define:
:$\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB} \subseteq \powerset {X_2}$
By the definition of an analytic sub-basis, we have $\tau_2 \subseteq \tau$.
Let $U \in \tau_2$.
Then $U \in \tau$; therefore:
:$\ds \exists \AA \subseteq \BB: U = \bigcup \AA$
Hence:
{{begin-eqn}}
{{eqn | l = f^{-1} \sqbrk U
      | r = f^{-1} \sqbrk {\bigcup \AA}
}}
{{eqn | r = \bigcup_{S \mathop \in \AA} f^{-1} \sqbrk S
      | c = Preimage of Union under Mapping: General Result
}}
{{eqn | o = \in
      | r = \tau_1
      | c = because $\forall B \in \BB: f^{-1} \sqbrk B \in \tau_1$, and by {{Open-set-axiom|1}} applied to $\tau_1$
}}
{{end-eqn}}
That is, $f$ is continuous.
{{qed}}