avewright/proofwiki-math huggingface dataset:
Theorem: Continuous Complex-Valued Function Vanishing at Infinity is Bounded and Attains Supremum

Let $X$ be a locally compact Hausdorff space. 
Let $f : X \to \C$ be a continuous function that vanishes at infinity.
Then $f$ is bounded and there exists $x_\ast \in X$ such that:
:$\ds \map f {x_\ast} = \sup_{x \mathop \in X} \cmod {\map f x}$

Proof:
From the definition of a function vanishing at infinity:
:there exists a compact set $F \subseteq X$ such that:
::$\cmod {\map f x} < 1$ for all $x \in X \setminus F$.
From Continuous Function on Compact Space is Bounded:
:$f$ is bounded on $F$. 
That is, there exists a real number $M > 0$ such that:
:$\cmod {\map f x} \le M$ for all $x \in F$. 
Hence, we have:
:$\cmod {\map f x} \le \max \set {1, M}$ for each $x \in X$.
So $f$ is bounded.
Now suppose that $\map f x = 0$ for each $x \in X$. 
Then $f$ clearly attains its bounds.
Now take $f$ such that:
:$\map f x \ne 0$ for some $x \in X$. 
Let:
:$\ds M = \sup_{x \mathop \in X} \cmod {\map f x} > 0$ 
which is finite from the above. 
Since $f$ vanishes at infinity, there exists a compact set $K \subseteq X$ such that:
:$\ds \cmod {\map f x} < \frac M 2$ for each $x \in X \setminus K$. 
By the definition of supremum:
:for each $M/2 > \epsilon > 0$ there exists $x_0 \in X$ such that $M - \epsilon < \cmod {\map f {x_0} } \le M$ 
Since:
:$\ds \cmod {\map f x} < \frac M 2$ for each $x \in X \setminus K$
the points $x_0$ described above must fall in $K$. 
Hence we have:
:$\ds \sup_{x \mathop \in X} \cmod {\map f x} = \sup_{x \mathop \in K} \cmod {\map f x}$ 
From Complex Modulus Function is Continuous and Composite of Continuous Mappings is Continuous, $\cmod f$ is continuous.
Consider the restriction $\cmod f \restriction K : K \to \R$. 
From Restriction of Continuous Mapping is Continuous: Topological Spaces, $\cmod f \restriction K$ is continuous.
Hence from {{Corollary|Continuous Image of Compact Space is Compact|3}}, $\cmod f \restriction K$ attains its bounds. 
Hence there exists $x_0 \in K$ such that $\cmod {\map f {x_0} } = M$, hence the result.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
9m4mkc1rpqb185i22fnkoyoqartt66b
Theorem: Independence System Induced from Set of Subsets

Let $S$ be a finite set.
Let $\mathscr A$ be a non-empty set of subsets of $S$.
Let $\mathscr I = \set {X \subseteq S : \exists A \in \mathscr A : X \subseteq A}$.
Then $\struct {S, \mathscr I}$ is an independence system.

Proof:
It is shown that $\mathscr I$ satisfies the independence system axioms:
{{:Axiom:Independence System Axioms}}
Theorem: Complex-Valued Function Vanishing in Neighborhood of Infinity Vanishes at Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $f : X \to \C$ be a function vanishing in a neighborhood of infinity. 
Then $f$ vanishes at infinity.

Proof:
Let $\epsilon > 0$. 
Since $f$ vanishes in a neighborhood of infinity, there exists a compact $F \subseteq X$ such that:
:$\map f x = 0$ for $x \in X \setminus F$
In particular:
:$\cmod {\map f x} = 0 < \epsilon$ for each $x \in X \setminus F$. 
Hence $f$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
Category:Complex-Valued Functions Vanishing in Neighborhood of Infinity
f0j45d6onglmixtf3ucoczkw1ka9jnw
Theorem: Zero Function Vanishes in Neighborhood of Infinity

Let $X$ be a locally compact Hausdorff space. 
Define a function $f : X \to \C$ by:
:$\map f x = 0$
for each $x \in X$. 
Then $f$ vanishes in a neighborhood of infinity.

