nyuuzyou/wikis huggingface dataset:
Midline and Median of Triangle Bisect Each Other

== Theorem ==
Let $\triangle ABC$ be a triangle.
Let $DE$ be the midline of $\triangle ABC$ which bisects $AB$ and $AC$.
Let $AF$ be the median of $ABC$ which bisects $BC$.
Then $AF$ and $DE$ bisect each other.
== Proof ==
Construct the midlines $DF$ and $EF$.
Then by the Midline Theorem $DF \parallel AE$ and $EF \parallel AD$.
Thus by Quadrilateral is Parallelogram iff Both Pairs of Opposite Sides are Equal or Parallel, $\Box ADFE$ is a parallelogram.
By construction, $AF$ and $DE$ are the diagonals of $\Box ADFE$.
The result follows from Diameters of Parallelogram Bisect each other.
== Sources ==
* : Chapter $1$: Triangles and Polygons: Theorems and Corollaries $1.26$: Corollary $2$
Category:Triangles
Category:Medians of Triangles
Midpoint-Convex Function is Rational Convex

== Theorem ==
Let $I$ be a non-empty real interval.
Let $f: I \to \R$ be a real function.
If $f$ is midpoint-convex, then $f$ is rational-convex. 
== Proof ==
It suffices to show that for each $n \in \N$ and for any choice of $n$ elements $x_1, \dots, x_n \in I$:
via Forward-Backward Induction.
=== Basis for the Induction ===
The statement holds:
:for $n = 0$ vacuously
:for $n = 1$ as $\map f {\dfrac x 1} = \dfrac {\map f x} 1$ for each $x \in I$.
Let $x_1, x_2$ be two points in $I$.
Then as $f$ is midpoint-convex:
This is the basis for the induction.
=== Induction Hypothesis ===
Suppose that if $n = 2^k$, then for any choice $x_1, \dots, x_n$ of $n$ elements in $I$, we have:
This is the induction hypothesis.
=== Induction Step ===
This is the induction step:
Let $n = 2^{k + 1}$.
Let $x_1, \dots, x_n \in I$. 
Then:
 
which completes the Proof by Mathematical Induction for integers of the form $2^k$. 
=== Backward Step ===
Let $2^k \le n \le 2^{k + 1}$ for some integer $k$.
Let $x_1, \dots, x_n \in I$.
Defined $\overline x := \dfrac {x_1 + \dots + x_n} n$.
Then:
from which we obtain:
completing the proof.
Category:Real Analysis
Midpoints of Sides of Quadrilateral form Parallelogram

== Theorem ==
Let $\Box ABCD$ be a quadrilateral.
Let $E, F, G, H$ be the midpoints of $AB, BC, CD, DA$ respectively.
Then $\Box EFGH$ is a parallelogram.
== Proof ==
Let $z_1, z_2, z_3, z_4$ be the position vectors of the vertices of $\Box ABCD$.
The midpoints of the sides of $\Box ABCD$ are, then:
Take two opposite sides $EF$ and $HG$:
The vectors defining the opposite sides of $\Box EFGH$ are equal.
The result follows by definition of parallelogram.
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Graphical Representation of Complex Numbers. Vectors: $68$
Category:Quadrilaterals
Category:Parallelograms
Midy's Theorem

