avewright/proofwiki-math huggingface dataset:
Theorem: Complex Plane is Separable

Let $\struct {\C, \tau_d}$ be the complex number line with the usual (Euclidean) topology.
Then $\struct {\C, \tau_d}$ is separable.

Proof:
{{Recall|Separable Space}}
{{:Definition:Separable Space}}
Consider the set:
:$\Q + i \Q = \set {\alpha + i \beta : \alpha, \beta \in \Q}$ 
which is trivially a subset of $\C$.
We first show that $\Q + i \Q$ is countable.
Define $f : \Q^2 \to \Q + i \Q$ by:
:$\map f {x, y} = x + i y$ for each $x, y \in \Q$. 
This function is evidently surjective.
Further, if $x + i y = a + i b$ for $a, b \in \Q$, we have $x = a$ and $y = b$.
So $f$ is an injection.
From Rational Numbers are Countably Infinite, $\Q$ is countably infinite.
From Cartesian Product of Countable Sets is Countable, $\Q^2$ is countably infinite.
Hence there exists a bijection $g : \N \to \Q^2$.
Then $g \circ f : \N \to \Q + i \Q$ is a bijection.
Hence $\Q + i \Q$ is countably infinite.
We now show that:
:$\Q + i \Q = \set {\alpha + i \beta : \alpha, \beta \in \Q}$
is everywhere dense in $\C$.
Let $x + i y \in \C$.
Let $\epsilon > 0$.
From Rationals are Everywhere Dense in Topological Space of Reals, there exists $\alpha \in \Q$ such that:
:$\cmod {\alpha - x} < \dfrac \epsilon 2$
and:
:$\cmod {\beta - y} < \dfrac \epsilon 2$ 
We therefore have:
{{begin-eqn}}
{{eqn	| l = \cmod {\paren {\alpha + i \beta} - \paren {x + i y} }
		| r = \cmod {\paren {\alpha - x} + i \paren {\beta - y} }
}}
{{eqn	| o = \le
		| r = \cmod {\alpha - x} + \cmod i \cmod {\beta - y}
		| c = Triangle Inequality for Complex Numbers
}}
{{eqn	| o = <
		| r = \frac \epsilon 2 + \frac \epsilon 2 
}}
{{eqn	| r = \epsilon 
}}
{{end-eqn}}
Since $x + i y \in \C$ was arbitrary and $\alpha + i \beta \in \Q + i \Q$, we have that $\Q + i \Q$ is everywhere dense in $\C$. 
{{qed}}
Category:Complex Plane
Category:Separable Spaces
qz4wbyjea7qgjrbpm0l3ulld430dg41
Theorem: Quotient of Banach Space by Topologically Complemented Subspace is Linearly Isomorphic to Topological Complement

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $Y$ be a closed vector subspace of $X$ that is topologically complemented.
From Closed Subspace of Banach Space is Topologically Complemented iff has Topological Complement, $Y$ has a topological complement $Z$.
Let $\struct {X/Y, \norm {\, \cdot \,}_{X/Y} }$ be the normed quotient vector space of $X$ modulo $Y$. 
Then $\struct {X/Y, \norm {\, \cdot \,}_{X/Y} }$ is linearly isomorphic to $Z$.

