avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Subfamily of Cardinality not greater than Weight of Space and Unions Equal

Let $T$ be a topological space.
Let $\FF$ be a set of open sets of $T$.
There exists a subset $\GG \subseteq \FF$ such that:
:$\ds \bigcup \GG = \bigcup \FF$
and:
:$\card \GG \le \map w T$
where:
:$\map w T$ denotes the weight of $T$
:$\card \GG$ denotes the cardinality of $\GG$.

Proof:
By definition of weight of $T$ there exists a basis $\BB$ of $T$ such that:
:$(1): \quad \card \BB = \map w T$
Let:
:$\BB_1 = \set {W \in \BB: \exists U \in \FF: W \subseteq U}$
By definition of subset:
:$\BB_1 \subseteq \BB$
Then by Subset implies Cardinal Inequality:
:$(2): \quad \card {\BB_1} \le \card \BB$
By definition of set $\BB_1$:
:$\forall W \in \BB_1: \exists U \in \FF: W \subseteq U$
Then by the Axiom of Choice there exists a mapping $f$ from $\BB_1$ into $\FF$ such that
:$(3): \quad \forall U \in \BB_1: U \subseteq f \sqbrk U$
Let:
:$\GG = \Img f$
where $\Img f$ denotes the image of $f$.
By hypothesis:
:$\GG \subseteq \FF$
Then by Union of Subset of Family is Subset of Union of Family:
:$\ds \bigcup \GG \subseteq \bigcup \FF$
By definition of set equality, to prove $\ds \bigcup \GG = \bigcup \FF$ it is sufficient to show:
:$\ds \bigcup \FF \subseteq \bigcup \GG$
Let $\ds x \in \bigcup \FF$.
By definition of union there exists a set $A$ such that:
:$A \in \FF$ and $x \in A$
Because $A$ is open, then by definition of basis there exists $U \in \BB$ such that:
:$x \in U \subseteq A$
By definition of the set $\BB_1$:
:$U \in \BB_1$
Because $\GG = \Img f$:
:$f \sqbrk U \in \GG$
By $(3)$ and Set is Subset of Union:
:$\ds U \subseteq f \sqbrk U \subseteq \bigcup \GG$
Thus by definition of subset:
:$\ds x \in \bigcup \GG$
This ends the proof of inclusion.
By Cardinality of Image of Mapping not greater than Cardinality of Domain:
:$\card {\Img f} \le \card {\BB_1}$
Thus by $(1)$ and $(2)$:
:$\card \GG \le \map w T$
{{qed}}
Theorem: Set of Singletons is Smallest Basis of Discrete Space

Let $T = \struct {S, \tau}$ be a discrete topological space.
Let $\BB = \set {\set x : x \in S}$.
Then $\BB$ is the smallest basis of $T$.
That is:
:$\BB$ is a basis of $T$
and:
:for every basis $\CC$ of $T$, $\BB \subseteq \CC$.

Proof:
By Basis for Discrete Topology $\BB$ is a basis of $T$.
It remains to be shown that $\BB$ is the smallest basis of $T$.
Let $\CC$ be a basis of $T$.
Let $A \in \BB$.
By definition of the set $\BB$:
:$\exists x \in S: A = \set x$
By definition of basis:
:$\exists B \in \CC: x \in B \subseteq A$
Then by Singleton of Element is Subset:
:$\set x \subseteq B$
Hence $B = A$ by definition of set equality.
Thus $A \in \CC$.
{{qed}}
Theorem: Conditional and Inverse are not Equivalent

A conditional statement:
:$p \implies q$
is not logically equivalent to its inverse:
:$\lnot p \implies \lnot q$

Proof:
We apply the Method of Truth Tables to the proposition:
:$\paren {p \implies q} \iff \paren {\lnot p \implies \lnot q}$
$\begin{array}{|ccc|c|ccc|} \hline
p & \implies & q) & \iff & (\lnot & p & \implies & \lnot & q) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
{{qed}}
Theorem: Weight of Discrete Topology equals Cardinality of Space

Let $T = \struct {S, \tau}$ be a discrete topological space.
Then:
:$\map w T = \size S$
where:
:$\map w T$ denotes the weight of $T$
:$\card S$ denotes the cardinality of $S$.

