avewright/proofwiki-math huggingface dataset:
Theorem: Product Distributes over Modulo Operation

Let $x, y, z \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation.
Then:
:$z \paren {x \bmod y} = \paren {z x} \bmod \paren {z y}$

Proof:
By definition of modulo operation:
:<nowiki>$x \bmod y := \begin {cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end {cases}$</nowiki>
If $y = 0$ we have that:
:$z \paren {x \bmod 0} = z x = \paren {z x} \bmod \paren {z 0}$
If $y \ne 0$ we have that:
{{begin-eqn}}
{{eqn | l = z \paren {x \bmod y}
      | r = z x - z y \floor {\frac x y}
      | c = 
}}
{{eqn | r = z x - z y \floor {\frac {z x} {z y} }
      | c = 
}}
{{eqn | r = \paren {z x} \bmod \paren {z y}
      | c = {{Defof|Modulo Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Congruence by Product of Moduli

Let $a, b, m \in \Z$.
Let $a \equiv b \pmod m$ denote that $a$ is congruent to $b$ modulo $m$.
Then $\forall n \in \Z, n \ne 0$:
:$a \equiv b \pmod m \iff a n \equiv b n \pmod {m n}$

Proof:
Let $n \in \Z: n \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod m
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = a \bmod m
      | r = b \bmod m
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{eqn | ll= \leadstoandfrom
      | l = n \paren {a \bmod n}
      | r = n \paren {b \bmod n}
      | c = Left hand implication valid only when $n \ne 0$
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a n} \bmod \paren {m n}
      | r = \paren {b n} \bmod \paren {m n}
      | c = Product Distributes over Modulo Operation
}}
{{eqn | ll= \leadstoandfrom
      | l = a n
      | o = \equiv
      | r = b n
      | rr= \pmod {m n}
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{end-eqn}}
Hence the result.
Note the invalidity of the third step when $n = 0$.
{{qed}}
Theorem: Definite Integral of Partial Derivative

Let $\map f {x, y}$ and $\map {\dfrac {\partial f} {\partial x} } {x, y}$ be continuous functions of $x$ and $y$ on $D = \closedint {x_1} {x_2} \times \closedint a b$.
Then:
:$\ds \frac \d {\d x} \int_a^b \map f {x, y} \rd y = \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y$
for $x \in \closedint {x_1} {x_2}$.

Proof:
From Leibniz's Integral Rule:
:$\ds \frac \d {\d y} \int_{\map a y}^{\map b y} \map f {x, y} \rd x = \map f {y, \map b y} \frac {\d b} {\d y} - \map f {y, \map a y} \frac {\d a} {\d y} + \int_{\map a y}^{\map b y} \frac {\partial} {\partial y} \map f {x, y} \rd x$
where $\map a y$, $\map b y$ are continuously differentiable.
Setting $\map a y$ and $\map b y$ constant, so that $\exists a, b \in \R: \map a y = a, \map b y = b$:
:$\dfrac {\d a} {\d y} = \dfrac {\d b} {\d y} = 0$
from which the result follows immediately.
{{qed}}
Theorem: Definite Integral of Partial Derivative

Let $\map f {x, y}$ and $\map {\dfrac {\partial f} {\partial x} } {x, y}$ be continuous functions of $x$ and $y$ on $D = \closedint {x_1} {x_2} \times \closedint a b$.
Then:
:$\ds \frac \d {\d x} \int_a^b \map f {x, y} \rd y = \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y$
for $x \in \closedint {x_1} {x_2}$.

Proof:
Define $\ds \map G x = \int_a^b \map f {x, y} \rd y$.
The continuity of $f$ ensures that $G$ exists.
Then by linearity of the integral:
:$\dfrac {\Delta G} {\Delta x} = \dfrac {\map G {x + \Delta x} - \map G x} {\Delta x} = \ds \int_a^b \frac {\map f {x + \Delta x, y} - \map f {x, y} } {\Delta x} \rd y$
We want to find the limit of this quantity as $\Delta x$ approaches zero.
For each $y \in \closedint a b$, we can consider $\map {f_y} x = \map f {x, y}$ as a separate function of the single variable $x$, with $\dfrac {\d f_y} {\d x} = \dfrac {\partial f} {\partial x}$.
Thus by the Mean Value Theorem, there is a number $c_y \in \openint x {x + \Delta x}$ such that:
:$\map {f_y} {x + \Delta x} - \map {f_y} x = \map {\dfrac {\d f_y} {\d x} } {c_y} \Delta x$
That is:
:$\map f {x + \Delta x, y} - \map f {x, y} = \map {\dfrac {\partial f} {\partial x} } {c_y, y} \Delta x$
Therefore:
:$\dfrac {\Delta G} {\Delta x} = \ds \int_a^b \map {\frac {\partial f} {\partial x} } {c_y, y} \rd y$
Now, pick any $\epsilon > 0$ and set $\epsilon_0 = \dfrac {\epsilon} {b - a}$.
Since $\dfrac {\partial f} {\partial x}$ is continuous on the compact set $D$, it is uniformly continuous on $D$.
Hence for each $x$ and $y$:
:$\size {\map {\dfrac {\partial f} {\partial x} } {x + h, y} - \map {\dfrac {\partial f} {\partial x} } {x, y} } < \epsilon_0$
whenever $h$ is sufficiently small.
Since $x < c_y < x + \Delta x$, it follows that for sufficiently small $\Delta x$:
:$\size {\map {\dfrac {\partial f} {\partial x} } {c_y, y} - \map {\dfrac {\partial f} {\partial x} } {x, y} } < \epsilon_0$
regardless of our choice of $y$.
So we can say:
{{begin-eqn}}
{{eqn | l = \size {\lim_{\Delta x \mathop \to 0} \frac {\Delta G} {\Delta x} - \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y}
      | r = \lim_{\Delta x \mathop \to 0} \size {\int_a^b \map {\frac {\partial f} {\partial x} } {c_y, y} - \frac {\partial f}{\partial x} \rd y}
}}
{{eqn | o = \le
      | r = \lim_{\Delta x \mathop \to 0} \int_a^b \size {\map {\frac {\partial f} {\partial x} } {c_y, y} - \map {\frac {\partial f} {\partial x} } {x, y} } \rd y
}}
{{eqn | o = \le
      | r = \int_a^b \epsilon_0 \rd y
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
But since $\epsilon$ was arbitrary, it follows that:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta G} {\Delta x} = \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y$
and the theorem is proved.
{{qed}}
Theorem: Law of Inverses (Modulo Arithmetic)

Let $m, n \in \Z$.
Then:
:$\exists n' \in \Z: n n' \equiv d \pmod m$
where $d = \gcd \set {m, n}$.

Proof:
We have that $d = \gcd \set {m, n}$.
So:
{{begin-eqn}}
{{eqn | q = \exists a, b \in \Z
      | l = a m + b n
      | r = d
      | c = Bézout's Identity
}}
{{eqn | ll= \leadsto
      | l = a m
      | r = d - b n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d - b n
      | o = \equiv
      | r = 0
      | rr= \pmod m
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{eqn | ll= \leadsto
      | l = b n
      | o = \equiv
      | r = d
      | rr= \pmod m
      | c = Modulo Addition: add $b n$ to both sides of congruence
}}
{{end-eqn}}
So $b$ (in the above) fits the requirement for $n'$ in the assertion to be proved.
{{qed}}
Category:Modulo Arithmetic
Category:Named Theorems
lwmlxsp3un1phf0ob597ivi56b186n3
Theorem: Common Factor Cancelling in Congruence

Let $a, b, x, y, m \in \Z$.
Let:
:$a x \equiv b y \pmod m$ and $a \equiv b \pmod m$
where $a \equiv b \pmod m$ denotes that $a$ is congruent modulo $m$ to $b$.
Then:
:$x \equiv y \pmod {m / d}$
where $d = \gcd \set {a, m}$.

Proof:
We have that $d = \gcd \set {a, m}$.
From Law of Inverses (Modulo Arithmetic), we have:
: $\exists a' \in \Z: a a' \equiv d \pmod m$
Hence:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod m
}}
{{eqn | ll= \leadsto
      | l = a a'
      | o = \equiv
      | r = b a'
      | rr= \pmod m
      | c = {{Defof|Modulo Multiplication}}
}}
{{eqn | o = \equiv
      | r = d
      | rr= \pmod m
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a x
      | o = \equiv
      | r = b y
      | rr= \pmod m
}}
{{eqn | ll= \leadsto
      | l =  a a' x
      | o = \equiv
      | r = b a' y
      | rr= \pmod m
      | c = {{Defof|Modulo Multiplication}}
}}
{{eqn | ll= \leadsto
      | l = d x
      | o = \equiv
      | r = d y
      | rr= \pmod m
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \equiv
      | r = y
      | rr= \paren {\bmod {\dfrac m d} }
      | c = Congruence by Product of Moduli
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Congruence by Factors of Modulo

Let $a, b \in \Z$.
Let $r$ and $s$ be coprime integers.
Then:
:$a \equiv b \pmod {r s}$ {{iff}} $a \equiv b \pmod r$ and $a \equiv b \pmod s$
where $a \equiv b \pmod r$ denotes that $a$ is congruent modulo $r$ to $b$.

Proof:
=== Necessary Condition ===
This is proved in Congruence by Divisor of Modulus.
Note that for this result it is not required that $r \perp s$.
{{qed|lemma}}
Theorem: Sum of Floors not greater than Floor of Sum

Let $\floor x$ denote the floor function.
Then:
:$\floor x + \floor y \le \floor {x + y}$
The equality holds:
:$\floor x + \floor y = \floor {x + y}$
{{iff}}:
:$x \bmod 1 + y \bmod 1 < 1$
where $x \bmod 1$ denotes the modulo operation.

Proof:
From the definition of the modulo operation, we have that:
:$x = \floor x + \paren {x \bmod 1}$
from which:
{{begin-eqn}}
{{eqn | l = \floor {x + y}
      | r = \floor {\floor x + \paren {x \bmod 1} + \floor y + \paren {y \bmod 1} }
      | c = 
}}
{{eqn | r = \floor x + \floor y + \floor {\paren {x \bmod 1} + \paren {y \bmod 1} }
      | c = Floor of Number plus Integer
}}
{{end-eqn}}
Hence the inequality.
The equality holds {{iff}}:
:$\floor {\paren {x \bmod 1} + \paren {y \bmod 1} } = 0$
that is, {{iff}}:
:$x \bmod 1 + y \bmod 1 < 1$
{{qed}}
Theorem: Sum of Ceilings not less than Ceiling of Sum

Let $\ceiling x$ be the ceiling function.
Then:
:$\ceiling x + \ceiling y \ge \ceiling {x + y}$
The equality holds:
:$\ceiling x + \ceiling y = \ceiling {x + y}$
{{iff}} either:
:$x \in \Z$ or $y \in \Z$
or:
:$x \bmod 1 + y \bmod 1 > 1$
where $x \bmod 1$ denotes the modulo operation.

Proof:
From the definition of the modulo operation, we have that:
:$x = \floor x + \paren {x \bmod 1}$
from which we obtain:
:$x = \ceiling x - \sqbrk {x \notin \Z} + \paren {x \bmod 1}$
where $\sqbrk {x \notin \Z}$ uses Iverson's convention.
{{begin-eqn}}
{{eqn | l = \ceiling {x + y}
      | r = \ceiling {\floor x + \paren {x \bmod 1} + \floor y + \paren {y \bmod 1} }
      | c = 
}}
{{eqn | r = \ceiling {\ceiling x - \sqbrk {x \notin \Z} + \paren {x \bmod 1} + \ceiling y - \sqbrk {y \notin \Z} + \paren {y \bmod 1} }
      | c = 
}}
{{eqn | r = \ceiling x + \ceiling y + \ceiling {\paren {x \bmod 1} + \paren {y \bmod 1} } - \sqbrk {x \notin \Z} - \sqbrk {y \notin \Z}
      | c = Ceiling of Number plus Integer
}}
{{end-eqn}}
We have that:
:$x \notin \Z \implies x \bmod 1 > 0$
As $0 \le x \bmod 1 < 1$ it follows that:
:$\sqbrk {x \notin \Z} \ge x \bmod 1$
Hence the inequality.
The equality holds {{iff}}:
:$\ceiling {\paren {x \bmod 1} + \paren {y \bmod 1} } = \sqbrk {x \notin \Z} + \sqbrk {y \notin \Z}$
that is, {{iff}} one of the following holds:
:$x \in \Z$, in which case $x \bmod 1 = 0$
:$y \in \Z$, in which case $y \bmod 1 = 0$
:both $x, y \in \Z$, in which case $\paren {x \bmod 1} + \paren {y \bmod 1} = 0$
:both $x, y \notin \Z$ and $\paren {x \bmod 1} + \paren {y \bmod 1} > 1$.
{{qed}}
Theorem: Integer to Power of p-1 over 2 Modulo p

Let $a \in \Z$.
Let $p$ be an odd prime.
Let $b = a^{\frac {\paren {p - 1} } 2}$.
Then one of the following cases holds:
:$b \bmod p = 0$
which happens exactly when $a \equiv 0 \pmod p$, or:
:$b \bmod p = 1$
or:
:$b \bmod p = p - 1$
where:
:$b \bmod p$ denotes the modulo operation
:$x \equiv y \pmod p$ denotes that $x$ is congruent modulo $p$ to $y$.

Proof:
By definition of congruence modulo $p$:
:$\forall x, y \in \R: x \equiv y \pmod p \iff x \bmod p = y \bmod p$ 
We have that:
:$b = a^{\frac{\paren {p - 1} } 2}$
and so:
:$b^2 = a^{p - 1}$
Let $a \equiv 0 \pmod p$.
Then by definition of congruence modulo $p$:
:$p \divides a$
and so:
:$p \divides a^{\frac{\paren {p - 1} } 2}$
where $\divides$ denotes divisibility.
Thus by definition of congruence modulo $p$:
:$b \equiv 0 \pmod p$
and so:
:$b \bmod p = 0$
{{qed|lemma}}
Otherwise, from Fermat's Little Theorem:
:$b^2 \equiv 1 \pmod p$
That is:
:$b^2 - 1 \equiv 0 \pmod p$
From Difference of Two Squares:
:$b^2 - 1 = \paren {b + 1} \paren {b - 1}$
So either:
:$p \divides b + 1$
or:
:$p \divides b - 1$
{{AimForCont}} both $p \divides b + 1$ and $p \divides b - 1$.
Then by Modulo Subtraction is Well-Defined:
:$p \divides \paren {b + 1} - \paren {b - 1} = 2$
But $p$ is an odd prime.
So it cannot be the case that $p \divides 2$.
From this contradiction it follows that 
Note that $p$ cannot divide both $b + 1$ and $b - 1$.
So either:
{{begin-eqn}}
{{eqn | l = \paren {b - 1}
      | o = \equiv
      | r = 0
      | rr= \pmod p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \equiv
      | r = 1
      | rr= \pmod p
      | c = Modulo Addition is Well-Defined
}}
{{end-eqn}}
or:
{{begin-eqn}}
{{eqn | l = \paren {b + 1}
      | o = \equiv
      | r = 0
      | rr= \pmod p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \equiv
      | r = -1
      | rr= \pmod p
      | c = Modulo Subtraction is Well-Defined
}}
{{eqn | o = \equiv
      | r = p - 1
      | rr= \pmod p
      | c = Negative Number is Congruent to Modulus minus Number
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Image Filter is Filter

Let $X, Y$ be sets.
Let $\powerset X$ and $\powerset Y$ be the power sets of $X$ and $Y$ respectively.
Let $f: X \to Y$ be a mapping.
Let $\FF \subset \powerset X$ be a filter on $X$.
Then the image filter of $\FF$ {{WRT}} $f$:
:$f \sqbrk \FF := \set {U \subseteq Y: f^{-1} \sqbrk U \in \FF}$
is a filter on $Y$.

Proof:
From the definition of a filter we have to prove four things:
: $(1): \quad f \sqbrk \FF \subset \powerset Y$
: $(2): \quad Y \in f \sqbrk \FF, \O \notin f \sqbrk \FF$
: $(3): \quad U, V \in f \sqbrk \FF \implies U \cap V \in f \sqbrk \FF$
: $(4): \quad U \in f \sqbrk \FF, U \subseteq V \subseteq Y \implies V \in f \sqbrk \FF$
By construction we have:
:$f \sqbrk \FF \subseteq \powerset Y$
Since $f^{-1} \sqbrk \O = \O \notin \FF$ we know that:
:$\O \notin f \sqbrk \FF$
Therefore:
:$f \sqbrk \FF \ne \powerset Y$
which implies $(1)$.
Because $f^{-1} \sqbrk Y = X \in \FF$, we have:
:$Y \in f \sqbrk \FF$
Since we've already shown $\O \notin f \sqbrk \FF$, this implies $(2)$.
Let $U, V \in f \sqbrk \FF$.
From Preimage of Intersection under Mapping:
:$f^{-1} \sqbrk {U \cap V} = f^{-1} \sqbrk U \cap f^{-1} \sqbrk V \in \FF$
(since $\FF$ is a filter).
Thus $U \cap V \in f \sqbrk \FF$, and so $(3)$ holds.
Finally, let $U \in f \sqbrk \FF$ and $V \subseteq Y$ such that $U \subseteq V$.
Then from Preimage of Subset is Subset of Preimage:
:$f^{-1} \sqbrk U \subseteq f^{-1} \sqbrk V$
Since $f^{-1} \sqbrk U \in \FF$ and $\FF$ is a filter it follows that:
:$f^{-1} \sqbrk V \in \FF$
which implies:
:$V \in f \sqbrk \FF$
and thus $(4)$.
{{qed}}
Category:Set Theory
Category:Filter Theory
i1d1ab5igkt86mitaheqndgtxrezyik
Theorem: Equivalence of Definitions of Continuous Mapping between Topological Spaces/Point

Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $f: S_1 \to S_2$ be a mapping from $S_1$ to $S_2$.
Let $x \in S_1$.
{{TFAE|def = Continuous at Point of Topological Space|view = continuity at a point of a topological space}}
=== Definition using Open Sets ===
{{Definition:Continuous Mapping (Topology)/Point/Open Sets}}
=== Definition using Neighborhoods ===
{{Definition:Continuous Mapping (Topology)/Point/Neighborhoods}}
=== Definition using Neighborhood Inverse ===
{{Definition:Continuous Mapping (Topology)/Point/Neighborhood Inverse}}
=== Definition using Filters ===
{{Definition:Continuous Mapping (Topology)/Point/Filters}}

Proof:
=== Definition using Open Sets implies Definition using Neighborhoods ===
Let $f$ be a continuous mapping defined using Open Sets.
Then by definition:
:For every open set $U_2$ of $T_2$ such that $\map f x \in U_2$, there exists an open set $U_1$ of $T_1$ such that $x \in U_1$ and $f \sqbrk {U_1} \subseteq U_2$.
Let $N$ be a neighborhood of $\map f x$ in $T_2$.
Then by definition of neighborhood, there exists an open set $U_2$ of $T_2$ such that $\map f x \in U_2$ and $U_2 \subseteq N$.
As $U_2$ is an open set $U_2$ of $T_2$, $f^{-1} \sqbrk {U_2}$ is an open set of $T_1$.
As $\map f x \in U_2$, it follows by definition of preimage of $U_2$ that $x \in f^{-1} \sqbrk {U_2}$.
Thus $f^{-1} \sqbrk {U_2}$ is a neighborhood of $x$ in $T_1$, which we relabel $M$.
From Image of Preimage under Mapping:
:$f \sqbrk M \subseteq U_2$
But we have that $U_2 \subseteq N$.
Thus we have demonstrated the existence of a neighborhood $M$ of $x$ such that $f \sqbrk M \subseteq N$
That is, $f$ is a continuous mapping defined using Neighborhoods.
{{qed|lemma}}
Theorem: Filter on Product Space Converges to Point iff Projections Converge to Projections of Point

Let $\family{X_i}_{i \mathop \in I}$ be an indexed family of non-empty topological spaces where $I$ is an arbitrary index set.
Let $\ds X := \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Let $\FF$ be a filter on $X$.
Let $x \in X$.
Let $\pr_i: X \to X_i$ denote the projection from $X$ onto $X_i$.
Then $\FF$ converges to $x$ {{iff}}:
:for all $i \in I$ the image filter $\map {\pr_i} \FF$ converges to $x_i := \map {\pr_i} x$.

Proof:
=== Necessary Condition ===
Let $\FF$ converge to $x$.
Let $i \in I$.
From Projection from Product Topology is Continuous, $\pr_i : X \to X_i$ is continuous.
Thus $\map {\pr_i} \FF$ converges to $\map {\pr_i} x$ as claimed.
{{qed|lemma}}
Theorem: Image of Ultrafilter is Ultrafilter

Let $X, Y$ be sets.
Let $f: X \to Y$ be a mapping.
Let $\FF$ be an ultrafilter on $X$.
Then the image filter $f \sqbrk \FF$ is an ultrafilter on $Y$.

Proof:
From Image Filter is Filter, we have that $\FF$ is a filter on $Y$.
Let $\GG$ be a filter on $Y$ such that $f \sqbrk \FF \subseteq \GG$.
We have to show that $f \sqbrk \FF = \GG$.
{{AimForCont}} there exists $U \in \GG$ such that $U \notin f \sqbrk \FF$.
By the definition of $f \sqbrk \FF$ this implies that $f^{-1} \sqbrk U \not \in \FF$.
By definition of ultrafilter:
:$V := X \setminus f^{-1} \sqbrk U \in \FF$
Because $V \subseteq f^{-1} \sqbrk {f \sqbrk V}$ it follows that:
:$f^{-1} \sqbrk {f \sqbrk V} \in \FF$
Thus also:
:$f \sqbrk V \in f \sqbrk \FF$
By assumption we have:
:$f \sqbrk \FF \subseteq \GG$
thus:
:$f \sqbrk V \in \GG$
But:
:$f \sqbrk V \cap U = f \sqbrk {X \setminus f^{-1} \sqbrk U} \cap U = \O \notin \GG$
Thus $\GG$ is not a filter, which is a contradiction to our assumptions.
Thus there can be no $U \in \GG$ such that $U \notin \FF$.
Therefore:
:$f \sqbrk \FF = \GG$
Hence $f \sqbrk \FF$ is an ultrafilter.
{{qed}}
Theorem: Image of Ultrafilter is Ultrafilter

Let $X, Y$ be sets.
Let $f: X \to Y$ be a mapping.
Let $\FF$ be an ultrafilter on $X$.
Then the image filter $f \sqbrk \FF$ is an ultrafilter on $Y$.

Proof:
From Image Filter is Filter, we have that $\FF$ is a filter on $Y$.
In view of definition of ultrafilter, we need to show that:
:for every $A \subseteq Y$, either $A \in f \sqbrk \FF$ or $\relcomp Y A \in f \sqbrk \FF$
Let $A \subseteq Y$ be arbitrary.
Suppose $A \not \in f \sqbrk \FF$.
Then, by definition of image filter:
:$f^{-1} \sqbrk A \not \in \FF$
By definition of ultrafilter:
:$\relcomp X {f^{-1} \sqbrk A} \in \FF$
As Complement of Preimage equals Preimage of Complement:
:$\relcomp X {f^{-1} \sqbrk A} = f^{-1} \sqbrk {\relcomp Y A}$
Thus:
:$f^{-1} \sqbrk {\relcomp Y A} \in \FF$
That is, by definition of image filter:
:$\relcomp Y A \in f \sqbrk \FF$
{{qed}}
Theorem: Tychonoff's Theorem

Let $I$ be an indexing set.
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of non-empty topological spaces.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Then $X$ is compact {{iff}} each $X_i$ is compact.

Proof:
First assume that $X$ is compact. 
From Projection from Product Topology is Continuous, the projections $\pr_i : X \to X_i$ are continuous.
It follows from Continuous Image of Compact Space is Compact that the $X_i$ are compact.
Assume now that each $X_i$ is compact.
By Equivalence of Definitions of Compact Topological Space it is enough to show that every ultrafilter on $X$ converges.
Thus let $\FF$ be an ultrafilter on $X$.
From Image of Ultrafilter is Ultrafilter, for each $i \in I$, the image filter $\map {\pr_i} \FF$ is an ultrafilter on $X_i$.
Each $X_i$ is compact by assumption.
So by Equivalence of Definitions of Compact Topological Space, each $\map {\pr_i} \FF$ converges.
By Filter on Product Space Converges iff Projections Converge, $\FF$ converges.
{{explain|Find the appropriate link for "converges" and explain why this proves the result.}}
{{qed}}
Theorem: Wallis's Product

{{begin-eqn}}
{{eqn | l = \prod_{n \mathop = 1}^\infty \frac {2 n} {2 n - 1} \cdot \frac {2 n} {2 n + 1}
      | r = \frac 2 1 \cdot \frac 2 3 \cdot \frac 4 3 \cdot \frac 4 5 \cdot \frac 6 5 \cdot \frac 6 7 \cdot \frac 8 7 \cdot \frac 8 9 \cdots
      | c = 
}}
{{eqn | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}

Proof:
Into Euler Formula for Sine Function:
{{begin-eqn}}
{{eqn | l = \dfrac {\sin x} x
      | r = \paren {1 - \dfrac {x^2} {\pi^2} } \paren {1 - \dfrac {x^2} {4 \pi^2} } \paren {1 - \dfrac {x^2} {9 \pi^2} } \cdots
      | c = 
}}
{{eqn | r = \prod_{n \mathop = 1}^\infty \paren {1 - \dfrac {x^2} {n^2 \pi^2} }
      | c = 
}}
{{end-eqn}}
we substitute $x = \dfrac \pi 2$.
From Sine of Half-Integer Multiple of Pi:
:$\sin \dfrac \pi 2 = 1$
Hence:
{{begin-eqn}}     
{{eqn | l = \frac 2 \pi
      | r = \prod_{n \mathop = 1}^\infty \paren {1 - \frac 1 {4 n^2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac \pi 2
      | r = \prod_{n \mathop = 1}^\infty \paren {\frac {4 n^2} {4 n^2 - 1} }
      | c = 
}}
{{eqn | r = \prod_{n \mathop = 1}^\infty \frac {\paren {2 n} \paren {2 n} } {\paren {2 n - 1} \paren {2 n + 1} }
      | c = 
}}
{{eqn | r = \frac 2 1 \cdot \frac 2 3 \cdot \frac 4 3 \cdot \frac 4 5 \cdot \frac 6 5 \cdot \frac 6 7 \cdot \frac 8 7 \cdot \frac 8 9 \cdots
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Wallis's Product

{{begin-eqn}}
{{eqn | l = \prod_{n \mathop = 1}^\infty \frac {2 n} {2 n - 1} \cdot \frac {2 n} {2 n + 1}
      | r = \frac 2 1 \cdot \frac 2 3 \cdot \frac 4 3 \cdot \frac 4 5 \cdot \frac 6 5 \cdot \frac 6 7 \cdot \frac 8 7 \cdot \frac 8 9 \cdots
      | c = 
}}
{{eqn | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \prod_{n \mathop = 1}^\infty \frac {2 n} {2 n - 1} \cdot \frac {2 n} {2 n + 1}
      | r = \prod_{n \mathop = 1}^\infty \frac {\paren {2 n - 0} \paren {2 n - 0} \times \dfrac 1 2 \times \dfrac 1 2} {\paren {2 n - 1} \paren {2 n + 1} \times \dfrac 1 2 \times \dfrac 1 2}
      | c = multiplying top and bottom by $\dfrac 1 2 \times \dfrac 1 2$ 
}}
{{eqn | r = \prod_{n \mathop = 1}^\infty \frac {\paren {n - 0} \paren {n - 0} } {\paren {n - \dfrac 1 2} \paren {n + \dfrac 1 2} }
      | c = 
}}
{{eqn | r = \frac { \map \Gamma {\dfrac 1 2} \map \Gamma {\dfrac 3 2} } {\map \Gamma {1} \map \Gamma {1} }
      | c = Infinite Product of Product of Sequence of n plus alpha over Sequence of n plus beta
}}
{{eqn | r = \frac { \sqrt \pi \times \dfrac {\sqrt \pi} 2 } {0! \times 0! }
      | c = Gamma Function of One Half, Gamma Difference Equation, Gamma Function Extends Factorial
}}
{{eqn | r = \frac \pi 2
      | c = {{Defof|Factorial}}
}}
{{end-eqn}}
{{qed}}
Theorem: Number of Regions in Plane Defined by Given Number of Lines

The maximum number $L_n$ of regions in the plane that can be defined by $n$ straight lines in the plane is:
:$L_n = \dfrac {n \paren {n + 1} } 2 + 1$
{{OEIS|A000124}}

Proof:
=== Setting up a Recurrence Rule ===
First we consider the plane with no lines at all.
This has one region, so $L_0 = 1$.
Now when we have one line, we divide the plane into two regions, so $L_1 = 2$.
Now consider the $n$th line.
This increase the number of regions by $k$ iff it splits $k$ of the old regions.
It can split $k$ of the old regions {{iff}} it hits the existing lines on the plane in $k-1$ places.
Two straight lines can intersect in at most one point.
So the new line can intersect the $n - 1$ old ones in at most $n - 1$ different points.
Therefore $k \le n$.
So we see that $L_n \le L_{n - 1} + n$.
Now, it is always possible to place the $n$th line so that:
:$(1): \quad$ It is not parallel to any of the others, and therefore intersects all the other $n - 1$ lines
:$(2): \quad$ It does not go through any of the existing intersection points (so intersects them all in different places).
Thus we see that $L_n \ge L_{n - 1} + n$.
Hence the recurrence:
:$L_n = L_{n - 1} + n$