nyuuzyou/wikis huggingface dataset:
Minimally Closed Class under Progressing Mapping is Well-Ordered/Proof

== Theorem ==
== Proof ==
According to hypothesis, let $M$ be a minimally closed under $g$ with respect to $b$.
By Minimally Closed Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
By Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element:
:if $x$ is a fixed point of $g$, then $x$ is the greatest element of $M$.
Thus the conditions for Closed Class under Progressing Mapping Lemma hold.
In order to show that $M$ is well-ordered under the subset relation, it is to be shown that every non-empty subclass $A$ of $M$ has a smallest element.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
If $b \in A$, then from Smallest Element of Minimally Closed Class under Progressing Mapping, $b$ is the smallest element of $A$.
So, consider the case where $b \notin A$.
Then $b$ is a proper subset of every element of $A$.
Thus $b \in L$ and so $L$ is non-empty.
By definition, $L$ is bounded by all elements of $A$.
Since $A$ is non-empty, $L$ is bounded by at least one element of $A$.
Hence by Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element:
:$L$ has a greatest element $x$.
Therefore, by Closed Class under Progressing Mapping Lemma, $\map g x$ is the smallest element of $A$.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Exercise $4.1$
Category:Minimally Closed Classes under Progressing Mapping
Minimally Inductive Class under Progressing Mapping induces Nest

== Theorem ==
Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
== Proof 1 ==
== Proof 2 ==
Category:Progressing Mappings
Category:Minimally Inductive Classes
Category:Minimally Inductive Class under Progressing Mapping induces Nest
Minimally Inductive Class under Progressing Mapping induces Nest/Proof 1

== Theorem ==
== Proof ==
Let $\RR$ be the relation on $M$ defined as:
:$\forall x, y \in M: \map \RR {x, y} \iff \map g x \subseteq y \lor y \subseteq x$
We are given that $g$ is a progressing mapping.
From the Progressing Function Lemma, we have that:
From the Double Induction Principle, if $\RR$ is a relation on $M$ which satisfies:
then $\map \RR {x, y}$ holds for all $x, y \in M$.
Thus:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
follows directly.
Then the fact that:
:$\map g x \subseteq y \lor y \subseteq x$
implies that:
:$x \subseteq y \lor y \subseteq x$
because:
:$x \subseteq \map g x$
Hence the result by definition of a nest.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Theorem $4.7$
Category:Minimally Inductive Class under Progressing Mapping induces Nest
Minimally Inductive Class under Progressing Mapping induces Nest/Proof 2

== Theorem ==
== Proof ==
A minimally inductive class under $g$ is the same thing as a minimally closed class under $g$ with respect to $\O$.
The result then follows by a direct application of Minimally Closed Class under Progressing Mapping induces Nest.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Exercise $4.1$
Category:Minimally Inductive Class under Progressing Mapping induces Nest
Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation

== Theorem ==
Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x$ be a fixed point of $g$.
Then $M$ is well-ordered under the subset relation.
== Proof 1 ==
== Proof 2 ==
Category:Minimally Inductive Classes
Category:Progressing Mappings
Category:Well-Orderings
Category:Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation
Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation/Proof 1

== Theorem ==
== Proof ==
According to hypothesis, let $M$ be minimally inductive under $g$.
By Minimally Inductive Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
By Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element:
:if $x$ is a fixed point of $g$, then $x$ is the greatest element of $M$.
Thus the conditions for Closed Class under Progressing Mapping Lemma hold.
In order to show that $M$ is well-ordered under the subset relation, it is to be shown that every non-empty subclass $A$ of $M$ has a smallest element.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
If $\O \in A$, then $\O$ is the smallest element of $A$.
So, consider the case where $\O \notin A$.
Then $\O$ is a proper subset of every element of $A$.
Thus $\O \in L$ and so $L$ is non-empty.
By definition, $L$ is bounded by all elements of $A$.
Since $A$ is non-empty, $L$ is bounded by at least one element of $A$.
Hence by Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element:
:$L$ has a greatest element $x$.
Therefore, by Closed Class under Progressing Mapping Lemma, $\map g x$ is the smallest element of $A$.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Theorem $4.16$
Category:Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation
Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation/Proof 2