Proof:
By Basis for Discrete Topology the set $\BB = \set {\set x: x \in S}$ is a basis of $T$.
By Set of Singletons is Smallest Basis of Discrete Space $\BB$ is smallest basis of $T$:
:for every basis $\CC$ of $T$, $\BB \subseteq \CC$.
Then by Subset implies Cardinal Inequality:
:for every basis $\CC$ of $T$, $\card \BB \le \card \CC$.
Hence $\card \BB$ is the minimal cardinality of a basis of $T$:
:$\map w T = \card \BB$ by definition of weight.
Thus by Cardinality of Set of Singletons:
:$\map w T = \card S$
{{qed}}
Theorem: Cardinality of Set of Singletons

Let $S$ be a set.
Let $T = \set {\set x: x \in S}$ be the set of all singletons of elements of $S$.
Then:
:$\card T = \card S$
where $\card S$ denotes the cardinality of $S$.

Proof:
Define a mapping $f: S \to T$:
:$\forall x \in S: \map f x = \set x$
By Singleton Equality:
:$\forall x, y \in S: \map f x = \map f y \implies x = y$
Then, by definition, $f$ is an injection.
By the definition of set $T$:
:$\forall y \in T: \exists x \in S: y = \map f x$
Then, by definition, $f$ is a surjection.
Hence, by definition, $f: S \to T$ is a bijection.
Thus, by definition, $S$ and $T$ are equivalent:
:$S \sim T$
Thus by definition of cardinality:
:$\card T = \card S$
{{qed}}
Theorem: Basis has Subset Basis of Cardinality equal to Weight of Space

Let $T = \struct {X, \tau}$ be a topological space.
Let $\BB$ be a basis of $T$.
Then there exists a basis $\BB_0$ of $T$ such that
:$\BB_0 \subseteq \BB$ and $\card {\BB_0} = \map w T$
where:
:$\card {\BB_0}$ denotes the cardinality of $\BB_0$
:$\map w T$ denotes the weight of $T$.

Proof:
There are two cases: 
:infinite weight
:finite weight.
Theorem: Cardinality of Union not greater than Product

Let $\FF$ be a set of sets.
Let:
:$\size \FF \le \mathbf m$
where 
:$\size \FF$ denotes the cardinality of $\FF$
:$\mathbf m$ is cardinal number (possibly infinite).
Let:
:$\forall A \in \FF: \size A \le \mathbf n$
where
:$\mathbf n$ is cardinal number (possibly infinite).
Then:
:$\ds \size {\bigcup \FF} \le \size {\mathbf m \times \mathbf n} = \mathbf m \mathbf n$