Proof:
From Empty Set is Compact:
:$\O \subseteq X$ is compact.
We then have: 
:$\map f x = 0$ for all $x \in X \setminus \O$
Hence $f$ vanishes in a neighborhood of infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing in Neighborhood of Infinity
mcdzq8whisimmco3vn1uhq0cj7i3api
Theorem: Linear Combination of Complex-Valued Functions Vanishing at Infinity Vanishes at Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $f, g : X \to \C$ be complex-valued functions vanishing at infinity.
Let $\lambda \in \C$.
Then $f + \lambda g$ vanishes at infinity.

Proof:
If $\lambda = 0$, we are done immediately. 
Take $\lambda \ne 0$. 
Let $\epsilon > 0$. 
Since $f$ vanishes at infinity, there exists a compact set $F_1 \subseteq X$ such that:
:$\cmod {\map f x} < \dfrac \epsilon 2$ for each $x \in X \setminus F_1$.
Since $g$ vanishes at infinity, there exists a compact set $F_2 \subseteq X$ such that:
:$\cmod {\map g x} < \dfrac \epsilon {2 \cmod \lambda}$ for each $x \in X \setminus F_2$. 
From Union of Two Compact Sets is Compact, $F_1 \cup F_2$ is compact and:
:$\cmod {\map f x} < \dfrac \epsilon 2$ and $\cmod {\map g x} < \dfrac \epsilon {2 \cmod \lambda}$ for each $x \in X \setminus \paren {F_1 \cup F_2}$.
Then, we have for $x \in X \setminus \paren {F_1 \cup F_2}$:
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x + \lambda \map g x}
		| o = \le
		| r = \cmod {\map f x} + \cmod \lambda \cmod {\map g x}
		| c = Triangle Inequality for Complex Numbers
}}
{{eqn	| o = <
		| r = \frac \epsilon 2 + \cmod \lambda \paren {\frac \epsilon {2 \cmod \lambda} }
}}
{{eqn	| r = \frac \epsilon 2 + \frac \epsilon 2 
}}
{{eqn	| r = \epsilon 
}}
{{end-eqn}}
Since again $F_1 \cup F_2$ is compact, we have that $f + \lambda g$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
g6q6c82pdnlpjo75fp1rhvqz71rzdjo
Theorem: Uniform Limit of Sequence of Continuous Complex-Valued Functions Vanishing at Infinity Vanishes at Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence of functions $f_n : X \to \C$ that vanishes at infinity.
Let $f : X \to \C$ be a function such that:
:$f_n - f$ is bounded for each $n \in \N$
and:
:$\ds \sup_{x \mathop \in X} \cmod {\map {f_n} x - \map f x} \to 0$ as $n \to \infty$.
Then $f$ vanishes at infinity.

Proof:
Let $\epsilon > 0$. 
Since:
:$\ds \sup_{x \mathop \in X} \cmod {\map {f_n} x - \map f x} \to 0$ as $n \to \infty$
we can take $N \in \N$ such that:
:$\ds \sup_{x \mathop \in X} \cmod {\map {f_N} x - \map f x} < \frac \epsilon 2$
Further since $f_N$ vanishes at infinity, there exists a compact set $F \subseteq X$ such that:
:$\cmod {\map {f_N} x} < \dfrac \epsilon 2$ for each $x \in X \setminus F$.
Since:
:$\cmod {\map {f_N} x - \map f x} < \dfrac \epsilon 2$ for each $x \in X$
we in particular have:
:$\cmod {\map {f_N} x - \map f x} < \dfrac \epsilon 2$ for each $x \in X \setminus F$
Then from Triangle Inequality for Complex Numbers, we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x}
		| r = \cmod {\map f x - \map {f_N} x} + \cmod {\map {f_N} x}
}}
{{eqn	| o = <
		| r = \frac \epsilon 2 + \frac \epsilon 2
}}
{{eqn	| r = \epsilon 
}}
{{end-eqn}}
for each $x \in X \setminus F$.
So $f$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
jnqxjeyxiquv0mycfwfi0nt1nkjdzb6
Theorem: Matroid Bases Satisfy Formulation 4 Base Axiom

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $\mathscr B$ be the set of bases of the matroid $M$.
Then $\mathscr B$ satisfies formulation $4$ of base axiom:
{{:Axiom:Base Axiom (Matroid)/Formulation 4}}