== Theorem ==
== Proof ==
A minimally inductive class under $g$ is the same thing as a minimally closed class under $g$ with respect to $\O$.
The result then follows by a direct application of Minimally Closed Class under Progressing Mapping is Well-Ordered.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Exercise $4.1$
Category:Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation
Minimally Inductive Class under Progressing Mapping with Fixed Element is Finite

== Theorem ==
Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let there exist an element $x \in M$ such that $x = \map g x$.
Then $M$ is a finite class.
== Proof ==
By Set of Subsets of Element of Minimally Inductive Class under Progressing Mapping is Finite, the set:
:$\set {y \in M: y \subseteq x}$
is finite.
From Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element, $x$ is the greatest element of $M$.
Thus:
:$M = \set {y \in M: y \subseteq x}$
Hence the result.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 6$ Finite Sets: Exercise $6.5$
Category:Minimally Inductive Classes
Category:Progressing Mappings
Category:Finite Classes
Minimally Inductive Class under Slowly Progressing Mapping is Nest

== Theorem ==
Let $M$ be a class.
Let $g: M \to M$ be a slowly progressing mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Then $M$ is a nest.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 9$ Supplement -- optional
Category:Minimally Inductive Classes
Category:Slowly Progressing Mappings
Category:Nests
Category:Minimally Inductive Class under Slowly Progressing Mapping is Nest
Minimally Inductive Class under Slowly Progressing Mapping is Nest/Proof 2

== Theorem ==
== Proof ==
By definition, a slowly progressing mapping is indeed a progressing mapping.
The result then follows from Minimally Inductive Class under Progressing Mapping induces Nest.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 9$ Supplement -- optional
Category:Minimally Inductive Class under Slowly Progressing Mapping is Nest
Minimally Inductive Set Exists

== Theorem ==
There exists a minimally inductive set $\omega$ that is a subset of every other inductive set.
== Proof ==
From the Axiom of Infinity, there is a set $S$ such that:
:$\O \in S$
:$x \in S \implies x^+ \in S$
where $\O$ denotes the empty set and $x^+$ is the successor set of $x$.
That is, there exists an inductive set.
Next, by the Axiom of Specification, the minimally inductive set $\omega$:
:$\omega := \ds \bigcap \set {S' \subseteq S: \text{$S'$ is an inductive set} }$
exists.
It remains to be shown that if $T$ is an inductive set, then $\omega \subseteq T$.
By Intersection of Inductive Sets, $S \cap T$ is an inductive set.
Moreover, by Intersection is Subset, $S \cap T$, so that:
:$S \cap T \in \set {S' \subseteq S: \text{$S'$ is an inductive set} }$
from which we conclude by definition of $\omega$ and Intersection is Subset: General Result that:
:$\omega \subseteq S \cap T \subseteq T$
as desired.
== Sources ==
* : $\S 11$: Numbers
Category:Minimally Inductive Set
Minimally Inductive Set forms Peano Structure

