avewright/proofwiki-math huggingface dataset:
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of B/Commutative Operations

:Exactly $8$ of the operations of $\BB$ is commutative.

Proof:
Recall Automorphism Group of $\BB$.
Consider each of the categories of $\BB$ induced by each of $a \circ a$, $a \circ b$ and $a \circ c$, illustrated by the partially-filled Cayley tables to which they give rise:
;$(1): \quad a \circ a$
:$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & a &   &   \\
b &   & b &   \\
c &   &   & c \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & b &   &   \\
b &   & c &   \\
c &   &   & a \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & c &   &   \\
b &   & a &   \\
c &   &   & b \\
\end {array}$
;$(2): \quad a \circ b$
:$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & a &   \\
b &   &   & b \\
c & c &   &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & b &   \\
b &   &   & c \\
c & a &   &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & c &   \\
b &   &   & a \\
c & b &   &   \\
\end {array}$
;$(3): \quad a \circ c$
:$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   &   & c \\
b & a &   &   \\
c &   & b &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   &   & b \\
b & c &   &   \\
c &   & a &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   &   & c \\
b & a &   &   \\
c &   & b &   \\
\end {array}$
With a view to Cayley Table for Commutative Operation is Symmetrical about Main Diagonal, we inspect the various combinations of these partial Cayley tables.
It is apparent that the result of $x \circ x$ makes no difference to whether an operation is commutative.
However, note that each of the partial operations in $(2)$ can be conjoined with exactly $1$ of the partial operations in $(3)$ to make a commutative operation:
:$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & a & c \\
b & a &   & b \\
c & c & b &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & b & a \\
b & b &   & c \\
c & a & c &   \\
\end {array} 
\qquad
\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a &   & c & b \\
b & c &   & a \\
c & b & a &   \\
\end {array}$
Hence by the Product Rule for Counting there are $3 \times 3 = 9$ commutative operations which can be constructed thus.
However, note that one of these:
:$\begin {array} {c|ccc}
\circ & a & b & c \\
\hline
a & a & c & b \\
b & c & b & a \\
c & b & a & c \\
\end {array}$
has already been accounted for in Automorphism Group of $\AA$: Commutative Operations.
This commutative operations is such that the group of automorphisms of $\struct {S, \circ}$ forms the complete symmetric group on $S$, not just the given permutations.
Hence the result.
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of C n/Commutative Operations

$8$ of the operations of each of $\CC_1$, $\CC_2$ and $\CC_3$ is commutative.

Proof:
{{WLOG}}, we will analyse the nature of $\CC_1$.
Recall this lemma:
Theorem: Sets of Operations on Set of 3 Elements/Automorphism Group of D/Commutative Operations

:$696$ of the operations of $\DD$ is commutative.

