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
.
Equations
Instances For
The Sorgenfrey line. It is the real line with the topology space structure generated by
half-open intervals Set.Ico a b
.
Equations
- SorgenfreyLine.termℝₗ = Lean.ParserDescr.node `SorgenfreyLine.termℝₗ 1024 (Lean.ParserDescr.symbol "ℝₗ")
Instances For
Ring homomorphism between the Sorgenfrey line and the standard real line.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Sorgenfrey line is a completely normal topological space. (Hausdorff follows as TotallyDisconnectedSpace → T₁)
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.
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.