Proof:
Let $B_1, B_2 \in \mathscr B$.
Let $x \in B_1 \setminus B_2$.
From Matroid Base Union External Element has Fundamental Circuit:
:there exists a fundamental circuit $\map C {x, B_2}$ of $M$ such that $x \in \map C {x, B_2} \subseteq B_2 \cup \set x$
By definition of set intersection:
:$x \in B_1 \cap \map C {x, B_2}$
From Element of Matroid Base and Circuit has Substitute:
:$\exists y \in \map C {x, B_2} \setminus B_1 : \paren{B_1 \setminus \set x} \cup \set y \in \mathscr B$
We have:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \map C {x, B_2} \setminus B_1
}}
{{eqn | o = \subseteq
      | r = \map C {x, B_2} \setminus \set x
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{eqn | o = \subseteq
      | r = \paren{B_2 \cup \set x} \setminus \set x
      | c = Set Difference over Subset
}}
{{eqn | o = \subseteq
      | r = B_2 \setminus \set x
      | c = Set Difference with Union is Set Difference
}}
{{eqn | o = \subseteq
      | r = B_2
      | c = Set Difference is Subset
}}
{{end-eqn}}
From Matroid Base Substitution From Fundamental Circuit:
:$\paren{B_2 \setminus \set y} \cup \set x \in \mathscr B$
It follows that $\mathscr B$ satisfies formulation $4$ of base axiom:
{{Axiom:Base Axiom (Matroid)/Formulation 4}}
{{qed}}
Category:Matroid Bases
rti1vrwrxk33zxgohmp1nsu5z9ust4m
Theorem: Product of Complex-Valued Functions Vanishing at Infinity Vanishes at Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $f, g : X \to \C$ be complex-valued functions vanishing at infinity.
Then $f g$ vanishes at infinity.

Proof:
Let $\epsilon > 0$. 
Since $f$ vanishes at infinity, there exists a compact set $F_1 \subseteq X$ such that:
:$\cmod {\map f x} < \sqrt \epsilon$ for each $x \in X \setminus F_1$.
Since $g$ vanishes at infinity, there exists a compact set $F_2 \subseteq X$ such that:
:$\cmod {\map g x} < \sqrt \epsilon$ for each $x \in X \setminus F_2$. 
From Union of Two Compact Sets is Compact, $F_1 \cup F_2$ is compact and:
:$\cmod {\map f x} < \sqrt \epsilon$ and $\cmod {\map g x} < \sqrt \epsilon$ for each $x \in X \setminus \paren {F_1 \cup F_2}$.
Then, we have for $x \in X \setminus \paren {F_1 \cup F_2}$:
:$\cmod {\map f x \map g x} \le \cmod {\map f x} \cmod {\map g x} < \paren {\sqrt \epsilon}^2 = \epsilon$
Since again $F_1 \cup F_2$ is compact, we have that $f g$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
68ycl6mbjbzskopb9137yv8o8y9dub3
Theorem: Mean Deviation about Mean equals Zero

Let $S$ be an object upon which an arithmetic mean and a mean deviation $\map D S$ are both defined.
Let $\map D S$ be the mean deviation about the arithmetic mean $\bar x$ of $S$.
Then:
:$\map D S = 0$

Proof:
From Sum of Deviations from Mean:
:$\ds \sum_{i \mathop = 1}^n \paren {x_i - \bar x} = 0$
Therefore:
:$\ds \map D S = \frac 1 n \sum_{i \mathop = 1}^n \paren {x_i - \bar x} = 0$
{{qed}}
Theorem: Mean Squared Error equals Variance for Unbiased Estimator

Let $T$ be an unbiased estimator for a population parameter of a population $P$.
Then the mean squared error for $T$ equals the variance of $T$.

Proof:
Let $T$ be a general estimator.
From Mean Squared Error for Biased Estimator:
:$M = \var T + \paren {\map B T}^2$
where:
:$\var T$ denotes the variance of $T$
:$\map B T$ denotes the bias on $T$.
By definition, if $T$ is unbiased:
:$\map B T = 0$
The result follows.
{{qed}}
Theorem: Variance is Least Mean Square Deviation about Point

Let $S$ be an object upon which:
:the mean square deviation
:the expectation
:the variance
is defined.
For each point $x$ in $S$, let $\map M x$ denote the mean square deviation of $S$ about $x$.
Then the minimum of $\map M x$ is the is the variance of $S$.
That is, the expectation $\bar x$ of $S$ is the value of $S$ for which the mean square deviation is smallest.

Proof:
=== Discrete Case ===
Let $\map f {x_i}$ be the probability mass function of $x_i \in S$.
Then:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \map M x
      | r = 0
      | c = Interior Extremum Theorem
}}
{{eqn | ll= \leadsto
      | l = \frac \d {\d x} \sum_{i \mathop = 1}^n \paren {x_i - x}^2 \map f {x_i}
      | r = 0
      | c = {{Defof|Mean Square Deviation}}
}}
{{eqn | ll= \leadsto
      | l = 2 \sum_{i \mathop = 1}^n \paren {x_i - x} \paren {-1} \map f {x_i}
      | r = 0
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 1}^n \paren {x - x_i} \map f {x_i}
      | r = 0
      | c = Divide both sides by $2$
}}
{{eqn | ll= \leadsto
      | l = x \sum_{i \mathop = 1}^n \map f {x_i} - \sum_{i \mathop = 1}^n x_i \map f {x_i}
      | r = 0
      | c = Summation of Sum of Mappings on Finite Set
}}
{{eqn | ll= \leadsto
      | l = x - \sum_{i \mathop = 1}^n x_i \map f {x_i}
      | r = 0
      | c = $x$ is constant over $i$
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \sum_{i \mathop = 1}^n x_i \map f {x_i}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \bar x
      | c = {{Defof|Expectation of Discrete Random Variable}}
}}
{{end-eqn}}
By the definition of variance, $\map M {\bar x}$ is the variance of $S$.
{{qed}}
Theorem: Dual Matroid is Matroid