Proof:
Let $\pi : X \to X/Y$ be the quotient mapping.
Let $\pi_Z : Z \to X/Y$ be the restriction of $\pi$ to $Z$.
From Quotient Mapping is Bounded in Normed Quotient Vector Space, $\pi_Z$ is a bounded linear transformation.
We argue that $\pi_Z$ is our desired linear isomorphism.
For this, we will apply the Banach Isomorphism Theorem. 
We first show that $\pi_Z$ is an injection.
Let $z_1, z_2 \in Z$ be such that $\map {\pi_Z} {z_1} = \map {\pi_Z} {z_2}$.
That is, since $\pi_Z$ is a linear, we have that $\map {\pi_Z} {z_1 - z_2} = {\mathbf 0}_{X/Y}$.
From Kernel of Quotient Mapping, we have that $z_1 - z_2 \in Y$. 
Further, $z_1 - z_2 \in Z$.
Hence $z_1 - z_2 \in Y \cap Z$.
From the definition of the topological complement, we have that $Y \cap Z = \set { {\mathbf 0}_X}$.
So $z_1 = z_2$.
Hence $\pi$ is injective.
We now show that $\pi_Z$ is surjective.
Let $\map \pi x \in X/Y$.
We can write:
:$x = y + z$ 
for some $y \in Y$ and $z \in Z$, by the definition of the topological complement.
We then have:
{{begin-eqn}}
{{eqn	| l = \map \pi x
		| r = \map \pi {y + z}
}}
{{eqn	| r = \map \pi y + \map \pi z
		| c = Quotient Mapping is Linear Transformation
}}
{{eqn	| r = \map \pi z 
		| c = Kernel of Quotient Mapping, since $y \in Y$ 
}}
{{eqn	| r = \map {\pi_Z} z
		| c = definition of $\pi_Z$ 
}}
{{end-eqn}}
Hence $\pi_Z$ is surjective.
Since $\pi_Z$ is a bijective bounded linear transformation, it follows that:
:$\pi_Z : Z \to \struct {X/Y, \norm {\, \cdot \,}_{X/Y} }$ is a linear isomorphism
by the Banach Isomorphism Theorem.
Hence $A$ and $\struct {X/Y, \norm {\, \cdot \,}_{X/Y} }$ are linearly isomorphic.
{{qed}}
Theorem: Linear Isomorphic Image of Complemented Subspace of Banach Space is Complemented

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be Banach spaces over $\GF$ such that:
:there exists a linear isomorphism $T : X \to Y$. 
Let $X_1$ be a complemented subspace of $X$ with topological complement $X_2$.
Then $T \sqbrk {X_1}$ is a complemented subspace of $Y$ with topological complement $T \sqbrk {X_2}$.

Proof:
By the definition of a complemented subspace, we have:
:$X = X_1 + X_2$
with:
:$X_1 \cap X_2 = \set { {\mathbf 0}_X}$
We show that:
:$Y = T \sqbrk {X_1} + T \sqbrk {X_2}$
and:
:$T \sqbrk {X_1} \cap T \sqbrk {X_2} = \set { {\mathbf 0}_Y}$
Let $y \in Y$.
Since $T$ is a linear isomorphism, there exists $x \in X$ such that $y = T x$.
Since:
:$X = X_1 + X_2$
there exists $x_1 \in X_1$ and $x_2 \in X_2$ with:
:$x = x_1 + x_2$
Since $T$ is linear, we therefore have:
:$y = T x = \map T {x_1 + x_2} = T x_1 + T x_2$
with:
:$T x_1 \in T \sqbrk {X_1}$
and:
:$T x_2 \in T \sqbrk {X_2}$
We therefore have:
:$Y = T \sqbrk {X_1} + T \sqbrk {X_2}$
We also have:
{{begin-eqn}}
{{eqn	| l = T \sqbrk {X_1} \cap T \sqbrk {X_2}
		| r = T \sqbrk {X_1 \cap X_2}
		| c = Image of Intersection under Injection
}}
{{eqn	| r = T \sqbrk {\set { {\mathbf 0}_X} }
		| c = since $X_1 \cap X_2 = \set { {\mathbf 0}_X}$
}}
{{eqn	| r = \set {\map T { {\mathbf 0}_X} }
}}
{{eqn	| r = \set { {\mathbf 0}_Y}
}}
{{end-eqn}}
Hence:
:$Y = T \sqbrk {X_1} \oplus T \sqbrk {X_2}$
where $\oplus$ denotes the internal direct sum.
{{qed}}
Theorem: Normalized Block Basic Sequence of Schauder Basis in P-Sequence Space is Isometrically Equivalent to Schauder Basis

Let $\GF \in \set {\R, \C}$.
Let $p \in \hointr 1 \infty$.
Let $\struct {\map {\ell_p} \GF, \norm {\, \cdot \,}_p}$ be the $p$-sequence space.
Let $\sequence {e_n}_{n \mathop \in \N}$ be the Schauder basis given by P-Sequence Space admits Schauder Basis.
Let $\sequence {y_k}_{k \mathop \in \N}$ be a block basic sequence of $\sequence {e_n}_{n \mathop \in \N}$ with:
:$\norm {y_k}_p = 1$ for each $k \in \N$. 
Then $\sequence {y_k}_{k \mathop \in \N}$ is isometrically equivalent to $\sequence {e_n}_{n \mathop \in \N}$.