Proof:
Let $n$ denote the number of commutative operations of $\DD$.
Recall these definitions:
Let $\AA$, $\BB$, $\CC_1$, $\CC_2$ and $\CC_3$ be respectively the set of all operations $\circ$ on $S$ such that the groups of automorphisms of $\struct {S, \circ}$ are as follows:
{{begin-eqn}}
{{eqn | l = \AA
      | o = :
      | r = \map \Gamma S
      | c = where $\map \Gamma S$ is the symmetric group on $S$
}}
{{eqn | l = \BB
      | o = :
      | r = \set {I_S, \tuple {a, b, c}, \tuple {a, c, b} }
      | c = where $I_S$ is the identity mapping on $S$
}}
{{eqn | l = \CC_1
      | o = :
      | r = \set {I_S, \tuple {a, b} }
}}
{{eqn | l = \CC_2
      | o = :
      | r = \set {I_S, \tuple {a, c} }
}}
{{eqn | l = \CC_3
      | o = :
      | r = \set {I_S, \tuple {b, c} }
}}
{{end-eqn}}
Let $N$ be the total number of commutative operations on $S$.
Let:
:$A$ denote the number of commutative operations in $\AA$
:$B$ denote the number of commutative operations in $\BB$
:$C$ denote the total number of commutative operations in $\CC_1$, $\CC_2$ and $\CC_3$.
From the lemma, and from the Fundamental Principle of Counting:
:$N = A + B + C + D$
From Count of Commutative Binary Operations on Set:
:$N = 3^6 = 729$
Then we have:
:From Automorphism Group of $\AA$: Operations with Identity: $A = 1$
:From Automorphism Group of $\BB$: Operations with Identity: $B = 8$
:From Automorphism Group of $\CC_n$: Operations with Identity: $C = 3 \times 8$
Hence we have:
{{begin-eqn}}
{{eqn | l = n
      | r = N - A - B - C
      | c = 
}}
{{eqn | r = 729 - 1 - 8 - 24
      | c = 
}}
{{eqn | r = 696
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sets of Operations on Set of 3 Elements/Commutative Operations

Let $\PP$ be the set of all commutative operations $\circ$ on $S$.
Then the elements of $\PP$ are divided in $129$ isomorphism classes.
That is, up to isomorphism, there are $129$ commutative operations on $S$ which have an identity element.

Proof:
From Automorphism Group of $\AA$: Commutative Operations:
:there is exactly $1$ commutative operation in $\AA$.
From Automorphism Group of $\BB$: Commutative Operations:
:there are $8$ commutative operations in $\BB$.
From Automorphism Group of $\CC_n$: Commutative Operations:
:there are $3 \times 8$ commutative operations in $\CC$.
From Automorphism Group of $\DD$: Commutative Operations:
:there are $696$ commutative operations in $\DD$.
From Automorphism Group of $\CC_n$: Isomorphism Classes:
:the elements of $\BB$ form isomorphism classes in pairs.
From Automorphism Group of $\CC_n$: Isomorphism Classes:
:the elements of $\CC$ form isomorphism classes in threes.
From Automorphism Group of $\DD$: Isomorphism Classes:
:the elements of $\DD$ form isomorphism classes in sixes.
Hence there are:
:$\dfrac 8 2 = 4$ isomorphism classes of commutative operations in $\BB$.
:$\dfrac {3 \times 8} 3 = 8$ isomorphism classes of commutative operations in $\CC$.
:$\dfrac {696} 6 = 116$ isomorphism classes of commutative operations in $\DD$.
Thus there are $1 + 4 + 8 + 116 = 129$ isomorphism classes of operations $\circ$ on $S$ which have an identity element..
{{qed}}
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 10

Let: 
:$n, k \in \N : k > 0 : r_n = r_{n + k}$
Then:
:$d_{n + 1} = d_{n + k + 1}$
:$r_{n + 1} = r_{n + k + 1}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = d_{n + 1} b + p r_{n + 1}
      | r = r_n
      | c = {{hypothesis}}
}}
{{eqn | r = r_{n + k}
      | c = {{hypothesis}}
}}
{{eqn | r = d_{n + k + 1} b + p r_{n + k + 1}
      | c = {{hypothesis}}
}}
{{eqn | ll = \leadsto
      | l = p \paren{ r_{n + k + 1} - r_{n + 1} }
      | r = \paren {d_{n + 1}  - d_{n + k + 1} }b
      | c = re-arranging terms
}}
{{end-eqn}}
As $b, p$ are coprime:
:$p \nmid b$
From Euclid's Lemma:
:$p \divides \paren {d_{n + 1}  - d_{n + k + 1} }$
By definition of $p$-adic digits:
:$d_{n + 1}, d_{n + k + 1} \in \set {0, 1, \ldots, p - 1}$
Hence:
:$d_{n + 1} = d_{n + k + 1}$
We have:
{{begin-eqn}}
{{eqn | l = p \paren{ r_{n + k + 1} - r_{n + 1} }
      | r = \paren {d_{n + 1}  - d_{n + k + 1} } b
}}
{{eqn | r = 0
      | c = as $d_{n + 1} = d_{n + k + 1}$
}}
{{eqn | ll= \leadsto
      | l = \paren {r_{n + k + 1} - r_{n + 1} }
      | r = 0
      | c = as $p \ne 0$
}}
{{eqn | ll= \leadsto
      | l = r_{n + 1}
      | r = r_{n + k + 1}
}}
{{end-eqn}}
{{qed}}
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
j6c0cdppsxcyxep0cszjnquc97whmfe
Theorem: Locally Integrable (f(x+ct) + f(x-ct))/2 is Weak Solution to Wave Equation