Let $M = \struct {S, \mathscr I}$ be a matroid.
Then the dual $M^*$ of $M$ is a matroid.

Proof:
Let $\mathscr B$ be the set of bases of the matroid $M$.
From Matroid Bases Satisfy Formulation 4 Base Axiom:
:$\mathscr B$ satisfies formulation 4 base axiom.
By formulation 5 base axiom:
:$\mathscr B$ satisfies formulation 5 base axiom.
Let $\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
From Subsets Satisfy Formulation 5 Matroid Base Axiom Iff Complements Satisfy Formulation 1:
:$\mathscr B^*$ satisfies formulation 1 base axiom.
From Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom:
:there exists a matroid $M^* = \struct{S, \mathscr I^*}$ whose bases is the set:
::$\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
From Matroid is Uniquely Defined by Bases:
:$M^*$ is the unique matroid whose bases is the set:
::$\mathscr B^* = \set{S \setminus B : B \in \mathscr B}$.
The result follows.
{{qed}}
Theorem: Kasteleyn's Formula

The number of perfect covers of a chessboard of dimensions $m \times n$ is given by the formula:
:$\ds \prod_{j \mathop = 1}^{\ceiling {\frac m 2} } \prod_{k \mathop = 1}^{\ceiling {\frac n 2} } \paren {4 \cos^2 \frac {\pi j} {m + 1} + 4 \cos^2 \frac {\pi k} {n + 1} }$

Proof:
{{ProofWanted|Import proof from Kasteleyns paper}}
{{Namedfor|Pieter Willem Kasteleyn|cat = Kasteleyn}}
Theorem: Perpendicular Bisector is Unique

Let $AB$ be a straight line segment in a Euclidean geometry.
Let $\LL$ be the perpendicular bisector of $AB$.
Then $\LL$ is unique.

