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$

There is believed to be a mistake here, possibly a typo. In particular: For $\paren x$ should it really be $\map k x$? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Mistake}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

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$

By Interior of Subset:

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

By Interior of Open Set:

$\openint x {z_1}^\circ_\R \openint x z_1$

There is believed to be a mistake here, possibly a typo. In particular: The relation is missing in the above -- subset or equals? Research needed You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Mistake}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

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:

$K$ is countable and $\map {f^\to} Y$ is countable

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 Set Union is Self-Distributive: 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

• 1989: Ryszard Engelking: General Topology (revised and completed ed.)

• Mizar article TOPGEN_6:Lm9