== Theorem ==
Let $\omega$ be the minimally inductive set.
Let $\cdot^+: \omega \to \omega$ be the mapping assigning to a set its successor set:
:$n^+ := n \cup \set n$
Let $\O \in \omega$ be the empty set.
Then $\struct {\omega, \cdot^+, \O}$ is a Peano structure.
== Proof ==
We need to check that all of Peano's axioms hold for $\struct {\omega, \cdot^+, \O}$.
Suppose first that for $m, n \in \omega$, we have $m^+ = n^+$.
Since $n \in n^+$ it follows that $n \in m^+$.
Hence, either $n \in m$ or $n = m$.
Similarly, either $m \in n$ or $m = n$.
Now if $n \ne m$, both $m \in n$ and $n \in m$.
By Element of Minimally Inductive Set is Transitive Set, it follows that $n \subseteq m$.
As $m \in n$, this contradicts Finite Ordinal is not Subset of one of its Elements.
Hence it must be that $n = m$, and holds.
Next, since $n \in n^+$ for all $n \in \omega$, it follows that $n^+ \ne \O$.
Hence, holds as well.
Finally, let $S \subseteq \omega$ satisfy:
:$\O \in S$
:$\forall n \in S: n^+ \in S$
Then by definition, $S$ is an inductive set.
Therefore, by definition of $\omega$ as the minimally inductive set:
:$\omega \subseteq S$
Consequently $S = \omega$ by the definition of set equality.
Thus is seen to hold.
That is, $\struct {\omega, \cdot^+, \O}$ is a Peano structure.
== Sources ==
* : $\S 12$: The Peano Axioms
* : $\S 7.30$
* : $\S 5.2$
Category:Peano's Axioms
Category:Minimally Inductive Set
Minimally Inductive Set is Infinite Cardinal

== Theorem ==
$\omega$, the minimally inductive set, is an element of the class of infinite cardinals $\NN'$.
== Proof ==
By Cardinal Number Less than Ordinal: Corollary:
:$\card \omega \le \omega$
Moreover, for any $n \in \omega$, by Cardinal of Finite Ordinal:
:$\card n < \card {n + 1} \le \card \omega$
Thus by Cardinal of Finite Ordinal:
:$n \in \card \omega$
Therefore:
:$\omega = \card \omega$
By Cardinal of Cardinal Equal to Cardinal: Corollary:
:$\omega \in \NN'$
Category:Cardinals
Category:Minimally Inductive Set
Minimally Inductive Set is Limit Ordinal

== Theorem ==
Let $\omega$ denote the minimally inductive set.
Then $\omega$ is a limit ordinal.
== Proof ==
Let $K_I$ denote the class of all nonlimit ordinals.
 $\omega$ is not a limit ordinal.
Every element of $\omega$ is a nonlimit ordinal.
So, if $\omega$ is also a nonlimit ordinal, $\omega + 1 \subseteq K_I$.
By the definition of $\omega$:
:$\omega \in \omega$
which violates No Membership Loops and is thus contradictory.
It follows from Proof by Contradiction that $\omega$ is a limit ordinal.
== Sources ==
* : $\S 7.33$
Category:Ordinals
Category:Minimally Inductive Set
Minimally Inductive Set is Minimal

== Theorem ==
The minimally inductive set $\omega$ is a subset of every inductive set.
== Proof ==
Let $A$ be an inductive set.
Let $B$ be another arbitrary inductive set.
Then from Intersection is Subset, $A \cap B \subseteq A$.
From Intersection of Inductive Sets, $A \cap B$ is also an inductive set.
This set $A \cap B$ is one of the subsets
By the definition of $\omega$ it follows that $\omega \subseteq A \cap B$, and consequently that $\omega \subseteq B$.
== Sources ==
* : $\S 11$: Numbers
Category:Minimally Inductive Set
Minimally Inductive Set is Ordinal

== Theorem ==
Let $\omega$ denote the minimally inductive set.
Then $\omega$ is an ordinal.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 7.32$
Category:Ordinals
Category:Minimally Inductive Set
Category:Minimally Inductive Set is Ordinal
Minimally Inductive Set is Ordinal/Proof 1

== Theorem ==
== Proof ==
The minimally inductive set is a set of ordinals by definition.
From the corollary of ordinals are well-ordered, it is seen that $\left({\omega, \Epsilon \! \restriction_\omega}\right)$ is a strictly well-ordered set.
It is to be shown by induction on minimally inductive set that $\forall n \in \omega: \omega_n = n$
=== Basis for the Induction ===
=== Induction Hypothesis ===
Suppose that $\omega_n = n$ for some $n \in \omega$.
=== Induction Step ===
And so $\omega$ is an ordinal.
Category:Minimally Inductive Set is Ordinal
Minimally Inductive Set is Ordinal/Proof 2