== Theorem ==
Let $p$ be a prime.
Let $a \in \set {1, 2, \ldots, p - 1}$ and $b > 1$ be integers.
Let $N$ be the recurring part of the expansion of $\dfrac a p$ in base $b$.
Let $\alpha$ be the period of recurrence of $N$.
Let $\alpha = c k$ for (strictly) positive integers $c > 1$ and $k$.
Then $N$ is divisible by $b^k - 1$.
Moreover, let $N = \ds \sum_{i \mathop = 1}^c N_i \paren {b^k}^i$ for $N_i \in \set {0, 1, \ldots b^k - 1}$.
Then:
:$\ds \sum_{i \mathop = 1}^c N_i = r \paren {b^k - 1}$ for some $r \in \set {1, 2, \ldots, c - 1}$
== Proof ==
=== $N$ is divisible by $b^k - 1$ ===
By definition of recurrence, we have:
:$\dfrac a p b^\alpha = N + \dfrac a p$
Moreover, by definition of period of recurrence, $\alpha$ is the smallest positive integer for which this is true.
Rearranging, we obtain:
:$\dfrac a p \paren {b^\alpha - 1} = N$
In particular, $a \paren {b^\alpha - 1}$ is divisible by $p$.
As $p$ is prime:
:$p \divides a$ or $p \divides \paren {b^\alpha - 1}$
The former is false because $0 < a < p$. 
Therefore, we must have $p \divides \paren {b^\alpha - 1}$.
If $\alpha = c k$ with $c > 1$, then $b^\alpha - 1 = \paren {b^k - 1} m$ for some integer $m$.
As $p$ is prime:
:$p \divides b^k - 1$ or $p \divides m$
The former is false because $0 < k < \alpha$ and $\alpha$ is the smallest positive integer for which this is true. 
Therefore, we must have $p \divides m$.
This implies that $a \dfrac m p$ is an integer.
We then have:
:$a \dfrac m p \paren {b^k - 1} = N$
By definition, $N$ is divisible by $b^k - 1$.
=== The Sum of the $N_i$ is divisible by $b^k - 1$ ===
Calculating modulo $b^k - 1$, we have:
Therefore, we have:
:$\ds \sum_{k \mathop = 1}^c N_i = r \paren {b^k - 1}$
Notice further that:
:$\ds 0 < \sum_{k \mathop = 1}^c N_i < \sum_{k \mathop = 1}^c \paren {b^k - 1}$
The latter strict inequality follows because otherwise, we would have $N_i = b^k - 1$, meaning $\alpha = 1$.
Therefore, we must have $1 < r < c-1$.
== Examples ==
== Also see ==
* Definition:Repdigit Number
* Number times Recurring Part of Reciprocal gives 9-Repdigit
Category:Midy's Theorem
Category:Basis Expansions
Midy's Theorem/Examples/7

== Example of Use of Midy's Theorem ==
Let $p = 7$.
We have for $a = 1$ and $b = 10$ the decimal expansion:
:$\dfrac 1 7 = 0 \cdotp \dot 14285 \dot 7$
Hence:
:$N = 142857$
This means that:
:$\alpha = 6 = 2 \times 3$
Midy's Theorem states that $N$ is divisible by $10^2 - 1$ and $10^3 - 1$.
Moreover, we can partition $N$ into blocks of digits of equal length:
:$N = 14 \times 100^2 + 28 \times 100 + 57$
:$N = 142 \times 1000 + 857$
Summing these blocks together, we obtain:
:$14 + 28 + 57 = 99 = 10^2 - 1$
and:
:$142 + 857 = 999 = 10^3 - 1$
Category:Midy's Theorem
Mills' Theorem

== Theorem ==
There exists a real number $A$ such that $\floor {A^{3^n} }$ is a prime number for all $n \in \N_{>0}$, where:
:$\floor x$ denotes the floor function of $x$
:$\N$ denotes the set of all natural numbers.
== Proof ==
We define $\map f x$ as a prime-representing function :
:$\forall x \in \N: \map f x \in \Bbb P$
where:
:$\N$ denotes the set of all natural numbers
:$\Bbb P$ denotes the set of all prime numbers.
Let $p_n$ be the $n$th prime number.
From Difference between Consecutive Primes:
:$p_{n + 1} - p_n < K {p_n}^{5 / 8}$
where $K$ is an unknown but fixed positive integer.
=== Lemma 1 ===
Let $P_0 > K^8$ be a prime number.
By Lemma 1, there exists an infinite sequence of primes:
:$P_0, P_1, P_2, \ldots$
such that:
:$\forall n \in \N_{>0}: {P_n}^3 < P_{n + 1} < \paren {P_n + 1}^3 - 1$
Let us define two mappings $u, v: \N \to \Bbb P$ as:
:$\forall n \in \N: \map u n = {P_n}^{3^{-n} }$
:$\forall n \in \N: \map v n = \paren {P_n + 1}^{3^{-n} }$
It is trivial that $\map v n > \map u n$.
=== Lemma 2 ===
=== Lemma 3 ===
It follows trivially that $\map u n$ is bounded and strictly monotone.
Therefore, there exists a number $A$ which is defined as:
:$A := \lim_{n \mathop \to \infty} \map u n$
From Lemma 2 and Lemma 3, we have:
:$\map u n < A < \map v n$
The result follows.
== Sources ==
* 
* 
Category:Number Theory
Category:Mills' Theorem
Mills' Theorem/Lemma 1