Proof:
Let $\sequence {r_j}_{j \mathop \in \N}$ be a strictly increasing sequence in $\N$ and $\sequence {a_j}_{j \mathop \in \N}$ be a sequence in $\GF$ such that:
:$\ds y_k = \sum_{j \mathop = r_{k - 1} + 1}^{r_k} a_j e_j$
where $r_0 = 0$.
By assumption, we have:
:$\ds 1 = \norm {y_k}_p^p = \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \cmod {a_j}^p$
Let $\struct {\map {c_{00} } \GF, \norm {\, \cdot \,}_\infty}$ be the space of almost-zero sequences.
By Characterization of Isometric Equivalence of Basic Sequences, it is enough to show that:
:$\ds \norm {\sum_{k \mathop = 1}^\infty \map \xi k y_k}_p = \norm {\sum_{k \mathop = 1}^\infty \map \xi k e_k}_p = \paren {\sum_{k \mathop = 1}^\infty \cmod {\map \xi k}^p}^{1/p}$ for each $\xi \in \map {c_{00} } \GF$.
We have:
:$\ds \norm {\sum_{k \mathop = 1}^\infty \map \xi k y_k}_p = \norm {\sum_{k \mathop = 1}^\infty \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \map \xi k a_j e_j}_p$
Note that the coefficient of $e_j$ is $\map \xi k a_j$ for $r_{k - 1} + 1 \le j \le r_k$. 
Hence we have:
{{begin-eqn}}
{{eqn	| l = \norm {\sum_{k \mathop = 1}^\infty \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \map \xi k a_j e_j}_p 
		| r = \paren {\sum_{k \mathop = 1}^\infty \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \cmod {\map \xi k}^p \cmod {a_k}^p}^{1/p}
}}
{{eqn	| r = \paren {\sum_{k \mathop = 1}^\infty \cmod {\map \xi j}^p \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \cmod {\map \xi k}^p \cmod {a_k}^p}^{1/p}
}}
{{eqn	| r = \paren {\sum_{k \mathop = 1}^\infty \cmod {\map \xi j}^p}^{1/p}
		| c = since $\ds \sum_{j \mathop = r_{k - 1} + 1}^{r_k} \cmod {a_j}^p = 1$
}}
{{end-eqn}}
for each $\xi \in \map {c_{00} } \GF$.
Hence:
:$\ds \norm {\sum_{k \mathop = 1}^\infty \map \xi k y_k}_p = \norm {\sum_{k \mathop = 1}^\infty \map \xi k e_k}_p = \paren {\sum_{k \mathop = 1}^\infty \cmod {\map \xi k}^p}^{1/p}$ for each $\xi \in \map {c_{00} } \GF$.
Hence by Characterization of Isometric Equivalence of Basic Sequences, we have that $\sequence {y_k}_{k \mathop \in \N}$ is isometrically equivalent to $\sequence {e_n}_{n \mathop \in \N}$.
{{qed}}
Theorem: Inverse Image Mapping of Identity is Identity

Let $S$ be a set.
Then:
:$\paren{I_S}^\gets = I_{\powerset S}$
where:
:$I_S$ denotes the identity mapping on $S$
:$\paren{I_S}^\gets$ denotes the inverse image mapping of $I_S$
:$\powerset S$ denotes the powerset of $S$
:$I_{\powerset S}$ denotes the identity mapping on $\powerset S$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \paren{I_S}^\gets
      | r = \paren{\paren{I_S}^\to}^{-1}
      | c = Identity Mapping is Bijection, Inverse Image Mapping of Bijection is Inverse of Direct Image Mapping
}}
{{eqn | r = \paren{I_{\powerset S} }^{-1}
      | c = Direct Image Mapping of Identity is Identity
}}
{{eqn | r = I_{\powerset S}
      | c = Inverse of Identity Mapping
}}
{{end-eqn}}
{{qed}}
Category:Inverse Image Mappings
Category:Identity Mappings
Category:Power Set
aczf3gsva606l7x3go3bnogf2sg7pim
Theorem: Restriction of Identity Mapping is Identity Mapping