Proof:
Let $\LL_2$ be another perpendicular bisector of $AB$.
Since both $\LL$ and $\LL_2$ are perpendicular to $AB$, they are parallel by Equal Corresponding Angles implies Parallel Lines.
Since both $\LL$ and $\LL_2$ bisect $AB$, they intersect at the midpoint of $AB$.
Therefore, the distance between $\LL$ and $\LL_2$, is zero.
By Distance between Two Parallel Straight Lines is Everywhere the Same, the distance between $\LL$ and $\LL_2$, is everywhere zero.
Thus, $\LL$ and $\LL_2$ coincide everywhere and are the same line.
{{qed}}
Category:Perpendicular Bisectors
40m9pbemxcn1i9c30qqalpxeq97gajq
Theorem: Complex-Valued Function on Compact Hausdorff Space Vanishes at Infinity

Let $X$ be a compact Hausdorff space. 
Let $f : X \to \C$ be a function.
Then $f$ vanishes at infinity.

Proof:
Let $\epsilon > 0$.
Then:
:$\cmod {\map f x} < \epsilon$ for all $x \in \O$.
By hypothesis:
:$X$ is compact.
Hence we in particular have:
:$\cmod {\map f x} < \epsilon$ for all $x \in X \setminus X$
with $X$ compact.
Hence $f$ vanishes at infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
hn4y929qygyifbpxn28s6b5k7t4q9rq
Theorem: Algebra of all Mappings is Algebra

Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {A, +_A, \circ_A, \ast_A}$ be an $R$-algebra. 
Let $S$ be a set.
Let $\struct {A^S, +, \circ, \ast}$ the $R$-algebra of all mappings from $S$ to $A$.
Then $\struct {A^S, +, \circ, \ast}$ is an $R$-algebra.

Proof:
From Module of All Mappings is Module, $\struct {A^S, +, \circ}$ is a module. 
It remains to show that $\ast$ is $R$-bilinear.
Let $f, g, h \in A^S$ and $\lambda \in R$. 
We have, for $x \in S$: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {\paren {f + \lambda \circ g} \ast h} } x
		| r = \map {\paren {f + \lambda \circ g} } x \ast_A \map h x
}}
{{eqn	| r = \paren {\map f x + \lambda \circ_A \map g x} \ast_A \map h x
}}
{{eqn	| r = \map f x \ast_A \map h x + \lambda \circ_A \paren {\map g x \ast_A \map h x}
}}
{{eqn	| r = \map {\paren {f \ast h} } x + \lambda \circ_A \map {\paren {g \ast h} } x
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn	| l = \map {\paren {f \ast \paren {g + \lambda \circ h} } } x
		| r = \map f x \ast_A \paren {\map g x + \lambda \circ_A \map h x}
}}
{{eqn	| r = \map f x \ast_A \map g x + \map f x \ast_A \paren {\lambda \circ_A \map h x}
}}
{{eqn	| r = \map f x \ast_A \map g x + \lambda \circ_A \paren {\map f x \ast_A \map h x}
}}
{{eqn	| r = \map {\paren {f \ast g} } x + \lambda \circ_A \map {\paren {f \ast h} } x
}}
{{end-eqn}}
So $\struct {A^S, +, \circ, \ast}$ is an $R$-algebra. 
{{qed}}
Category:Algebras over Rings
9cjc4zsxo4oy65ndqln8n41kmmr1o9l
Theorem: Linear Combination of Bounded Mappings on Normed Vector Space is Bounded

Let $\struct {R, \norm {\, \cdot \,}_R}$ be a normed division ring.
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $R$. 
Let $S$ be a set.
Let $f, g : S \to X$ be bounded mappings.
Let $\lambda \in R$. 
Then $f + \lambda g$ is bounded.

Proof:
Since $f$ is bounded, there exists a real number $M_1 > 0$ such that:
:$\norm {\map f x} \le M_1$ for each $x \in X$. 
Since $g$ is bounded, there exists a real number $M_2 > 0$ such that:
:$\norm {\map g x} \le M_2$ for each $x \in X$. 
Then from {{NormAxiomVector|3}}, we have:
:$\norm {\map f x + \lambda \map g x} \le \norm {\map f x} + \norm \lambda_R \norm {\map g x}$
for each $x \in X$.
So:
:$\norm {\map f x + \lambda \map g x} \le M_1 + \norm \lambda_R M_2$ for each $x \in X$.
Since $M_1 + \norm \lambda_R M_2 > 0$, we have that $f + \lambda g$ is bounded.
{{qed}}
Category:Bounded Mappings on Normed Vector Spaces
iis3bn7t872849qnsqf30bugufpdvwr
Theorem: Product of Bounded Mappings on Normed Algebra is Bounded