== Lemma for Mills' Theorem ==
Let:
:$\N$ denotes the set of all natural numbers
:$\Bbb P$ denotes the set of all prime numbers.
Let $p_n$ be the $n$th prime number.
From Difference between Consecutive Primes:
:$p_{n + 1} - p_n < K {p_n}^{5 / 8}$
where $K$ is an unknown but fixed positive integer.
Then we have that:
:$\forall N > K^8 \in \Z: \exists p \in \Bbb P: N^3 < p < \paren {N + 1}^3 - 1$
== Proof ==
Let $p_n$ be the greatest prime less than $N^3$.
Therefore:
:$N^3 < p_{n + 1} < \paren {N + 1}^3 - 1$
Category:Mills' Theorem
Mills' Theorem/Lemma 2

== Lemma for Mills' Theorem ==
Let:
:$\N$ denote the set of all natural numbers
:$\Bbb P$ denote the set of all prime numbers.
Let $p_n$ be the $n$th prime number.
From Difference between Consecutive Primes:
:$p_{n + 1} - p_n < K {p_n}^{5 / 8}$
where $K$ is an unknown but fixed positive integer.
Let $P_0 > K^8$ be a prime number.
By Lemma 1, there exists an infinite sequence of primes:
:$P_0, P_1, P_2, \ldots$
such that:
:$\forall n \in \N_{>0}: {P_n}^3 < P_{n + 1} < \paren {P_n + 1}^3 - 1$
Let us define a mapping $u: \N \to \Bbb P$ as:
:$\forall n \in \N: \map u n = {P_n}^{3^{-n} }$
Then we have that:
:$\forall n \in \N_{>0}: \map u {n + 1} > \map u n$
== Proof ==
Category:Mills' Theorem
Mills' Theorem/Lemma 3