Let $S$ be a set.
Let $A$ be a subset of $S$.
Then:
:$I_S \restriction_{A \times A} = I_A$
where:
:$I_S$ denotes the identity mapping on $S$
:$I_S \restriction_{A \times A}$ denotes the restriction of $I_S$ to $A \times A$
:$I_A$ denotes the identity mapping on $A$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall a \in A
      | l = \map {\paren{I_S \restriction_{A \times A} } } a
      | r = \map {I_S} a
      | c = {{Defof|Restricted Mapping}}
}}
{{eqn | r = a
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \map {I_A} a
      | c = {{Defof|Identity Mapping}}
}}
{{end-eqn}}
From Equality of Mappings:
:$I_S \restriction_{\paren{A \times A}} = I_A$
{{qed}}
Category:Identity Mappings
Category:Restrictions
pgrb4t0xo4y388vlltsucrrbd7fyptf
Theorem: Characterization of Isometric Equivalence of Basic Sequences

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be Banach spaces over $\GF$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a basic sequence in $X$.
Let $\sequence {y_n}_{n \mathop \in \N}$ be a basic sequence in $Y$. 
Let $\struct {\map \BB {\sqbrk {x_n}_{n \mathop \in \N}, \sqbrk {y_n}_{n \mathop \in \N} }, \norm {\, \cdot \,}_{\map \BB {\sqbrk {x_n}_{n \mathop \in \N}, \sqbrk {y_n}_{n \mathop \in \N} } } }$ and $\struct {\map \BB {\sqbrk {y_n}_{n \mathop \in \N}, \sqbrk {x_n}_{n \mathop \in \N} }, \norm {\, \cdot \,}_{\map \BB {\sqbrk {y_n}_{n \mathop \in \N}, \sqbrk {x_n}_{n \mathop \in \N} } } }$ be the space of bounded linear transformations $\sqbrk {x_n}_{n \mathop \in \N} \to \sqbrk {y_n}_{n \mathop \in \N}$ and $\sqbrk {y_n}_{n \mathop \in \N} \to \sqbrk {x_n}_{n \mathop \in \N}$ respectively. 
Let $\struct {\map {c_{00} } \GF, \norm {\, \cdot \,}_\infty}$ be the space of almost-zero sequences.
We have that $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ are isometrically equivalent {{iff}}:
:$\ds \norm {\sum_{j \mathop = 1}^\infty \map \xi j x_j}_X = \norm {\sum_{j \mathop = 1}^\infty \map \xi j y_j}_Y$ for all $\xi \in \map {c_{00} } \GF$.

Proof:
We have that $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ are isometrically equivalent {{iff}}:
:there exists an isometric isomorphism $T : \sqbrk {x_n}_{n \mathop \in \N} \to \sqbrk {y_n}_{n \mathop \in \N}$ such that:
::$T x_n = y_n$ for each $n \in \N$.
From Invertible Bounded Linear Transformation with Norm and Norm of Inverse Bounded Above by One is Isometric Isomorphism, $T$ is an isometric isomorphism {{iff}}:
:$\norm T_{\map \BB {\sqbrk {x_n}_{n \mathop \in \N}, \sqbrk {y_n}_{n \mathop \in \N} } } \le 1$ 
and:
:$\norm {T^{-1} }_{\map \BB {\sqbrk {y_n}_{n \mathop \in \N}, \sqbrk {x_n}_{n \mathop \in \N} } } \le 1$ 
From Basic Sequences in Banach Spaces are Equivalent iff Map between is Linear Isomorphism: Corollary, this is equivalent to:
:$\ds \norm {\sum_{j \mathop = 1}^\infty \map \xi j y_j}_Y \le \norm {\sum_{j \mathop = 1}^\infty \map \xi j x_j}_X \le \norm {\sum_{j \mathop = 1}^\infty \map \xi j y_j}$ for each $\xi \in \map {c_{00} } \GF$.
That is, equivalent to:
:$\ds \norm {\sum_{j \mathop = 1}^\infty \map \xi j x_j}_X = \norm {\sum_{j \mathop = 1}^\infty \map \xi j y_j}_Y$ for $\xi \in \map {c_{00} } \GF$.
{{qed}}
Category:Basic Sequences
bmd0p180rov4z71pkrfkbblbaajvpfu
Theorem: There Exist a Countable Number of Computable Numbers

