# 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$

By Union is Smallest Superset:

- $W := \bigcup \VV \subseteq \R$

By Topological Subspace of Real Number Line is Lindelöf:

- $R_W$ is Lindelöf

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

By Set is Subset of Union/Set of Sets:

- $\forall A \in \VV: A \subseteq W$

By Intersection with Subset is Subset:

- $\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}$

By Trichotomy Law for Real Numbers:

- $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}$

By Open Real Interval is Open Set:

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

By definition of subset:

- $\openint x {z_1} \subseteq \hointr x {z_1}$

By Subset Relation is Transitive:

- $\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$

By Set Union Preserves Subsets:

- $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$

By Set of Pairwise Disjoint Intervals is Countable

- $\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$

This contradicts:

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

Thus $x = y$.

By Injection to Image is Bijection:

- $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$.

By Cardinality of Image of Set not greater than Cardinality of Set:

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

By Countable iff Cardinality not greater than Aleph Zero:

- $\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$

By Countable iff Cardinality not greater than Aleph Zero:

Thus by Countable Union of Countable Sets 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$

thus by corollary of Set Union Preserves Subsets:

- $\GG \subseteq \CC$

It remains to prove that

- $\GG$ is cover for $\R$

Let $x \in \R$.

By Union Distributes over Union: Sets of Sets:

- $\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$

## Sources

- Mizar article TOPGEN_6:Lm9