== Lemma for Mills' Theorem ==
Let:
:$\N$ denote the set of all natural numbers
:$\Bbb P$ denote the set of all prime numbers.
Let $p_n$ be the $n$th prime number.
From Difference between Consecutive Primes:
:$p_{n + 1} - p_n < K {p_n}^{5 / 8}$
where $K$ is an unknown but fixed positive integer.
Let $P_0 > K^8$ be a prime number.
By Lemma 1, there exists an infinite sequence of primes:
:$P_0, P_1, P_2, \ldots$
such that:
:$\forall n \in \N_{>0}: {P_n}^3 < P_{n + 1} < \paren {P_n + 1}^3 - 1$
Let us define the mapping $v: \N \to \Bbb P$ as:
:$\forall n \in \N: \map v n = \paren {P_n + 1}^{3^{-n} }$
Then we have that:
:$\forall n \in \N_{>0}: \map v {n + 1} < \map v n$
== Proof ==
Category:Mills' Theorem
Min Operation Equals an Operand

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $x_1, x_2, \dotsc, x_n \in S$ for some $n \in \N_{>0}$.
Then:
:$\exists i \in \closedint 1 n : x_i = \min \set {x_1, x_2, \dotsc, x_n}$
where:
:$\min$ denotes the min operation.
== Proof ==
We will prove the result by induction on the number of operands $n$.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\exists i \in \closedint 1 n : x_i = \min \set {x_1, x_2, \dotsc, x_n}$
=== Basis for the Induction ===
$\map P 1$ is the case:
:$\exists i \in \closedint 1 1 : x_i = \min \set {x_1}$
By definition of the min operation:
:$\min \set {x_1} = x_1$
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\exists i \in \closedint 1 k : x_i = \min \set {x_1, x_2, \dotsc, x_k}$
from which it is to be shown that:
:$\exists i \in \closedint 1 {k + 1} : x_i = \min \set {x_1, x_2, \dotsc, x_k, x_{k + 1} }$
=== Induction Step ===
This is the induction step.
By definition of the min operation:
:$\min \set {x_1, x_2, \dotsc, x_k, x_{k + 1} } = \min \set {\min \set {x_1, x_2, \dotsc, x_k}, x_{k + 1} }$
By the induction hypothesis:
:$\exists i \in \closedint 1 k : x_i = \min \set {x_1, x_2, \dotsc, x_k}$
So:
:$\min \set {x_1, x_2, \dotsc, x_k, x_{k + 1} } = \min \set {x_i, x_{k + 1} }$
As $\struct {S, \preceq}$ is a totally ordered set, all elements of $S$ are comparable by $\preceq$.
Therefore there are two cases to consider:
==== Case 1: $x_{k + 1} \preceq x_i$ ====
By definition of the min operation:
:$\min \set {x_i, x_{k + 1} } = x_{k+i}$
==== Case 2: $x_i \preceq x_{k + 1}$ ====
By definition of the min operation:
:$\min \set {x_i, x_{k + 1} } = x_i$
In either case, the result holds.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\exists i \in \closedint 1 n : x_i = \min \set {x_1, x_2, \dotsc, x_n}$
Category:Min Operation
Min Operation Preserves Total Ordering

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $a, b, c, d \in S$:
:$a \preceq b, c \preceq d$
Then:
:$\min \set{a, c} \preceq \min \set{b, d}$
where $\min$ denotes the min operation on $\struct {S, \preceq}$.
== Proof ==
From Min Operation Equals an Operand, either:
:$\min \set{b, d} = b$
or
:$\min \set{b, d} = d$
, suppose:
:$\min \set{b, d} = b$
We have:
By transitivity of an ordering:
:$\min \set{a, c} \preceq \min \set{b, d}$
Category:Min Operation
Min Operation Representation on Real Numbers

== Theorem ==
Let $x, y \in \R$.
Then:
:$\min \set{x, y} = \dfrac 1 2 \paren {x + y - \size {x - y} }$
where $\min$ denotes the min operation.
== Proof ==
From the Trichotomy Law for Real Numbers exactly one of the following holds:
:$x < y$ and so $\min \set {x, y} = x$
:$x = y$ and so $\min \set {x, y} = x = y$
:$y < x$ and so $\min \set {x, y} = y$
By the definition of the absolute value function for each case respectively we have:
:$\size {x - y} = y - x$
:$\size {x - y} = 0$
:$\size {x - y} = x - y$
Thus the equation holds by $+$ being commutative and associative as for each case:
:$\dfrac 1 2 \paren {x + y - \paren {y - x} } = x$
:$\dfrac 1 2 \paren {x + y + 0} = x = y$
:$\dfrac 1 2 \paren {x + y - \paren {x - y} } = y$
== Also see ==
* Max Operation Representation on Real Numbers
== Sources ==
* : $1$: Review of some real analysis: Exercise $1.5: 18 \ \text {(a)}$
Category:Real Analysis
Category:Min Operation
Min Operation Yields Infimum of Parameters

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set. 
Let $x, y \in S$.
Then:
:$\map \min {x, y} = \map \inf {\set {x, y} }$
where:
:$\min$ denotes the min operation
:$\inf$ denotes the infimum.
=== General Case ===
== Proof ==
As $\struct {S, \preceq}$ be a totally ordered set, all elements of $S$ are $\preceq$-comparable.
Therefore there are two cases to consider:
=== Case 1: $x \preceq y$ ===
In this case:
:$\map \min {x, y} = x = \map \inf {\set {x, y} }$
=== Case 2: $y \preceq x$ ===
In this case:
:$\map \min {x, y} = y = \map \inf {\set {x, y} }$
In either case, the result holds.
== Warning ==
Note that it is considered abuse of notation to write
:$\min = \inf$
This is because
:$\min: S \times S \to S$
while
:$\inf: \powerset S \to S$
where $\powerset S$ is the power set of $S$.
== Also see ==
* Max Operation Yields Supremum of Parameters
Category:Min Operation
Min Operation is Associative