The computable numbers form a countably infinite set.

Proof:
Let $S$ be the set of computable numbers.
From Rational Number is Computable, we know that $S$ is at least countably infinite.
{{Recall|Computable Number|computable number}}
{{:Definition:Computable Number}}
Such an algorithm can be implemented by a computer program.
The set of computer programs that compute computable numbers is a subset of the set of finite strings.
From Set of Finite Strings is Countably Infinite, the set of expressions that can be formed from a finite alphabet is countably infinite.
Hence $S$ is at most countably infinite.
The result follows.
{{qed}}
Theorem: Almost All Real Numbers are Not Computable

Almost all real numbers are not computable.

Proof:
Let $S$ be the set of computable numbers.
From There Exist a Countable Number of Computable Numbers, $S$ is countably infinite.
From Real Numbers are Uncountable, the set of real numbers $\R$ is uncountable.
The result follows by definition of almost all.
{{qed}}
Theorem: Product Law of Independent Events

Let $\EE$ be an experiment with probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $A, B \in \Sigma$ be events of $\EE$ such that $\map \Pr A > 0$ and $\map \Pr B > 0$.
Let $A$ and $B$ be independent of each other.
Then:
:$\map \Pr {A \cap B} = \map \Pr A \map \Pr B$

Proof:
{{begin-eqn}}
{{eqn | l = \condprob A B
      | r = \map \Pr A
      | c = {{Defof|Independent Events|index = 1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac {\map \Pr {A \cap B} } {\map \Pr B}
      | r = \map \Pr A
      | c = {{Defof|Conditional Probability}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \Pr {A \cap B}
      | r = \map \Pr A \, \map \Pr B
      | c = which is valid, as $\map \Pr B > 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Conic Section/Cartesian Form/Circle

Let $a = b$ and $h = 0$.
Then $\CC$ is a circle.

Proof:
When $a = b$ and $h = 0$, $(1)$ becomes:
:$a \paren {x^2 + y^2} + 2 g x + 2 f y + c = 0$
which is in the form specified in formulation $2$ of Equation of Circle.
{{qed}}
Theorem: Moment of Inertia of Uniform Rectangular Lamina about Edge

Let $\LL$ be a uniform lamina of mass $M$ in the shape of a rectangle whose sides are of length $2 a$ and $2 b$.
Let $\AA$ be the straight line passing through the side of $\LL$ of length $2 b$.
Then the moment of inertia $\II$ of $\LL$ about $\AA$ is given by:
:$\II = \dfrac {4 M a^2} 3$

Proof:
Let $\AA'$ be the straight line:
:through the centroid of $\LL$
:in the plane of $\LL$
:perpendicular to the side of $\LL$ of length $2 a$.
Let $\II'$ be the moment of inertia of $\RR$ about $\AA'$.
We note that:
:$\AA'$ is parallel to $\AA$
:$\AA$ and $\AA'$ are at a distance $a$ apart.
Then:
{{begin-eqn}}
{{eqn | l = \II'
      | r = \dfrac {M a^2} 3
      | c = Moment of Inertia of Uniform Rectangular Lamina about Axis in Plane Bisecting Lamina
}}
{{eqn | l = \II
      | r = \II' + M a^2
      | c = Huygens-Steiner Theorem
}}
{{eqn | r = \dfrac {M a^2} 3 + M a^2
      | c = 
}}
{{eqn | r = \dfrac {4 M a^2} 3
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Moment of Inertia of Uniform Hoop about Diameter

Let $\HH$ be a hoop of uniform density of radius $r$ and mass $M$.
Let $\DD$ be a straight line through a diameter of $\HH$.
Then the moment of inertia $\II$ of $\HH$ about $\DD$ is given by:
:$\II = \dfrac {M r^2} 2$

Proof:
Let $\AA$ denote the axis of $\HH$.
Let $\DD_1$ and $\DD_2$ be two distinct diameters of $\HH$.
Let the moments of inertia of $\HH$ about $\DD_1$ and $\DD_2$ be $\II_1$ and $\II_2$.
By symmetry, $\II_1 = \II_2$ and both are equal to $\II$.
Let $\II_a$ be the moment of inertia of $\HH$ about $\AA$.
We note that $\AA$ is perpendicular to both $\DD_1$ and $\DD_2$.
We have:
{{begin-eqn}}
{{eqn | l = \II_a
      | r = M r^2
      | c = Moment of Inertia of Uniform Hoop about Axis
}}
{{eqn | l = \II_a
      | r = \II_1 + \II_2
      | c = Perpendicular Axes Theorem
}}
{{eqn | r = 2 \II
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \II
      | r = \dfrac {\II_a} 2
      | c = 
}}
{{eqn | r = \dfrac {M r^2} 2
      | c = Moment of Inertia of Uniform Hoop about Axis: $\II_a = M r^2$
}}
{{end-eqn}}
{{qed}}
Theorem: Cardinality of Conjugacy Class is Divisor of Order of Group

Let $G$ be a group.
For $x \in G$, let $\conjclass x$ denote the conjugacy class of $x$.
Then the cardinality of $\conjclass x$ is a divisor of the order of $G$.

Proof:
{{ProofWanted|Follows obviously enough from Size of Conjugacy Class is Index of Normalizer}}
Theorem: Product of Conjugate Quadratic Irrationals

Let $a + \sqrt b$ and $a - \sqrt b$ be conjugate quadratic irrationals.
Then their product is rational:
:$\paren {a + \sqrt b} \paren {a - \sqrt b} = a^2 - b$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a + \sqrt b} \paren {a - \sqrt b}
      | r = a^2 - \paren {\sqrt b}^2
      | c = Difference of Two Squares
}}
{{eqn | r = a^2 - b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Conjugate Quadratic Irrationals

Let $a + \sqrt b$ and $a - \sqrt b$ be conjugate quadratic irrationals.
Then their sum is rational:
:$\paren {a + \sqrt b} + \paren {a - \sqrt b} = 2 a$

Proof:
Simple algebra.
{{qed}}
Theorem: Epimorphism in Isomorphic Category

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ be an isomorphism of categories.
Let $f$ be a morphism of $\mathbf C$.
Then $f$ is an epimorphism in $\mathbf C$ {{iff}} $Ff$ is an epimorphism in $\mathbf D$.

Proof:
Let $G: \mathbf D \to \mathbf C$ denote the inverse of $F$.
By definition of inverse Isomorphism of categories:
:$G F: \mathbf C \to \mathbf C$ is the identity functor $\operatorname{id}_{\mathbf C}$
:$F G: \mathbf D \to \mathbf D$ is the identity functor $\operatorname{id}_{\mathbf D}$
Theorem: Monomorphism in Isomorphic Category

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ be an isomorphism of categories.
Let $f$ be a morphism of $\mathbf C$.
Then $f$ is a monomorphism in $\mathbf C$ {{iff}} $Ff$ is a monomorphism in $\mathbf D$.

Proof:
Let $G: \mathbf D \to \mathbf C$ denote the inverse of $F$.
By definition of inverse Isomorphism of categories:
:$G F: \mathbf C \to \mathbf C$ is the identity functor $\operatorname{id}_{\mathbf C}$
:$F G: \mathbf D \to \mathbf D$ is the identity functor $\operatorname{id}_{\mathbf D}$
Theorem: Connected Component is not necessarily Open

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq T$ be a connected component of $T$.
Then it is not necessarily the case that $H$ is open.

Proof:
Let $T = \struct {\Q, \tau_d}$ be the rational number space formed by the rational numbers $\Q$ under the usual (Euclidean) topology $\tau_d$.
Let $x \in \Q$.
From Components of Rational Number Space are Singletons, $\set x$ is a connected component of $T$.
{{finish|Need to establish that $\set x$ is not an open set of $\Q$.}}
Theorem: Connected Space is not necessarily Path-Connected

Let $T$ be a topological space which is connected.
Then it is not necessarily the case that $T$ is path-connected.

Proof:
Let $T$ be the closed topologist's sine curve.
From Closed Topologist's Sine Curve is not Path-Connected, $T$ is path-connected.
From Closed Topologist's Sine Curve is Connected, $T$ is connected.
Hence the result.
{{qed}}
Theorem: Isomorphism in Isomorphic Category

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $F: \mathbf C \to \mathbf D$ be an isomorphism of categories.
Let $f$ be a morphism of $\mathbf C$.
Then $f$ is an isomorphism in $\mathbf C$ {{iff}} $Ff$ is an isomorphism in $\mathbf D$.

Proof:
Let $G: \mathbf D \to \mathbf C$ denote the inverse of $F$.
By definition of inverse Isomorphism of categories:
:$G F: \mathbf C \to \mathbf C$ is the identity functor $\operatorname{id}_{\mathbf C}$
:$F G: \mathbf D \to \mathbf D$ is the identity functor $\operatorname{id}_{\mathbf D}$
Theorem: Ultrafilter is Principal iff Contains a Finite Set

Let $\UU \subseteq \powerset S$ be a ultrafilter on $S$.
Then:
:$\UU$ is principal
{{iff}}:
:there is a finite $A \in \UU$

Proof:
=== Necessary Condition ===
By Filter is Principal Ultrafilter iff Contains Singleton, there is some $x \in S$ such that:
:$\set x \in \UU$
Putting $A = \set x$, the result follows from Singleton is Finite.
{{qed|lemma}}
Theorem: Filter is Principal Ultrafilter iff Contains Singleton

Let $\FF \subseteq \powerset S$ be a filter on $S$.
Then:
:$\FF$ is a principal ultrafilter on $S$
{{iff}}:
:$\set x \in \FF$ for some $x \in S$

Proof:
=== Necessary Condition ===
Suppose $\FF$ is a principal ultrafilter on $S$.
By definition, it has a cluster point $x \in S$.
By Principal Ultrafilter is All Sets Containing Cluster Point, we have in particular that:
:$\set x \in S$
{{qed|lemma}}
Theorem: Filter Contains no Disjoint Sets

Let $\FF \subseteq \powerset S$ be a filter on $S$.
Let $A, B \subseteq S$ be disjoint.
Then, at most one of $A$ or $B$ is an element of $\FF$.

Proof:
{{AimForCont}} both $A \in \FF$ and $B \in \FF$.
Then, by filter axiom $\text F 3$:
:$A \cap B \in \FF$
But:
:$A \cap B = \O$
by definition of disjoint, which contradicts filter axiom $\text F 2$.
The result follows by Proof by Contradiction.
{{qed}}
Category:Filter Theory
8k8gcblt5ciuoa8brbmedi1jfx9256m
Theorem: Ultrafilter Contains Set or Complement

Let $\UU \subseteq \powerset S$ be a ultrafilter on $S$.
Let $A \subseteq S$.
Then, exactly one of $A$ and $\relcomp S A$ is an element of $\UU$.

Proof:
At least one is an element by definition of an ultrafilter.
Moreover, at most one is by Filter Contains no Disjoint Sets, since:
:$A \cap \relcomp S A = \O$
The result follows.
{{qed}}
Category:Ultrafilters on Sets
nr1pvkot0ch2je8rzkjs3b0rx6mhrni
Theorem: Ultrafilter is Nonprincipal iff Contains Fréchet Filter

Let $\UU \subseteq \powerset S$ be an ultrafilter on $S$.
Then:
:$\UU$ is nonprincipal
{{iff}}:
:$\FF \subseteq \UU$, where $\FF$ is the Fréchet filter on $S$.

Proof:
By Ultrafilter Contains Set or Complement, we have that:
:$A \notin \UU \iff \relcomp S A \in \UU$
for each $A \subseteq S$.
Considering $A$ to range over all finite subsets of $S$, we find that:
:$A \notin \UU$ for every finite $A \subseteq S$
{{iff}}:
:$\relcomp S A \in \UU$ for every finite $A \subseteq S$
But the latter is equivalent to:
:$B \in \UU$ for every cofinite $B$ in $S$
which is to say:
:$\FF \subseteq \UU$
where $\FF$ is the Fréchet filter on $S$.
So, it suffices to show that:
:$\UU$ is nonprincipal
{{iff}}:
:there is no finite $A \in \UU$
But this follows from Ultrafilter is Principal iff Contains a Finite Set by Biconditional Equivalent to Biconditional of Negations.
{{qed}}
Category:Fréchet Filters
Category:Nonprincipal Ultrafilters
Category:Ultrafilters on Sets
brvt0nx8mtnhr4v6hp9m0oseh3pw4xt