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

• ℝₗ: Sorgenfrey line.

## 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
Instances For

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

Instances For

Sorgenfrey line is a completely normal Hausdorff topological space.

theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal (hs : ∀ (x : ), x sx.fst + x.snd = c) :

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

The Sorgenfrey plane ℝₗ × ℝₗ is not a normal space.

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

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

theorem Counterexample.SorgenfreyLine.not_separatedNhds_rat_irrational_antidiag :
¬SeparatedNhds {x | x.fst + x.snd = 0 r, r = x.fst} {x | x.fst + x.snd = 0 }

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.

Topology on the Sorgenfrey line is not metrizable.

Topology on the Sorgenfrey line is not second countable.