Let $\struct {R, \norm {\, \cdot \,}_R}$ be a normed division ring.
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed algebra over $R$. 
Let $S$ be a set.
Let $f, g : S \to X$ be bounded mappings.
Then $f g$ is bounded.

Proof:
Since $f$ is bounded, there exists a real number $M_1 > 0$ such that:
:$\norm {\map f x} \le M_1$ for each $x \in X$. 
Since $g$ is bounded, there exists a real number $M_2 > 0$ such that:
:$\norm {\map g x} \le M_2$ for each $x \in X$. 
Since $\norm {\, \cdot \,}$ is a algebra norm, we have:
:$\norm {\map f x \map g x} \le \norm {\map f x} \norm {\map g x}$ for each $x \in X$.
So we have:
:$\norm {\map f x \map g x} \le M_1 M_2$
for each $x \in X$. 
Since $M_1 M_2 > 0$, we have that $f g$ is bounded.
{{qed}}
Category:Bounded Mappings on Normed Vector Spaces
sfb9hfg1agxdr4vm6izjanp2vfwh1gf
Theorem: Banach Algebra of Continuous Functions on Compact Hausdorff Space is Banach Algebra

Let $X$ be a compact Hausdorff space.
Let $\map \CC X = \map \CC {X, \C}$ be the vector space of continuous functions on $X$.
Let $\ast$ be pointwise multiplication on $\C^X$. 
Let $\norm {\, \cdot \,}_\infty$ be the supremum norm on $\map \CC X$. 
Then $\struct {\map \CC X, \ast, \norm {\, \cdot \,} }$ is a Banach algebra.

Proof:
We first show that $\struct {\map \CC X, \ast}$ is an algebra over $\C$.
For this, we show that $\struct {\map \CC X, \ast}$ is a subalgebra of $\C^X$.
As shown in Continuous Functions on Compact Space form Banach Space, $\map \CC X$ is a linear subspace of $\C^X$.
From Product of Continuous Functions on Topological Ring is Continuous, we have $f \ast g \in \map \CC X$. 
Hence $\struct {\map \CC X, \ast}$ is a subalgebra of $\C^X$.
Hence $\struct {\map \CC X, \ast}$ is an algebra over $\C$.
From Continuous Functions on Compact Space form Banach Space, $\map \CC X$ is a Banach space. 
It remains to show that $\norm {\, \cdot \,}_\infty$ is a algebra norm on $\map \CC X$. 
That is: 
:$\norm {f \ast g}_\infty \le \norm f_\infty \norm g_\infty$ for each $f, g \in \map \CC X$.
For each $x \in X$, we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x \map g x}
		| r = \cmod {\map f x} \cmod {\map g x}
}}
{{eqn	| o = \le
		| r = \paren {\sup_{x \mathop \in X} \cmod {\map f x} } \cmod {\map g x}
		| c = {{Defof|Supremum of Subset of Real Numbers}}
}}
{{eqn	| o = \le
		| r = \paren {\sup_{x \mathop \in X} \cmod {\map f x} } \paren {\sup_{x \mathop \in X} \cmod {\map g x} }
		| c = {{defof|Supremum of Subset of Real Numbers}}
}}
{{eqn	| r = \norm f_\infty \norm g_\infty
		| c = {{Defof|Supremum Norm}}
}}
{{end-eqn}}
Hence $\struct {\map \CC X, \ast, \norm {\, \cdot \,} }$ is a Banach algebra.
{{qed}}
Category:Banach Algebras
12ryy1dda49s6r3yzd085juldwh7sra
Theorem: Linear Combination of Complex-Valued Functions Vanishing in Neighborhood of Infinity Vanishes in Neighborhood of Infinity

Let $X$ be a locally compact Hausdorff space. 
Let $f, g : X \to \C$ be complex-valued functions vanishing in a neighborhood of infinity.
Let $\lambda \in \C$.
Then $f + \lambda g$ vanishes in a neighborhood of infinity.