Consider the wave equation:
:$\dfrac {\partial^2 u} {\partial t^2} - c^2 \dfrac {\partial^2 u} {\partial x^2} = 0$
with the initial conditions:
:$\map u {x, 0} = \map f x$
:$\map {\dfrac {\partial u} {\partial t}} {x, 0} = 0$
and $c \in \R$.
Then it has a weak solution of the form:
:$\map u {x, t} := \dfrac {\map f {x + ct} + \map f {x - ct}} 2$ 
where $f \in \map {L^1_{loc} } \R$ is a locally integrable function.

Proof:
Let $\map u {x, t} = \map f {x + ct}$ be a locally integrable function.
We have that a locally integrable function defines a distribution.
Let $T_u \in \map {\DD'} {\R^2}$ be a Schwartz distribution associated with $u$.
Let $\phi \in \map \DD {\R^2}$ be a test function.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {\dfrac {\partial^2 T_u}{\partial t^2} - c^2 \dfrac {\partial^2 T_u}{\partial x^2} } } \phi
      | r = \paren {\dfrac {\partial^2}{\partial t^2} - c^2 \dfrac {\partial^2}{\partial x^2} } \map {T_{\frac 1 2 \map f {x \mathop + ct} } } \phi + \paren {\dfrac {\partial^2}{\partial t^2} - c^2 \dfrac {\partial^2}{\partial x^2} } \map {T_{\frac 1 2 \map f {x \mathop - ct} } } \phi
       | c = {{Defof|Pointwise Addition of Distributions}}
}}
{{eqn | r = \paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \map {T_{\frac 1 2 \map f {x \mathop + ct} } } \phi + \paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \map {T_{\frac 1 2 \map f {x \mathop - ct} } } \phi
      | c = Distributional Partial Derivatives Commute
}}
{{eqn | r = -\paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \map {T_{\frac 1 2 \map f {x \mathop + ct} } } {\paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \phi} - \paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \map {T_{\frac 1 2 \map f {x \mathop - ct} } } {\paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \phi}
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = - \frac 1 2 \paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \map {T_{\map f {x \mathop + ct} } } {\paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \phi} - \frac 1 2 \paren {\dfrac {\partial}{\partial t} + c \dfrac {\partial}{\partial x} } \map {T_{\map f {x \mathop - ct} } } {\paren {\dfrac {\partial}{\partial t} - c \dfrac {\partial}{\partial x} } \phi}
}}
{{eqn | r = -0 -0
      | c = Locally Integrable f(x+ct) is Weak Solution to Transport Equation, {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Therefore, $\map u {x, t} := \dfrac {\map f {x + c t} + \map f {x - c t} } 2$ is a weak solution to the wave equation.
{{qed}}
Theorem: Weak Solution to Dx u = Heaviside Step Function

Let $H: \R \to \closedint 0 1$ be the Heaviside step function.
Let $u : \R \to \R$ be such that:
:<nowiki>$\map u x = \begin{cases}
c & : x < 0 \\
x + c & : x > 0 
\end{cases}$</nowiki> 
where $c \in \R$.
Let $T_u$ be the Schwartz distribution associated with $u$.
Then $u$ is a weak solution of:
:$u' = H$
That is, in the distributional sense it holds that:
:$\dfrac \d {\d x} T_u = T_H$

Proof:
$u$ is continuous on $\R$ and continously differentiable on $\R \setminus \set 0$.
For $x < 0$ we have $\map {u'} x = 0$.
For $x > 0$ we have $\map {u'} x = 1$.
That is:
:$\map {u'} x = \map H x$
Furthermore:
:$\ds \lim_{x \mathop \to 0^-} = 0$
:$\ds \lim_{x \mathop \to 0^+} = 1$
By the jump rule:
{{begin-eqn}}
{{eqn | l = T_u' 
      | r = T_H + 0 \cdot \delta
}}
{{eqn | r = T_H
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Derivative with Finite Discontinuities

Let $f$ have a finite number of jump discontinuities at $t = a_i$ for $i = 1, 2, \ldots, n$.
Then:
:$\laptrans {\map {f'} t} = s \laptrans {\map f t} - \map f 0 - \ds \sum_{i \mathop = 1}^n e^{-a_i s} \paren {\map f {a_i^+} - \map f {a_i^-} }$

Proof:
{{tidy|Rewrite the following in house style}}
The proof is found similarly to the proof in Laplace Transform of Derivative but requires breaking the integral into $n$ integrals of finite range between the discontinuities and one improper integral from $a_n^+$ to $+\infty$. Integration by parts yields the summation when evaluating $e^{-s t}x(t)$ and the remaining integrals can all be recombined into one improper integral that is identically equal to $s \laptrans {\map f t}$.
Specifically, as in the proof in Laplace Transform of Derivative,
{{begin-eqn}}
{{eqn | l = \laptrans {\map {f'} t}
      | r = \int_0^{\mathop \to +\infty} e^{-s t} \map {f'} t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \lim_{A \mathop \to +\infty} \int_0^A e^{-s t} \map {f'} t \rd t
      | c = {{Defof|Improper Integral on Closed Interval Unbounded Above}}
}}
{{end-eqn}}
Breaking the integral into $n+1$ integrals over continuous intervals gives
:$\ds \lim_{A \mathop \to +\infty} \int_0^A e^{-s t} \map {f'} t \rd t = \int_0^{a_1^-} e^{-s t} \map {f'} t \rd t + \int_{a_1^+}^{a_2^-} e^{-s t} \map {f'} t \rd t + \cdots + \int_{a_{n-1}^+}^{a_n^-} e^{-s t} \map {f'} t \rd t + \lim_{A \mathop \to +\infty} \int_{a_n^+}^A e^{-s t} \map {f'} t \rd t$
Integration by parts on all integrals yields
:$\ds \lim_{A \mathop \to +\infty} \int_0^A e^{-s t} \map {f'} t \rd t = \bigintlimits {e^{-s t} \map f t} {t \mathop = 0} {t \mathop = a_1^-} + s \int_0^{a_1^-} e^{-s t} \map {f} t \rd t + \bigintlimits {e^{-s t} \map f t} {t \mathop = a_1^+} {t \mathop = a_2^-} + s \int_{a_1^+}^{a_2^-} e^{-s t} \map {f} t \rd t + \cdots + \bigintlimits {e^{-s t} \map f t} {t \mathop = a_{n-1}^+} {t \mathop = a_n^-} + s \int_{a_{n-1}^+}^{a_n^-} e^{-s t} \map {f} t \rd t + \lim_{A \mathop \to +\infty} \bigintlimits {e^{-s t} \map f t} {t \mathop = a_n^+} {t \mathop = A} + \lim_{A \mathop \to +\infty} s \int_{a_n^+}^A e^{-s t} \map {f} t \rd t$
These terms combine to form
:$\ds \lim_{A \mathop \to +\infty} \int_0^A e^{-s t} \map {f'} t \rd t = \sum_{i \mathop = 1}^n e^{-a_i s} \paren {\map f {a_i^+} - \map f {a_i^-} } + \lim_{A \mathop \to +\infty} \bigintlimits {e^{-s t} \map f t} {t \mathop = 0} {t \mathop = A} + \lim_{A \mathop \to +\infty} s \int_0^A e^{-s t} \map {f} t \rd t$
where the proof in Laplace Transform of Derivative simplifies the terms other than the summation and gives the final result
:$\ds \lim_{A \mathop \to +\infty} \int_0^A e^{-s t} \map {f'} t \rd t = s \laptrans {\map f t} - \map f 0 - \ds \sum_{i \mathop = 1}^n e^{-a_i s} \paren {\map f {a_i^+} - \map f {a_i^-} }$
Theorem: Power Set is Nonempty

Let $S$ be a set.
Then:
:$\powerset S \ne \O$

Proof:
By Empty Set is Element of Power Set:
:$\O \in \powerset S$
Thus we conclude that $\powerset S$ is non-empty.
{{qed}}
Category:Empty Set
Category:Power Set
j0xb6oxhss17kiz835w4sxlq42kj82i
Theorem: Multiplication of Distribution induced by Locally Integrable Function by Smooth Function

Let $f \in \map {L^1_{loc} } {\R^d}$ be a locally integrable function.
Let $\alpha \in \map {C^\infty} {\R^d}$ be a smooth function.
Let $T_f \in \map {\DD'} {\R^d}$ be a Schwartz distribution induced by $f$.
Then in the distributional sense it holds that:
:$\alpha T_f = T_{\alpha f}$

Proof:
Let $\Omega \subseteq \R^d$ be a compact subset.
Then for all $\mathbf x \in \Omega$ we have that $\map \alpha {\mathbf x}$ is bounded.
Hence, $\alpha f$ is locally integrable.
Let $\phi \in \map \DD {\R^d}$ be a test function.
Then:
{{begin-eqn}}
{{eqn | l = \alpha \map {T_f} \phi
      | r = \map {T_f} {\alpha \phi}
      | c = {{Defof|Multiplication of Schwartz Distribution by Smooth Function}}
}}
{{eqn | r = \int_{\R^d} \map f {\mathbf x} \map \alpha {\mathbf x} \map \phi {\mathbf x} \rd \mathbf x
      | c = Locally Integrable Function defines Distribution
}}
{{eqn | r = \map {T_{\alpha f} } \phi
      | c = Locally Integrable Function defines Distribution
}}
{{end-eqn}}
{{qed}}
Theorem: Cartesian Product is Unique

Let $A$ and $B$ be classes.
If there exists a '''cartesian product''' of $A$ and $B$, then it is unique.

Proof:
Let $C_1$ and $C_2$ be cartesian products of $A$ and $B$.
Then by the cartesian product definition, for an arbitrary $a$:
:$a \in C_1 \iff \exists x \in A: \exists y \in B: a = \tuple {x, y}$
:$a \in C_2 \iff \exists x \in A: \exists y \in B: a = \tuple {x, y}$
By Biconditional is Transitive:
:$a \in C_1 \iff a \in C_2$
By Axiom of Extension:
:$C_1 = C_2$
Thus the cartesian product of $A$ and $B$ is unique.
{{qed}}
Theorem: Biconditional of Proposition and its Negation

:$\vdash \neg (p \iff \neg p)$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|cccc|} \hline
\neg & (p & \iff & \neg & p)\\
\hline
\T & \F & \F & \T & \F \\
\T & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Cycle Graph is Eulerian

Let $G$ be a cycle graph.
Then $G$ is Eulerian.

Proof:
From Cycle Graph is Connected, $G$ is a connected graph.
From Cycle Graph is $2$-Regular, $G$ is $2$-regular.
It follows directly from Characteristics of Eulerian Graph that $G$ is Eulerian.
{{Qed}}
Category:Cycle Graphs
Category:Eulerian Graphs
jt94p8yky7cp9lr3s8g8bw2rngonfnd
Theorem: Cycle Graph is 2-Regular

Let $G$ be a cycle graph.
Then $G$ is regular.

Proof:
Let $G$ be a cycle graph.
By definition, a '''cycle graph''' is a graph which consists of a single cycle $C$.
By definition, a '''cycle''' is a circuit in which no vertex except the first (which is also the last) appears more than once.
By definition, a '''circuit''' is a closed trail with at least one edge.
By definition, a '''trail''' is a walk in which all edges are distinct.
Let $v$ be a vertex of $G$.
Then $v$ is a vertex of a closed walk.
Hence for every edge which is incident with $v$, there exists another edge which is also incident with $v$.
Suppose $v$ were odd.
Then at least one edge must appear at least twice in $C$.
But then $C$ would not be a '''trail'''.
Thus $v$ is even.
Suppose $v$ has degree zero.
Then there are no edges incident with $v$.
Hence $v$ is not on a closed walk.
Hence the degree of $v$ is greater than $0$.
Suppose $v$ has degree greater than $2$.
Then $v$ must be on a circuit in which $v$ appears more than once.
Hence that circuit is not a cycle
Hence $G$ is not a cycle graph.
Hence $v$ is of degree $2$.
The result follows.
{{qed}}
Category:Cycle Graphs
Category:Regular Graphs
0vyko1av1fajw9k38zhe3iq4i1on2j0
Theorem: Cycle Graph is Connected

Let $G = \struct {V, E}$ be a cycle graph.
Then $G$ is connected.

Proof:
A cycle graph is defined as a (simple) graph which consists of a single cycle.
So a cycle graph consists of just one component, and hence is connected.
{{qed}}
Category:Cycle Graphs
Category:Connectedness (Graph Theory)
0enbhaoaa4eus769o1qcyjxp639ol87
Theorem: Cycle Graph is Bipartite iff Order is Even

Let $n \in \N$ be a natural number.
Let $C_n$ be the cycle graph of order $n$.
Then $C_n$ is a bipartite graph {{iff}} $n$ is even.

Proof:
Let $V$ be the set of vertices of $C_n$.
Let the elements of $V$ be denoted $v_1, v_2, \ldots, v_n$.
Then by definition of cycle graph, by appropriate selection of subscripts, $C_n$ consists of one cycle $C$ that can be expressed as:
:$C := \tuple {v_1 v_2 \ldots, v_n v_1}$
Let $v_k \in C_n$.
Then for $1 < k < n$, $v_k$ is adjacent to $v_{k - 1}$ and $v_{k + 1}$ and no other vertices of $C_n$.
We also have that:
:$v_1$ is adjacent to $v_2$ and $v_n$
and by the same coin:
:$v_n$ is adjacent to $v_{n - 1}$ and $v_1$.
Theorem: Cycle Graph of Order 1 is Loop-Graph

Let $C_1$ denote the cycle graph of order $1$.
Then $C_1$ is a loop-graph.

Proof:
By definition, the vertex set of $C_1$ is singleton, $\set v$, say.
The only vertex of $C_1$ that an edge can be incident to is $v$.
Hence there exists an edge which is incident to $v$ at both ends.
That is, $C_1$ has a loop.
Hence the result by definition of loop-graph.
{{qed}}
Category:Examples of Cycle Graphs
Category:Examples of Loop-Graphs
4urzas3fyk1tp8cq1kwrn71ii17bw1f
Theorem: Cycle Graph of Order 2 is Multigraph

Let $C_2$ denote the cycle graph of order $2$.
Then $C_2$ is a multigraph.

Proof:
By definition, the vertex set of $C_2$ is doubleton, $\set {v_1, v_2}$, say.
By definition of cycle graph, there is a circuit $v_1 v_2 v_1$.
That is:
:there exists an edge which is incident to $v_1$ and $v_2$
:there exists an edge which is incident to $v_2$ and $v_1$
That is, there are $2$ edges which are both incident to $v_1$ and $v_2$
Hence the result by definition of multigraph.
{{qed}}
Category:Examples of Cycle Graphs
Category:Examples of Multigraphs
jzo9ongimui5j82spfrkhqdazlw9vmt
Theorem: Cycle Graph of Order 3 is Complete Graph

Let $C_3$ denote the cycle graph of order $2$.
Then $C_3$ is the complete graph of of order $3$.

Proof:
Let the vertex set of $C_3$ is $\set {v_1, v_2, v_3}$.
By definition of cycle graph, $C_3$ consists of the cycle $v_1 v_2 v_3 v_1$.
It is seen by inspection that:
:$v_1$ is adjacent to $v_2$ and $v_3$
:$v_2$ is adjacent to $v_1$ and $v_3$
:$v_3$ is adjacent to $v_1$ and $v_2$.
Hence the result by definition of complete graph.
{{qed}}
Category:Examples of Cycle Graphs
Category:Examples of Complete Graphs
krfspl7hdtadf9za2n50sgylop67htl
Theorem: Negated Restricted Existential Quantifier

Let $x$ and $A$ be sets.
Let $\map P x$ be a propositional function.
:$\neg \exists x \in A : \map P x \iff \forall x \in A : \neg \map P x $

Proof:
From left to right:
{{begin-eqn}}
{{eqn | q = \neg \exists x \in A
      | o = \map P x
}}
{{eqn | ll= \leadsto
      | q = \neg \exists x 
      | o = x \in A \land \map P x
      | c = {{defof|Restricted Existential Quantifier}}
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = \neg \paren{x \in A \land \map P x}
      | c = De Morgan's Laws (Predicate Logic)/Denial of Existence
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = x \in A \implies \neg \map P x
      | c = Modus Ponendo Tollens/Variant
}}
{{eqn | ll= \leadsto
      | q = \forall x \in A
      | o = \neg \map P x
      | c = {{defof|Restricted Universal Quantifier}}
}}
{{end-eqn}}
From right to left:
{{begin-eqn}}
{{eqn | q = \forall x \in A
      | o = \neg \map P x
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = x \in A \implies \neg \map P x
      | c = {{defof|Restricted Universal Quantifier}}
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = \neg \paren{x \in A \land \map P x}
      | c = Modus Ponendo Tollens/Variant
}}
{{eqn | ll= \leadsto
      | q = \neg \exists x
      | o = x \in A \land \map P x
      | c = De Morgan's Laws (Predicate Logic)/Denial of Existence
}}
{{eqn | ll= \leadsto
      | q = \neg \exists x \in A
      | o = \map P x
      | c = {{defof|Restricted Existential Quantifier}}
}}
{{end-eqn}}
{{qed}}
o4wj8v7pnvhttfcuowss3cbuk0g3iis
Theorem: Negated Restricted Universal Quantifier

Let $x$ and $A$ be sets.
Let $\map P x$ be a propositional function.
:$\neg \forall x \in A : \map P x \iff \exists x \in A : \neg \map P x $

Proof:
=== Sufficient Condition ===
{{begin-eqn}}
{{eqn | q = \neg \forall x \in A
      | o = \map P x
}}
{{eqn | ll= \leadsto
      | q = \neg \forall x 
      | o = x \in A \implies \map P x
      | c = {{defof|Restricted Universal Quantifier}}
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | o = \neg \paren{x \in A \implies \map P x}
      | c = De Morgan's Laws (Predicate Logic)/Denial of Universality
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | o = x \in A \land \neg \map P x
      | c = Conjunction with Negative is Equivalent to Negation of Conditional
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A
      | o = \neg \map P x
      | c = {{defof|Restricted Existential Quantifier}}
}}
{{end-eqn}}
{{qed|lemma}}