== Theorem ==
The min operation is associative:
:$\map \min {\map \min {x, y}, z} = \map \min {x, \map \min {y, z} }$
Thus we are justified in writing $\map \min {x, y, z}$.
== Proof ==
To simplify our notation:
:Let $\map \min {x, y}$ be (temporarily) denoted $x \underline \vee y$.
There are the following cases to consider:
:$(1): \quad x \le y \le z$
:$(2): \quad x \le z \le y$
:$(3): \quad y \le x \le z$
:$(4): \quad y \le z \le x$
:$(5): \quad z \le x \le y$
:$(6): \quad z \le y \le x$
Taking each one in turn:
:$(1): \quad$ Let $x \le y \le z$. Then:
:$(2): \quad$ Let $x \le z \le y$. Then:
:$(3): \quad$ Let $y \le x \le z$. Then:
:$(4): \quad$ Let $y \le z \le x$. Then:
:$(5): \quad$ Let $z \le x \le y$. Then:
:$(6): \quad$ Let $z \le y \le x$. Then:
Thus in all cases it can be seen that the result holds.
== Also see ==
* Max Operation is Associative
Category:Min Operation
Category:Examples of Associative Operations
Min Operation is Commutative

== Theorem ==
The Min operation is commutative:
:$\map \min {x, y} = \map \min {y, x}$
== Proof ==
To simplify our notation:
:Let $\map \min {x, y}$ be (temporarily) denoted $x \underline \vee y$.
There are three cases to consider:
:$(1): \quad x \le y$
:$(2): \quad y \le x$
:$(3): \quad x = y$
$(1): \quad$ Let $x \le y$.
Then:
$(2): \quad$ Let $y \le x$.
Then:
$(3): \quad$ Let $x = y$.
Then:
Thus $\underline \vee$, i.e. $\min$, has been shown to be commutative in all cases.
== Also see ==
* Max Operation is Commutative
Category:Min Operation
Category:Examples of Commutative Operations
Min Operation is Idempotent

== Theorem ==
The min operation operation is idempotent:
:$\map \min {x, x} = x$
== Proof ==
Follows immediately from the definition of min operation:
:$\map \min {a, b} = \begin {cases} a & : a \le b \\ b & : b \le a \end {cases}$
Setting $x = a = b$ returns the result.
== Also see ==
* Max Operation is Idempotent
Category:Min Operation
Category:Examples of Idempotence‎
Min Operation on Continuous Real Functions is Continuous

== Theorem ==
Let $f: \R \to \R$ and $g: \R \to \R$ be real functions.
Let $f$ and $g$ be continuous at a point $a \in \R$.
Let $h: \R \to \R$ be the real function defined as:
:$\map h x := \map \min {\map f x, \map g x}$ 
Then $h$ is continuous at $a$.
== Proof ==
From Min Operation Representation on Real Numbers
:$\min \set{x, y} = \dfrac 1 2 \paren {x + y - \size {x - y} }$
Hence:
:$\min \set {\map f x, \map g x} = \dfrac 1 2 \paren {\map f x + \map g x - \size {\map f x - \map g x} }$
From Difference Rule for Continuous Real Functions:
:$\map f x - \map g x$ is continuous at $a$.
From Absolute Value of Continuous Real Function is Continuous:
:$\size {\map f x - \map g x}$ is continuous at $a$.
From Sum Rule for Continuous Real Functions:
:$\map f x + \map g x$ is continuous at $a$
and hence from Difference Rule for Continuous Real Functions again:
:$\map f x + \map g x - \size {\map f x - \map g x}$ is continuous at $a$
From Multiple Rule for Continuous Real Functions:
:$\dfrac 1 2 \paren {\map f x + \map g x - \size {\map f x - \map g x} }$ is continuous at $a$.
== Also see ==
* Max Operation on Continuous Real Functions is Continuous
== Sources ==
* : $1$: Review of some real analysis: Exercise $1.5: 18 \ \text {(b)}$
Category:Continuous Real Functions
Category:Min Operation
Min Operation on Toset forms Semigroup

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\map \min {x, y}$ denote the min operation on $x, y \in S$.
Then $\struct {S, \min}$ is a semigroup.
== Proof ==
By the definition of the min operation, either:
:$\map \min {x, y}= x$
or
:$\map \min {x, y}= y$
So $\min$ is closed on $S$.
From Min Operation is Associative:
:$\forall x, y, z \in S: \map \min {x, \map \min {y, z} } = \map \min {\map \min {x, y}, z}$
Hence the result, by definition of semigroup.
== Also see ==
* Max Operation on Toset forms Semigroup
Category:Min Operation
Min Semigroup is Commutative

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set. 
Then the semigroup $\struct {S, \min}$ is commutative.
== Proof ==
Let $x, y \in S$. 
From Min Operation is Commutative:
:$\map \min {x, y} = \map \min {y, x}$
Hence the result, by definition of commutative semigroup.
== Also see ==
* Max Semigroup is Commutative
	