== Theorem ==
== Proof ==
Let $K_I$ denote the set of all nonlimit ordinals.
Let $\On$ denote the set of all ordinals.
Let $a \in \omega$.
It follows that $a^+ \subseteq K_I$, so $a \in K_I$.
Thus:
:$\omega \subseteq K_I \subseteq \On$
We now must prove that $\omega$ is a transitive set, at which point it will satisfy the Alternative Definition of Ordinal.
Let $x \in y$ and $y \in \omega$.
Then:
:$y \in \On \land y^+ \subseteq K_I$
Because $y$ is an ordinal, it is transitive.
Therefore:
:$x \subseteq y$
and:
:$x^+ \subseteq y^+ \subseteq K_I$
Therefore, $x^+ \subseteq K_I$.
Applying the definition of minimally inductive set:
:$x \in \omega$
so $\omega$ is transitive.
== Motivation ==
This demonstrates that $\omega$ can be shown to be an ordinal without use of the Axiom of Infinity.
By Ordinal is Member of Class of All Ordinals, it follows that $\omega \in \On$ or $\omega = \On$.
The Axiom of Infinity rejects the latter option in favor of the former.
Category:Minimally Inductive Set is Ordinal
Minimally Superinductive Class is Well-Ordered under Subset Relation

== Theorem ==
Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be minimally superinductive under $g$.
Then $M$ is well-ordered under the subset relation.
== Proof ==
We have that $M$ is a $g$-tower.
The result follows from $g$-Tower is Well-Ordered under Subset Relation.
Category:Minimally Superinductive Classes
Category:Well-Orderings
Category:Subset Relation
Minimax Theorem

== Theorem ==
Let $G$ be a two-person game.
Let each player $\text A$ and $\text B$ adopt their best mixed strategy.
Then the expected gain of $\text A$ will exactly equal the expected loss of $\text B$.
This gain or loss will then be the value of $G$.
== Proof ==
== Historical Note ==
== Sources ==
* 
* 
* 
* 
Category:Mixed Strategies
Category:Game Theory
Category:Named Theorems
Minimization of Arithmetically Definable Function is Arithmetically Definable

== Theorem ==
Let $f: \N^{k + 1} \to \N$ be a partial function.
Let $g: \N^k \to \N$ be the partial function defined as:
:$\map g {x_1, \dotsc, x_k} \approx \map {\mu z} {\map f {x_1, \dotsc, x_k, z} }$
where $\mu$ is minimization.
Suppose that there exists a $\Sigma_1$ WFF of $k + 2$ free variables:
:$\map {\phi_f} {y, x_1, \dotsc, x_k, z}$
such that:
:$y = \map f {x_1, \dotsc, x_k, z} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k}, \sqbrk z}$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.
Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:
:$\map {\phi_g} {y, x_1, \dotsc, x_k}$
such that:
:$y = \map g {x_1, \dotsc, x_k} \iff \N \models \map {\phi_g} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$
== Proof ==
Define:
:$\map {\phi_g} {y, x_1, \dotsc, x_k} := \map {\phi_f} {0, x_1, \dotsc, x_k, y} \land \forall p < y: \exists q: \paren {q \ne 0 \land \map {\phi_f} {q, x_1, \dotsc, x_k, y} }$
For, by definition of minimization:
:$y = \map g {x_1, \dotsc, x_k}$
:$\map f {x_1, \dotsc, x_k, y} = 0$
and
:$\map f {x_1, \dotsc, x_k, p}$ is defined and $\ne 0$ for each $p < y$.
That $\phi_g$ is $\Sigma_1$ follows from:
:Conjunction of Existential Quantifier
:Bounded Universal Quantifier Distributes over Conjunction
Category:Recursive Functions
Minimization on Relation Equivalent to Minimization on Function