Proof:
$\FF = \O$ or $\FF = \set \O$ or $\O \ne \FF \ne \set \O$.
In case when $\FF = \O$ or $\FF = \set \O$:
{{begin-eqn}}
{{eqn | l = \size {\bigcup \FF}
      | r = \size \O
      | c = Union of Empty Set, Union of Singleton
}}
{{eqn | o = \le
      | r = \size {\mathbf m \times \mathbf n}
      | c = Subset implies Cardinal Inequality because Empty Set is Subset of All Sets
}}
{{end-eqn}}
In case when $\O \ne \FF \ne \{\O\}$:
:by Surjection iff Cardinal Inequality there exists a surjection $f: \mathbf m \to \FF$ as $\size {\mathbf m} = \mathbf m$ by Cardinal of Cardinal Equal to Cardinal.
$\FF$ contains non empty set $A_0$.
:$\size {A_0} > \mathbf 0$.
By assumption:
:$\size {A_0} \le \mathbf n$.
Then:
:$\mathbf 0 < \mathbf n$.
Hence:
:$\size {\set 0} = \mathbf 1 \le \mathbf n$.
Define a family $\family {B_A}_{A \mathop \in \FF}$:
:$B_A = \begin{cases} A & A \ne \O \\ \set 0 & A = \O \end {cases}$
By Surjection iff Cardinal Inequality define a family
$\family {g_A}_{A \mathop \in \FF}$ of surjections:
:$\forall A \in \FF: g_A: \mathbf n \to B_A$ is a surjection.
Define a mapping $h:\mathbf m \times \mathbf n \to \ds \bigcup_{A \mathop \in \FF} B_A$:
:$\forall \alpha \in \mathbf m: \forall \beta \in \mathbf n: \map h {\alpha, \beta} = \map {g_{\map f \alpha} } \beta$
We will show by definition that $h$ is a surjection.
Let $x \in \ds \bigcup_{A \mathop \in \FF} B_A$.
Then by definition of union:
:$\exists A \in \FF: x \in B_A$.
By definition of surjection:
:$\exists \alpha \in \mathbf m: \map f \alpha = A$.
By definition of surjection:
:$\exists \beta \in \mathbf n: \map {g_A} \beta = x$
So:
:$\map h {\alpha, \beta} = \map {g_{\map f \alpha} } \beta = x$
This ends the proof of surjection.
Hence by Surjection iff Cardinal Inequality:
:$\ds \size {\bigcup_{A \mathop \in \FF} B_A} \le \size {\mathbf m \times \mathbf n}$
By definition of subset:
:$\forall A \in \FF: A \subseteq B_A$.
Then by Set Union Preserves Subsets:
:$\ds \bigcup \FF \subseteq \bigcup_{A \mathop \in \FF} B_A$.
Hence by Subset implies Cardinal Inequality:
:$\ds \size {\bigcup \FF} \le \ds \size {\bigcup_{A \mathop \in \FF} B_A}$
Thus the result:
:$\size {\bigcup \FF} \le \size {\mathbf m \times \mathbf n}$
Thus by definition of product of cardinals:
:$\size {\mathbf m \times \mathbf n} = \mathbf m \mathbf n$
{{qed}}
Theorem: Image of Mapping of Intersections is Smallest Basis

Let $T = \struct {X, \tau}$ be a topological space.
Let $f: X \to \tau$ be a mapping such that:
:$\forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$.
Then the image $\Img f$ is subset of every basis of $T$.

Proof:
Let $\BB$ be a basis.
Let $V \in \Img f$.
Then by definition of image there exists a point $b \in X$ such that:
:$V = \map f b$
Then $V$ is open because $\Img f \subseteq \tau$.
By assumption of mapping $f$:
:$b \in V$
Then by definition of basis there exists a subset $U \in \BB$ such that:
:$b \in U \subseteq V$
By definition of basis:
:$\BB \subseteq \tau$
Then by definition of subset:
:$U \in \tau$
Then by assumption of mapping $f$:
:$\map f b \subseteq U$
Thus by definition of set equality:
:$V = U \in \BB$
{{qed}}
Theorem: Cardinality of Image of Mapping of Intersections is not greater than Weight of Space

Let $T = \struct {X, \tau}$ be a topological space.
Let $f: X \to \tau$ be a mapping such that:
:$\forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$
Then the cardinality of the image of $f$ is no greater than the weight of $T$:
:$\card {\Img f} \le \map w T$

Proof:
By definition of weight, there exists a basis $\BB$ of $T$ such that:
:$\card \BB = \map w T$
By Image of Mapping of Intersections is Smallest Basis:
:$\Img f \subseteq \BB$
Thus by Subset implies Cardinal Inequality:
:$\card {\Img f} \le \card \BB = \map w T$
{{qed}}
Theorem: Finite Weight Space has Basis equal to Image of Mapping of Intersections

Let $T = \struct {X, \tau}$ be a topological space with finite weight.
Then there exist a basis $\BB$ of $T$ and a mapping $f:X \to \tau$ such that:
:$\BB = \Img f$ and
:$\forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$
where $\Img f$ denotes the image of $f$.

