# Set of Local Minimum is Countable

## Theorem

Let $X$ be a subset of $\R$.

The set:

- $\leftset {x \in X: x}$ is local minimum in $\rightset X$

is countable.

## Proof

Define:

- $Y := \leftset {x \in X: x}$ is local minimum in $\rightset X$

By definition of $Y$ and definition of local minimum in set:

- $\forall x \in Y: \exists y \in \R: y < x \land \openint y x \cap X = \O$

By the Axiom of Choice, define a mapping $f: Y \to \powerset \R$ as:

- $\forall x \in Y: \exists y \in \R: \map f x = \openint y x \land y < x \land \map f x \cap X = \O$

We will prove that $f$ is an injection by definition:

Let $x_1, x_2 \in Y$ such that

- $\map f {x_1} = \map f {x_2}$

By definition of $f$:

- $\exists y_1 \in \R: \map f {x_1} = \openint {y_1} {x_1} \land y_1 < x_1 \land \map f {x_1} \cap X = \O$

and:

- $\exists y_2 \in \R: \map f {x_2} = \openint {y_2} {x_2} \land y_2 < x_2 \land \map f {x_2} \cap X = \O$

Then:

- $\openint {y_1} {x_1} = \openint {y_2} {x_2}$

Thus $x_1 = x_2$.

This ends the proof of injection.

By Cardinality of Image of Injection:

- $(1): \quad \card Y = \card {\map {f^\to} Y} = \card {\Img f}$

where

- $\card Y$ denotes the cardinality of $Y$,
- $\map {f^\to} Y$ denotes the image of $Y$ under $f$,
- $\Img f$ denotes the image of $f$.

We will prove that $\Img f$ is pairwise disjoint by definition.

Let $A, B \in \Img f$ such that

- $A \ne B$.

Then by definition of image:

- $\exists x_1 \in Y: \map f {x_1} = A$

and

- $\exists x_2 \in Y: \map f {x_2} = B$.

By difference of $A$ and $B$:

- $x_1 \ne x_2$

By definition of $f$:

- $\exists y_1 \in \R: \map f {x_1} = \openint {y_1} {x_1} \land y_1 < x_1 \land \map f {x_1} \cap X = \O$

and:

- $\exists y_2 \in \R: \map f {x_2} = \openint {y_2} {x_2} \land y_2 < x_2 \land \map f {x_2} \cap X = \O$

Aiming at contradiction suppose that

- $A \cap B \ne \O$.

$x_1 < x_2$ or $x_1 > x_2$.

In case when $x_1 < x_2$, $x_1 \in \map f {x_2}$ what contradicts with $\map f {x_2} \cap X = \O$.

In case when $x_1 > x_2$, analogically.

This ends the proof that $\Img f$ is pairwise disjoint.

By Set of Pairwise Disjoint Intervals is Countable:

- $\Img f$ is countable.

Thus by $(1)$ and Set is Countable if Cardinality equals Cardinality of Countable Set the result:

- $Y$ is countable.

$\blacksquare$

## Sources

- Mizar article TOPGEN_3:19