mathlib3 documentation

mathlib-counterexamples / sorgenfrey_line

Sorgenfrey line #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define sorgenfrey_line (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.

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

Equations
@[protected, instance]

Sorgenfrey line is a completely normal Hausdorff topological space.

The product of the Sorgenfrey line and itself is not a normal topological space.