# Sorgenfrey Line is Lindelöf

## Theorem

The Sorgenfrey line is Lindelöf.

## Proof

Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.

Let $\CC$ be an open cover for $\R$.

Define $\VV = \set {U^\circ_\R: U \in \CC}$

where $U^\circ_\R$ denotes the interior of $U$ in the real number line $R = \struct {\R, \tau_d}$ with the usual (Euclidean) topology.

By definition of interior:

$\forall U \in \CC: U^\circ_\R \subseteq \R$
$W := \bigcup \VV \subseteq \R$
$R_W$ is Lindelöf

where $R_W$ denotes topological subspace of $R$ on $W$.

$\forall A \in \VV: A \subseteq W$
$\forall A \in \VV: A \cap W = A$

By definition of topological subspace:

$\forall A \in \VV: A$ is open in $R_W$

By definition

$\VV$ is open cover

By definition of Lindelöf space:

there exists a countable subcover $\SS$ of $\VV$

By definition of $\VV$:

$\forall A \in \VV: \exists U \in \CC: A = U^\circ_\R$

By Axiom of Choice define a mapping $g: \VV \to \C C$:

$\forall A \in \VV: A = \map g A^\circ_\R$

Define $K = \map {g^\to} \SS$

where $\map {g^\to} \SS$ denotes the image of $\SS$ under $g$.

Define $Y := \R \setminus \bigcup K$

By definition of cover:

$\R \subseteq \bigcup \CC$

By definition of subset:

$\forall x \in \R: x \in \bigcup \CC$

By definition of union:

$\forall x \in \R: \exists U \in \CC: x \in U$

By Axiom of Choice define a mapping $f: \R \to \CC$ such that

$\forall x \in \R: x \in \map f x$

Define $\BB := \set {\hointr x y: x, y \in \R}$

By definition of the Sorgenfrey line:

$\BB$ is a basis of $T$.

By definition of $f$:

$\forall x \in \R: \map f x \in \CC$

By definition of open cover:

$\forall x \in \R: \map f x$ is open

By definition of a basis:

$\forall x \in \R: \exists U_x \in \BB: x \in U_x \subseteq \map f x$

By definition of $\BB$:

$\forall x \in \R: \exists y, z \in \R: x \in \hointr y z \subseteq \map f x$

By definition of half-open real interval:

$\forall x \in \R: \exists z \in \R: x \in \hointr x z \subseteq \map f x$

By Axiom of Choice define a mapping $k: \R \to \BB$:

$\forall x \in \R: \exists z \in \R: x \in \map k x = \hointr x z \subseteq \map f x$

We will prove that

$(1): \quad \forall x, y \in Y: x \ne y \implies \paren x \cap \map k y = \O$

Let $x, y \in Y$ such that $x \ne y$.

Aiming for a contradiction, suppose:

$\paren x \cap \map k y \ne \O$

By definitions of empty set and intersection:

$\exists s: s \in \map k x \land s \in \map k y$

By definition of $k$:

$\exists z_1 \in \R: \map k x = \hointr x {z_1} \subseteq \map f x$

and

$\exists z_2 \in \R: \map k y = \hointr y {z_2}$
$x < y$ or $x > y$

Without loss of generality, suppose $x < y$

By definition of half-open real interval:

$x \le s < z_1$ and $y \le s < z_2$

Then: $y < z_1$

By definition of open real interval:

$y \in \openint x {z_1}$
$\openint x {z_1}$ is topologically open in $R$

By definition of subset:

$\openint x {z_1} \subseteq \hointr x {z_1}$
$\openint x {z_1} \subseteq \map f x$
$\openint x {z_1}^\circ_\R \subseteq \map f x^\circ_\R$
$\openint x {z_1}^\circ_\R \openint x z_1$

By definition of subset:

$y \in \map f x^\circ_\R$

By definition of $\VV$:

$\map f x^\circ_\R \in \VV$

By definition of union: $y \in W$

By definition of interior:

$\forall A \in \SS: A \subseteq \map g A$
$W \subseteq \bigcup \SS \subseteq \bigcup K$

By definition of subset:

$y \in \bigcup K$

This contradicts $y \in Y$ by definition of difference.

Thus:

$\map k x \cap \map k y = \O$
$\map {k^\to} Y$ is countable

We will prove that

$k \restriction_Y$ is an injection

Let $x, y \in Y$ such that

$\map {k \restriction_Y} x = \map {k \restriction_Y} Y$

Aiming for a contradiction, suppose:

$x \ne y$

Then by $(1)$:

$\map k x \cap \map k y = \O$

By definition of restriction of mapping:

$\map {k \restriction_Y} x = \map k x$

and

$\map {k \restriction_Y} y = \map k y$

By definition of $k$:

$x \in \map k x$

So:

$x \in \map k y$

$\map k x \cap k \map k y = \O$

Thus $x = y$.

$k \restriction_Y: Y \to \map {k^\to} Y$ is a bijection

By definitions of set equivalence and cardinality:

$\card Y = \card {\map {k^\to} Y}$

where $\card Y$ denotes the cardinality of $Y$.

$\card K \le \card \SS$ and $\card {\map {f^\to} Y} \le \card Y$
$\card \SS \le \aleph_0$ and $\card Y \le \aleph_0$

Then:

$\card K \le \aleph_0$ and $\card {\map {f^\to} Y} \le \aleph_0$
$K$ is countable and $\map {f^\to} Y$ is countable
$\GG := K \cup \map {f^\to} Y$ is countable

By definition of image of set:

$K \subseteq \CC$ and $\map {f^\to} Y \subseteq \CC$
$\GG \subseteq \CC$

It remains to prove that

$\GG$ is cover for $\R$

Let $x \in \R$.

$\bigcup \GG = \paren {\bigcup K} \cup \bigcup \map {f^\to} Y$

Aiming for a contradiction, suppose:

$x \notin \bigcup \GG$

By definition of union:

$x \notin \bigcup K$ and $x \notin \bigcup \map {f^\to} Y$

By definition of difference:

$x in Y$

By definition of image of set:

$\map f x \in \map {f^\to} Y$

By definition of $f$:

$x \in \map f x$

By definition of union:

$x \in \bigcup \map {f^\to} Y$

This contradicts $x \notin \bigcup \map {f^\to} Y$.

Thus the result by Proof by Contradiction.

$\blacksquare$