Proof:
Since $f$ vanishes in a neighborhood of infinity, there exists a compact set $F_1 \subseteq X$ such that:
:$\map f x = 0$ for each $x \in X \setminus F_1$.
Since $g$ vanishes in a neighborhood of infinity, there exists a compact set $F_2 \subseteq X$ such that:
:$\map g x = 0$ for each $x \in X \setminus F_2$.
From Union of Two Compact Sets is Compact:
:$F_1 \cup F_2$ is compact.
Further:
:$\map f x = 0$ and $\map g x = 0$ for each $x \in X \setminus \paren {F_1 \cup F_2}$. 
So we have:
:$\map f x + \lambda \map g x = 0$ for each $x \in X \setminus \paren {F_1 \cup F_2}$. 
Recalling that $F_1 \cup F_2$ is compact, we have that $f + \lambda g$ vanishes in a neighborhood of infinity.
{{qed}}
Category:Complex-Valued Functions Vanishing in Neighborhood of Infinity
4yexgalytedgjstohyuw98mmt3licol
Theorem: Space of Continuous Functions on Locally Compact Hausdorff Space Vanishing at Infinity is Banach Space

Let $X$ be a locally compact Hausdorff space.
Let $\struct {\map {\CC_0} X, \norm {\, \cdot \,}_\infty}$ be the space of continuous functions on $X$ vanishing at infinity.
Then $\struct {\map {\CC_0} X, \norm {\, \cdot \,}_\infty}$ is a Banach space over $\C$.

Proof:
We first show that $\map {\CC_0} X$ is a vector space. 
From Bounded Continuous Functions on Topological Space form Banach Space, it is enough to show that $\map {\CC_0} X$ is a linear subspace of $\map {\CC_b} X$, where $\map {\CC_b} X$ is the space of bounded continuous functions on $X$ valued in $\C$. 
From Linear Combination of Complex-Valued Functions Vanishing at Infinity Vanishes at Infinity, we have:
:$f + \lambda g \in \map {\CC_0} X$
for $f, g \in \map {\CC_0} X$ and $\lambda \in \C$.
Hence from One-Step Vector Subspace Test, $\map {\CC_0} X$ is a linear subspace of $\map {\CC_b} X$.
Hence $\map {\CC_0} X$ is a vector space. 
Now let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence in $\map {\CC_0} X$ converging to $f \in \map {\CC_b} X$.
From Uniform Limit of Sequence of Continuous Complex-Valued Functions Vanishing at Infinity Vanishes at Infinity, we have $f \in \map {\CC_0} X$. 
From Closed Subspace of Banach Space forms Banach Space, $\struct {\map {\CC_0} X, \norm {\, \cdot \,}_\infty}$ is a Banach space over $\C$.
{{qed}}
Category:Complex-Valued Functions Vanishing at Infinity
Category:Banach Spaces
c69cnpp2db8hnyikm2gsveujo7mh2qv
Theorem: Sequential Characterization of Closed Linear Transformation

Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be Banach spaces.
Let $\map D T$ be a linear subspace of $X$.
Let $T : \map D T \to Y$ be a linear transformation.
Then $T$ is closed {{iff}}:
:for each convergent sequence $\sequence {x_n}_{n \in \N}$ in $\struct {X, \norm {\, \cdot \,}_X}$ valued in $\map D T$ such that $\sequence {T x_n}_{n \in \N}$ converges in $\struct {Y, \norm {\, \cdot \,}_Y}$, we have:
::$\ds \lim_{n \mathop \to \infty} x_n \in \map D T$
:and:
::$\ds \lim_{n \mathop \to \infty} T x_n = \map T {\lim_{n \mathop \to \infty} x_n}$

Proof:
Let $\struct {X \times Y, \norm \cdot_{X \times Y} }$ be the direct product $X \times Y$ equipped with the direct product norm.
From Direct Product of Banach Spaces is Banach Space, $\struct {X \times Y, \norm \cdot_{X \times Y} }$ is a Banach space. 
Let:
:$\map G T = \set {\tuple {x, T x} \in X \times Y : x \in \map D T}$ 
be the graph of $T$.