== Theorem ==
Let $\RR$ be a $k + 1$-ary relation on $\N^{k + 1}$.
Then the function $g: \N^{k + 1} \to \N$ defined as:
:$\map g {n_1, n_2, \ldots, n_k, z} = \mu y \ \map \RR {n_1, n_2, \ldots, n_k, y}$
where $\mu y \ \map \RR {n_1, n_2, \ldots, n_k, y}$ is the minimization operation on $\RR$
is equivalent to minimization on a total function.
== Proof ==
We have that $\map \RR {n_1, n_2, \ldots, n_k, y}$ holds $\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} = 1$, from the definition of the characteristic function of a relation.
This in turn holds $\map {\overline{\operatorname{sgn} } } {\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} } = 0$, where $\overline{\operatorname{sgn} }$ is the signum-bar function.
Hence we have:
:$\mu y \ \map \RR {n_1, n_2, \ldots, n_k, y} \iff \map {\mu y} {\map {\overline{\operatorname{sgn} } } {\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} } = 0}$.
Since $\overline{\operatorname{sgn}}$ and $\chi_\RR$ are total functions, then so is $\overline{\operatorname{sgn} } \circ \chi_\RR$.
Category:Primitive Recursive Functions
Category:Recursive Functions
Minimum Area of Triangle whose Vertices are Lattice Points

== Theorem ==
Let $T$ be a triangle embedded in a cartesian plane.
Let the vertices of $T$ be lattice points which are not all on the same straight line.
Then the area of $T$ is such that:
:$\map \Area T \ge \dfrac 1 2$
== Proof ==
 let one of the vertices of $T$ be at $\tuple {0, 0}$.
Let the other $2$ vertices be at $\tuple {a, b}$ and $\tuple {x, y}$.
By Area of Triangle in Determinant Form with Vertex at Origin‎:
:$\map \Area T = \dfrac {\size {b y - a x} } 2$
As the vertices of $T$ are non-collinear, $\map \Area T \ge 0$.
Thus $\size {b y - a x} > 0$.
As $\tuple {a, b}$ and $\tuple {x, y}$ are lattice points, all of $a, b, x, y \in \Z$.
Thus $\size {b y - a x} \ge 1$.
Hence the result.
== Sources ==
* : $\text {2-3}$ The Linear Diophantine Equation: Exercise $6$
Category:Areas of Triangles
Minimum Connector Problem

== Problem ==
Given a weighted graph $G$, the object is to find a minimum spanning tree for $G$.
== Solution ==
There are two methods of solving this problem:
* Kruskal's Algorithm
* Prim's Algorithm
proved as:
* Kruskal's Algorithm produces Minimum Spanning Tree
* Prim's Algorithm produces Minimum Spanning Tree
== Also see ==
The Maximum Connector Problem is effectively the same problem taken from a different direction.
== Sources ==
* 
Category:Graph Theory
Minimum Degree Bound for Simple Planar Graph

== Theorem ==
Let $G$ be a simple connected planar graph.
Then: 
:$\map \delta G \le 5$
where $\map \delta G$ denotes the minimum degree of vertices of $G$.
== Proof ==
 $G$ is a simple connected planar graph with $\map \delta G \ge 6$. 
Let $m$ and $n$ denote the number of edges and vertices respectively in $G$. 
Then by the Handshake Lemma: 
This contradicts the Linear Bound Lemma:
:$m \le 3 n - 6$
Hence $\map \delta G \le 5$.
Category:Graph Theory
Minimum Degree is at Least Connectivity