Category:Min Operation
Category:Examples of Commutative Semigroups
Min Semigroup is Idempotent

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Then the semigroup $\struct {S, \min}$ is an idempotent semigroup.
== Proof ==
The fact that $\struct {S, \min}$ is a semigroup is demonstrated in Min Operation on Toset forms Semigroup.
Then the min operation is idempotent:
:$\forall x \in S: \min \set {x, x} = x$
The result follows by the definition of idempotent semigroup.
== Also see ==
* Max Semigroup is Idempotent
Category:Min Operation
Category:Examples of Idempotent Semigroups‎
Min Semigroup on Toset forms Semilattice

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set. 
Then the min semigroup $\struct {S, \min}$ is a semilattice.
== Proof ==
We have:
:Min Semigroup is Commutative
:Min Semigroup is Idempotent.
Hence the result, by definition of a semilattice.
== Also see ==
* Max Semigroup on Toset forms Semilattice
	
Category:Min Operation
Category:Semilattices
Min is Half of Sum Less Absolute Difference

== Theorem ==
For all numbers $a, b$ where $a, b$ in $\N, \Z, \Q$ or $\R$:
:$\min \set {a, b} = \dfrac 1 2 \paren {a + b - \size {a - b} }$
== Proof ==
From the definition of min:
:$\map \min {a, b} = \begin{cases}
a: & a \le b \\
b: & b \le a
\end{cases}$
Let $a < b$.
Then:
Let $a \ge b$.
Then:
== Also see ==
* Max is Half of Sum Plus Absolute Difference
Category:Min Operation
Minimal Arithmetic is Sigma 1 Complete

== Theorem ==
Let $\phi$ be a $\Sigma_1$ sentence in the language of arithmetic.
Suppose $\N \models \phi$.
Then $\phi$ is a theorem in minimal arithmetic.
== Proof ==
By definition of $\Sigma_1$, $\phi$ is logically equivalent to:
:$Q_1 Q_2 \dotsm Q_k \map \psi {x_1, x_2, \dotsc, x_k}$
where $\psi$ is a WFF with no quantifiers.
Proceed by induction on the number of quantifiers in the formula.
=== Basis for the Induction ===
Let $x_1, x_2, \dotsc, x_k \in \N$ be natural numbers.
Let $\sqbrk x$ denote the unary representation of $x$.
By Quantifier-Free Formula of Arithmetic is Provable:
:$\map \psi {x_1 \gets \sqbrk {x_1}, x_2 \gets \sqbrk {x_2}, \dotsc, x_k \gets \sqbrk {x_k} }$
is a theorem whenever $\N \models \map \psi {\dots}$.
=== Induction Hypothesis ===
Let $\psi$ be a WFF with $n$ quantifiers and $k - n$ free variables.
Suppose that, for every $x_1, x_2, \dotsc, x_{k - n} \in \N$ such that:
:$\N \models \map \psi {x_1 \gets \sqbrk {x_1}, x_2 \gets \sqbrk {x_2}, \dotsc, x_{k - n} \gets \sqbrk {x_{k - n} } }$
it follows that:
:$\map \psi {x_1 \gets \sqbrk {x_1} \dotsc, x_{k - n} \gets \sqbrk {x_{k - n} } }$
is a theorem.
=== Induction Step ===
Suppose the $k - n$-th quantifier is existential.
The step follows from Existential Quantification of Provable Arithmetic Formula is Provable.
Suppose instead that the $k - n$th quantifier is bounded universal.
The step follows from Bounded Universal Quantification of Provable Arithmetic Formula is Provable.
By Principle of Mathematical Induction, the statement holds in particular for $n = k$.
That is, when there are no free variables, and every quantifier has been considered.
Category:Natural Numbers
Category:Proof Theory
Minimal Element/Examples/Finite Subsets of Natural Numbers

