Documentation

Counterexamples.SorgenfreyLine

Sorgenfrey line #

In this file we define SorgenfreyLine (notation: ℝₗ) to be the Sorgenfrey line. It is the real line with the topology space structure generated by half-open intervals Set.Ico a b.

We prove that this line is a completely normal Hausdorff space but its product with itself is not a normal space. In particular, this implies that the topology on ℝₗ is neither metrizable, nor second countable.

Notations #

TODO #

Prove that the Sorgenfrey line is a paracompact space.

The Sorgenfrey line. It is the real line with the topology space structure generated by half-open intervals Set.Ico a b.

Instances For

    Ring homomorphism between the Sorgenfrey line and the standard real line.

    Instances For

      Any subset of an antidiagonal {(x, y) : ℝₗ × ℝₗ| x + y = c} is a closed set.

      An antidiagonal is a separable set but is not a separable space.

      An antidiagonal is a separable set but is not a separable space.

      The sets of rational and irrational points of the antidiagonal {(x, y) | x + y = 0} cannot be separated by open neighborhoods. This implies that ℝₗ × ℝₗ is not a normal space.