== Theorem ==
Let $G = \struct {V, E}$ be a simple graph.
Then:
:$\map \delta G \ge \map \kappa G$
That is, the minimum degree of $G$ is at least its connectivity.
== Proof ==
Pick a vertex $v \in G$ with $\map {\deg_G} v = \map \delta G$, that is, a vertex with minimum degree.
Recall that $\map {\Gamma_G} v$ is the neighborhood of $v$ in $G$.
Suppose that $V = \map {\Gamma_G} v \cup \set v$.
That is, that $v$ is adjacent to all other vertices of $G$.
Then:
:$\card V = \card {\map {\Gamma_G} v} + 1 = \map \delta G + 1$
By definition, $\map \kappa G < \card V$, so $\map \kappa G \le \map \delta G$.
Otherwise, there is at least one vertex of $G$ not adjacent to $v$.
So, deleting $\map {\Gamma_G} v$ from $G$ leaves $v$ isolated.
Thus $\map {\Gamma_G} v$ is a vertex cut of size $\map \delta G$. 
Since $G$ has a vertex cut of size $\map \delta G$, it follows that $\map \kappa G \le \map \delta G$.
== Notes ==
This bound is not necessarily tight:
:
In this example, the minimum degree of the graph is $2$, yet $C$ is a cut-vertex and so this graph has connectivity $1$.
Category:Connectedness (Graph Theory)
Minimum Distance of Linear Code is Smallest Weight of Non-Zero Codeword

== Theorem ==
Let $C$ be a linear $\tuple {n, k}$-code whose master code is $\map V {n, p}$.
Let $\map d C$ denote the minimum distance of $C$.
Then:
:$\map d C = \ds \min_{u \mathop \in C} \map w u$
where $\map w u$ denotes the weight of $u$.
== Proof ==
Let $f := \ds \min_{u \mathop \in C} \map w u$.
Let $\mathbf 0$ denote the codeword in $\map V {n, p}$ consisting of all zeroes.
As $C$ is a subspace of $\map V {n, p}$, we have that $\mathbf 0 \in C$.
Let $w$ be a codeword with weight $f$.
Then:
:$\map d {w, \mathbf 0} = f$
so $f \ge \map d C$.
Let $u, v \in C$ such that $\map d {u, v} = \map d C$.
We have that $C$ is a linear code.
Therefore:
:$u - v \in C$
where $u - v$ denotes the difference between $u$ and $v$.
But $u - v$ has weight $\map d C$.
Thus:
:$\map d C \ge f$
and it follows that $\map d C = f$.
== Sources ==
* : Chapter $6$: Error-correcting codes: Proposition $6.9$
Category:Linear Codes
Minimum Function in terms of Absolute Value

== Theorem ==
Let $x$ and $y$ be real numbers.
Then:
:$\ds \min \set {x, y} = \frac 1 2 \paren {\paren {x + y} - \size {x - y} }$
== Proof ==
We aim to show that: 
:$\ds \frac 1 2 \paren {\paren {x + y} - \size {x - y} } = \begin{cases}x & x \le y \\ y & x > y\end{cases}$
Let $x \le y$, then: 
:$x - y \le 0$
so, by the definition of absolute value, we have: 
:$\size {x - y} = y - x$
So, for $x \le y$, we have: 
Now let $x > y$, then:
:$x - y > 0$
so, by the definition of absolute value, we have: 
:$\size {x - y} = x - y$
So, for $x > y$ we have: 
so:
:$\ds \frac 1 2 \paren {\paren {x + y} - \size {x - y} } = \begin{cases}x & x \le y \\ y & x > y\end{cases}$
as required.
Category:Absolute Value Function
Minimum Function is Primitive Recursive

== Theorem ==
The minimum function $\min: \N^2 \to \N$, defined as:
:$\map \min {n, m} = \begin{cases}
n: & n \le m \\
m: & m \le n
\end{cases}$
is primitive recursive‎.
== Proof ==
From Sum Less Maximum is Minimum we have that:
:$\map \min {n, m} = n + m - \map \max {n, m}$.
As $n + m \ge \map \max {n, m}$, we have that:
:$\map \min {n, m} = n + m \ \dot - \ \map \max {n, m}$
Hence we see that $\min$ is obtained by substitution from:
* the primitive recursive function $n \ \dot - \ m$
* the primitive recursive function $\map \max {n, m}$.
Hence the result.
Category:Primitive Recursive Functions