Proof:
By definition of weight there exists a basis $\BB$ such that:
:$\card \BB = \map w T$
where:
:$\map w T$ denotes the weight of $T$
:$\card \BB$ denotes the cardinality of $\BB$.
By assumption that weight is finite:
:$\card \BB$ is finite
Then by Cardinality of Set is Finite iff Set is Finite:
:$\BB$ is finite
Define a mapping $f: X \to \powerset X$:
:$(1): \quad \forall x \in X: \map f x = \bigcap \set {U \in \BB: x \in U}$
By definition of subset:
:$\forall x \in X: \set {U \in \BB: x \in U} \subseteq \BB$
By Subset of Finite Set is Finite:
:$\forall x \in X: \set {U \in \BB: x \in U}$ is finite
Then by General Intersection Property of Topological Space:
:$\forall x \in X: \bigcap \set {U \in \BB: x \in U} \in \tau$
So:
:$f: X \to \tau$
We will prove that:
:$(2): \quad \forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$
Let $x \in X$.
By $(1)$:
:$\map f x = \bigcap \set {U \in \BB: x \in U}$
Thus by definition of intersection:
:$x \in \map f x$
Let $U$ be an open set of $T$.
Let $x \in U$.
By definition of basis:
:$\exists V \in \BB: x \in V \subseteq U$
Then:
:$V \in \set {U \in \BB: x \in U}$
Hence by Intersection is Subset:
:$\map f x \subseteq V$
Thus by Subset Relation is Transitive:
:$\map f x \subseteq U$
This ends the proof of $(2)$.
We will prove that $\Img f$ is a basis of $T$.
By $f: X \to \tau$ and definition of image:
:$\Img f \subseteq \tau$
Let $U$ be an open set of $T$.
Let $x$ be a point $x \in X$ such that:
:$x \in U$
By $(2)$:
:$\map f x \in \Img f \land x \in \map f x \subseteq U$
By definition of basis this ends the proof of basis.
Thus the result.
{{qed}}
Theorem: Rubik's Cube has 54 Facets

Let $S$ be the set of facets of Rubik's cube.
Then the cardinality of $S$ is given by:
:$\card S = 54$
That is:
:A Rubik's cube has $54$ facets.

Proof:
A cube, by definition, has $6$ faces.
Each face is subdivided into $9$ facets.
Hence there are $6 \times 9 = 54$ facets in total.
{{qed}}
Theorem: Equivalence of Definitions of Symmetric Difference/(3) iff (5)

Let $S$ and $T$ be sets.
{{TFAENocat|def = Symmetric Difference|view = symmetric difference $S \symdif T$ between $S$ and $T$}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in S \symdif T
}}
{{eqn | o = \leadstoandfrom
      | r = x \in S \oplus x \in T
      | c = {{Defof|Symmetric Difference|index = 5}}
}}
{{eqn | r = \paren {\neg \paren {x \in S} \land \paren {x \in T} } \lor \paren {\paren {x \in S} \land \neg \paren {x \in T} }
      | o = \leadstoandfrom
      | c = Non-Equivalence as Disjunction of Conjunctions
}}
{{eqn | r = \paren {x \in \overline S \land x \in T} \lor \paren {x \in S \land x \in \overline T}
      | o = \leadstoandfrom
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \paren {x \in \overline S \cup T} \lor \paren {x \in S \cup \overline T}
      | o = \leadstoandfrom
      | c = {{Defof|Set Intersection}}
}}
{{eqn | r = x \in \paren {\overline S \cup T} \cup \paren {S \cup \overline T}
      | o = \leadstoandfrom
      | c = {{Defof|Set Union}}
}}
{{eqn | r = x \in \paren {S \cup \overline T} \cup \paren {\overline S \cup T}
      | o = \leadstoandfrom
      | c = Union is Commutative
}}
{{end-eqn}}
The result follows by definition of set equality.
Theorem: Equivalence of Definitions of Symmetric Difference/(2) iff (5)

