Weight of Sorgenfrey Line is Continuum
Jump to navigation
Jump to search
Theorem
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Then $\map w T = \mathfrak c$
where
- $\map w T$ denotes the weight of $T$
- $\mathfrak c$ denotes continuum, the cardinality of real numbers.
Proof
By definition of Sorgenfrey line, the set:
- $\BB = \set {\hointr x y: x, y \in \R \land x < y}$
is a basis of $T$.
By definition of weight:
- $\map w T \le \card \BB$
where $\card \BB$ denotes the cardinality of $\BB$.
By Cardinality of Basis of Sorgenfrey Line not greater than Continuum:
- $\card \BB \le \mathfrak c$
Thus
- $\map w T \le \mathfrak c$
It remains to show that:
- $\mathfrak c \le \map w T$
Aiming for a contradiction, suppose
- $\mathfrak c \not \le \map w T$
Then:
- $\map w T < \mathfrak c$
By definition of weight, there exists a basis $\BB_0$ of $T$:
- $\map w T = \card {\BB_0}$
Then by Set of Subset of Reals with Cardinality less than Continuum has not Interval in Union Closure:
- $\exists x, y \in \R: x < y \land \hointr x y \notin \set {\bigcup A: A \subseteq \BB_0} = \tau$
By definition of $\BB$:
- $\hointr x y \in \BB \subseteq \tau$
Thus this contradicts by definition of subset with:
- $\hointr x y \notin \tau$
$\blacksquare$
Sources
- Mizar article TOPGEN_3:33