== Examples of Minimal Elements ==
Let $\FF$ denote the set of finite subsets of the natural numbers $\N$.
Consider the ordered set $\struct {\FF, \subseteq}$.
There is one minimal element of $\struct {\FF, \subseteq}$, and that is the empty set $\O$.
== Proof ==
We have that $\O$ is a finite set.
By Empty Set is Subset of All Sets it follows that $\O$ is a subset of $\N$.
Hence $\O \in \FF$ by definition of $\FF$.
Let $A \in \FF$ be some finite subset of $\N$ such that $A \subseteq \O$.
Then by Subset of Empty Set iff Empty:
:$A = \O$
Hence $\O$ is a minimal element of $\struct {\FF, \subseteq}$ by definition.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $6 \ \text {(a)}$
Category:Examples of Minimal Elements
Minimal Element/Examples/Finite Subsets of Natural Numbers less Empty Set

== Examples of Minimal Elements ==
Let $\FF$ denote the set of finite subsets of the natural numbers $\N$.
Let $\GG$ denote the set $\FF \setminus \set \O$, that is, $\FF$ with the empty set excluded.
Consider the ordered set $\struct {\GG, \subseteq}$.
The minimal elements of $\struct {\GG, \subseteq}$ are the sets of the form $\set n$, for $n \in \N$.
== Proof ==
Let $n \in \N$.
We have that $\set n$ is a finite subset of $\N$.
Hence $\set n \in \GG$ by definition of $\GG$.
Let $A \in \GG$ be some finite subset of $\N$ such that $A \subseteq \set n$.
Then either $A = \O$ or $A = \set n$.
Because $\O \notin \GG$ it follows that $A = \set n$
Hence $\set n$ is a minimal element of $\struct {\GG, \subseteq}$ by definition.
Now suppose $B \subseteq \N$ such that:
:$\exists m, n \in B: m \ne n$
Then $B$ is a finite subset of $\N$ such that $B \ne \O$.
Hence $B \in \GG$ by definition of $\GG$.
Note that we have:
:$\set n \subseteq B$
and also:
:$\set m \subseteq B$
but $B \ne \set n$ and $B \ne \set m$.
Hence $B$ is not a minimal element of $\struct {\GG, \subseteq}$.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $6 \ \text {(a)}$
Category:Examples of Minimal Elements
Minimal Element in Toset is Unique and Smallest

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $m$ be a minimal element of $\struct {S, \preceq}$.
Then:
:$(1): \quad m$ is the smallest element of $\struct {S, \preceq}$
:$(2): \quad m$ is the only minimal element of $\struct {S, \preceq}$.
== Proof ==
By definition of minimal element:
:$\forall y \in S: y \preceq m \implies m = y$
As $\struct {S, \preceq}$ is a totally ordered set, by definition $\preceq$ is connected.
That is:
:$\forall x, y \in S: y \preceq x \lor x \preceq y$
It follows that:
:$\forall y \in S: m = y \lor m \preceq y$
But as $m = y \implies m \preceq y$ by definition of $\preceq$, it follows that:
:$\forall y \in S: m \preceq y$
which is precisely the definition of smallest element.
Hence $(1)$ holds.
Suppose $m_1$ and $m_2$ are both minimal elements of $S$.
By $(1)$ it follows that both are smallest elements.
It follows from Smallest Element is Unique that $m_1 = m_2$.
That is, $(2)$ holds.
== Also see ==
* Maximal Element in Toset is Unique and Greatest
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $6 \ \text {(b)}$
Category:Total Orderings
Category:Minimal Elements
Category:Smallest Elements