Let $S$ and $T$ be sets.
{{TFAENocat|def = Symmetric Difference|view = symmetric difference $S \symdif T$ between $S$ and $T$}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in S \symdif T
}}
{{eqn | o = \leadstoandfrom
      | r = x \in S \oplus x \in T
      | c = {{Defof|Symmetric Difference|index =  5}}
}}
{{eqn | r = \paren {x \in S \lor x \in T} \land \neg \paren {x \in S \land x \in T}
      | o = \leadstoandfrom
      | c = {{Defof|Exclusive Or}}
}}
{{eqn | r = \paren {x \in S \cup T} \land \paren {x \notin S \cap T}
      | o = \leadstoandfrom
      | c = {{Defof|Set Intersection}} and {{Defof|Set Union}}
}}
{{eqn | r = x \in \paren {S \cup T} \setminus \paren {S \cap T}
      | o = \leadstoandfrom
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
The result follows by definition of set equality.
Theorem: Partition of Facets of Rubik's Cube

Let $S$ denote the set of the facets of Rukik's cube.
Then $S$ can be partitioned as follows:
:$S = \set {S_C \mid S_E \mid S_Z}$
where:
:$S_C$ denotes the set of corner facets
:$S_E$ denotes the set of edge facets
:$S_Z$ denotes the set of center facets.

Proof:
From the definition of the facets, each face is divided into $9$ facets.
:600px
A facet is either:
:on the corner of a face, for example $flu$, $fru$
:on the edge of a face, for example $fu$, $fr$
:in the center of a face, for example $F$.
:$(1):\quad$ Each facet can be either in $S_C$ or $S_E$ or $S_Z$ and can not be in more than one.
:$(2):\quad$ Each facet can be either in $S_C$ or $S_E$ or $S_Z$ and there are no other possibilities.
:$(3):\quad$ None of $S_C$, $S_E$ and $S_Z$ is empty.
Thus the criteria for $S = \set {S_C \mid S_E \mid S_Z}$ to be a partition are fulfilled.
{{qed}}
Theorem: Even and Odd Integers form Partition of Integers

The odd integers and even integers form a partition of the integers.

Proof:
Let $n \in \Z$ be an integer.
Let $\Bbb O$ be the set of odd integers and $\Bbb E$ be the set of even integers.
By the Division Theorem:
:$\forall n \in \Z: \exists! q, r \in \Z: n = 2 q + r, 0 \le r < 2$
from which it follows that either:
:$n = 2 q \in \Bbb E$
or:
:$n = 2 q + 1 \in \Bbb O$
Thus:
:$(1): \quad$ each element of $\Z$ is in no more than one of $\Bbb E$ and $\Bbb O$
:$(2): \quad$ each element of $\Z$ is in at least one of $\Bbb E$ and $\Bbb O$
and:
:$(3): \quad$ setting $q = 0$ it is seen that $0 \in \Bbb E$ and $1 \in \Bbb O$ and so neither $\Bbb E$ or $\Bbb O$ is empty.
Thus $\set {\Bbb E \mid \Bbb O}$ is a partition of $\Z$ by definition.
{{qed}}
Theorem: Analog between Logic and Set Theory

The concepts of set theory have directly corresponding concepts in logic:
:{| border = "1"
|-
! style="padding: 2px 10px" | Set Theory
! style="padding: 2px 10px" | Logic
|-
| align="left" style="padding: 2px 10px"| Set: $S, T$
| align="left" style="padding: 2px 10px"| Statement: $p, q$
|-
| align="left" style="padding: 2px 10px"| Union: $S \cup T$
| align="left" style="padding: 2px 10px"| Disjunction: $p \lor q$
|-
| align="left" style="padding: 2px 10px"| Intersection: $S \cap T$
| align="left" style="padding: 2px 10px"| Conjunction: $p \land q$
|-
| align="left" style="padding: 2px 10px"| Subset: $S \subseteq T$
| align="left" style="padding: 2px 10px"| Conditional: $p \implies q$
|-
| align="left" style="padding: 2px 10px"| Symmetric Difference: $S \symdif T$
| align="left" style="padding: 2px 10px"| Exclusive Or: $p \oplus q$
|-
| align="left" style="padding: 2px 10px"| Complement: $\relcomp {} S$
| align="left" style="padding: 2px 10px"| Logical Not: $\lnot p$
|-
| align="left" style="padding: 2px 10px"| Set Equality: $S = T$
| align="left" style="padding: 2px 10px"| Biconditional: $p \iff q$
|-
| align="left" style="padding: 2px 10px"| Venn Diagram
| align="left" style="padding: 2px 10px"| Truth Table
|}

Proof:
Let $P$ and $Q$ be propositional functions.
Let $S$ and $T$ be subsets of a universe $\Bbb U$ such that:
:$S = \set {x \in \Bbb U: \map P x}$
:$T = \set {x \in \Bbb U: \map Q x}$
By the following definitions:
{{begin-axiom}}
{{axiom | n = 1
        | lc= Intersection:
        | ml= S \cap T
        | mo= :=
        | mr= \set {x \in \Bbb U: \map P x \land \map Q x}
}}
{{axiom | n = 2
        | lc= Union:
        | ml= S \cup T
        | mo= :=
        | mr= \set {x \in \Bbb U: \map P x \lor \map Q x}
}}
{{axiom | n = 3
        | lc= Subset:
        | ml= S \subseteq T
        | mo= :=
        | mr= \forall x \in \Bbb U: \map P x \implies \map Q x
}}
{{axiom | n = 4
        | lc= Symmetric Difference:
        | ml= S \symdif T
        | mo= =
        | mr= \set {x \in \Bbb U: \map P x \oplus \map Q x}
}}
{{axiom | n = 5
        | lc= Complement:
        | ml= \relcomp {} S
        | mo= :=
        | mr= \set {x \in \Bbb U: \lnot \map P x}
}}
{{axiom | n = 6
        | lc= Set Equality:
        | ml= S = T
        | mo= :=
        | mr= \forall x \in \Bbb U: \map P x \iff \map Q x
}}
{{end-axiom}}
{{qed}}
Theorem: Euler Phi Function of 1

:$\map \phi 1 = 1$

Proof:
The only (strictly) positive integer less than or equal to $1$ is $1$ itself.
By Integer is Coprime to 1, $1$ is coprime to itself.
Hence, by definition, there is exactly $1$ integer less than or equal to $1$ which is coprime with $1$.
Hence the result.
{{qed}}
Theorem: Cardinality of Set is Finite iff Set is Finite

Let $A$ be a set.
:$\card A$ is finite
{{iff}}:
:$A$ is finite
where $\card A$ denotes the cardinality of $A$.

Proof:
Definition of cardinal:
:$(1): \quad \card A \sim A$
:$\card A$ is finite
{{iff}}:
:$\exists n \in \N: \card A \sim \N_n$ by definition of finite set
{{iff}}:
:$\exists n \in \N: A \sim \N_n$ by $(1)$ and Set Equivalence behaves like Equivalence Relation
{{iff}}:
:$A$ is finite by definition of finite set.
{{qed}}
Theorem: Multiplication using Parabola

:500pxrightthumb
Let the parabola $P$ defined as $y = x^2$ be plotted on the Cartesian plane.
Let $A = \tuple {x_a, y_a}$ and $B = \tuple {x_b, y_b}$ be points on the curve $\map f x$ so that $x_a < x_b$.
Then the line segment joining $A B$ will cross the $y$-axis at $-x_a x_b$.
Thus $P$ can be used as a nomogram to calculate the product of two numbers $x_a$ and $x_b$, as follows:
:$(1) \quad$ Find the points $-x_a$ and $x_b$ on the $x$-axis.
:$(2) \quad$ Find the points $A$ and $B$ where the lines $x = -x_a$ and $x = x_b$ cut $P$.
:$(3) \quad$ Lay a straightedge on the straight line joining $A$ and $B$ and locate its $y$-intercept $c$.
Then $x_a x_b$ can be read off from the $y$-axis as the position of $c$.

Proof:
Let $\map f x = x^2$.
Then:
:$\map f {x_a} = x_a^2$
and:
:$\map f {x_b} = x_b^2$
Then the slope $m$ of the line segment joining $A B$ will be:
{{begin-eqn}}
{{eqn | l = m 
      | r = \frac {x_b^2 - x_a^2} {x_b - x_a}
      | c = Equation of Straight Line in Plane: Point-Slope Form
}}
{{eqn | r = \frac {\paren {x_b - x_a} \paren {x_b + x_a} } {x_b - x_a}
      | c = Difference of Two Squares
}}
{{eqn | r = x_b + x_a
      | c = cancelling, $x_a \ne x_b$
}}
{{end-eqn}}
From Equation of Straight Line in Plane: Slope-Intercept Form:
:$y = \paren {x_b + x_a} x + c$
where $c$ denotes the $y$-intercept.
Substituting the coordinates of point $A = \tuple {x_a, x_a^2}$ for $\tuple {x, y}$:
{{begin-eqn}}
{{eqn | l = x_a^2 
      | r = \paren {x_b + x_a} x_a + c
}}
{{eqn | ll= \leadsto
      | l = c
      | r = x_a^2 - \paren {x_a + x_b} x_a
}}
{{eqn | r = x_a^2 - x_a^2 - x_b x_a
}}
{{eqn | r = -x_b x_a
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Countably Infinite Set

Let $S$ be a set.
{{TFAE|def = Countably Infinite Set}}

Proof:
From Integers are Countably Infinite there is a bijection between $\Z$, the set of integers, and $\N$, the set of natural numbers.
Let $h: \N \to \Z$ be such a bijection.
Let $f: S \to \N$ be a bijection.
From Composite of Bijections is Bijection:
:$h \circ f: S \to \Z$ is a bijection.
Similarly, let $g: S \to \Z$ be a bijection.
By Inverse of Bijection is Bijection, $h^{-1}: \Z \to \N$ is a bijection.
Again from Composite of Bijections is Bijection:
:$h^{-1} \circ g: S \to \N$ is a bijection.
Hence the result.
{{qed}}
Category:Countable Sets
s7idhd996fd7blca6a2kfvk7asgj26o
Theorem: Set of Odd Integers is Countably Infinite

Let $\Bbb O$ be the set of odd integers.
Then $\Bbb O$ is countably infinite.

Proof:
Let $f: \Bbb O \to \Z$ be the mapping defined as:
:$\forall x \in \Bbb O: \map f x = \dfrac {x + 1} 2$
$f$ is well-defined as $x + 1$ is even and so $\dfrac {x + 1} 2 \in \Z$.
Let $x, y \in \Bbb O$ such that $\map f x = \map f y$.
Then:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x + 1} 2
      | r = \dfrac {y + 1} 2
      | c = Definition of $f$
}}
{{eqn | ll= \leadsto
      | l = x + 1
      | r = y + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{end-eqn}}
Thus $f$ is injective by definition.
Consider the inverse $f^{-1}$.
By inspection:
:$\forall x \in \Z: \map {f^{-1} } x = 2 x - 1$
$f^{-1}$ is well-defined, and $2 x - 1$ is odd.
Thus $f^{-1}$ is a mapping from $\Z$ to $\Bbb O$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f^{-1} } x
      | r = \map {f^{-1} } y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 x - 1
      | r = 2 y - 1
      | c = Definition of $f^{-1}$
}}
{{eqn | ll= \leadsto
      | l = 2 x
      | r = 2 y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{end-eqn}}
Thus $f^{-1}$ is injective by definition.
It follows by the Cantor-Bernstein-Schröder Theorem that there exists a bijection between $\Z$ and $\Bbb O$.
{{qed}}
Theorem: Unique Readability for Prefix Notation

Let $\AA$ be an alphabet.
Then prefix notation for $\AA$ has the unique readability property.

Proof:
Let $\phi$ be a WFF of prefix notation for $\AA$.
Apply the Principle of Mathematical Induction on the length of $\phi$ to prove:
:$(1): \quad$ No prefix of $\phi$ is a WFF, except $\phi$ itself;
:$(2): \quad$ If the first symbol of $\phi$ has arity $n$, then there exist unique WFFs $\phi_1, \ldots, \phi_n$ such that $\phi = s \phi_1 \cdots \phi_n$.
Let $\phi'$ be a WFF that is a prefix of $\phi$.
Because all WFFs have at least length $1$, it follows that:
:$\phi' = s \phi'_1 \cdots \phi'_n$
Now it must be that either $\phi_1$ is a prefix of $\phi'_1$ or vice versa.
By the induction hypothesis on $(1)$, it must be that $\phi_1 = \phi'_1$ because $\phi_1$ and $\phi'_1$ are both strictly shorter than $\phi$.
Now if, given $1 < j \le n$:
:$\phi_i = \phi'_i$ for all $i < j$
it follows that $\phi_j$ and $\phi'_j$ start at the same position in $\phi$.
Hence again, inductively, it follows that $\phi_j = \phi'_j$.
Thus $\phi_i = \phi'_i$ for all $1 \le i \le n$; that is:
:$\phi = \phi'$
The result follows by the Principle of Mathematical Induction.
{{qed}}