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.

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

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

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_rat (a : Counterexample.SorgenfreyLine) :
        (nhds a).HasCountableBasis (fun (r : ) => a < r) fun (r : ) => Set.Ico a r
        theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_inv_pnat (a : Counterexample.SorgenfreyLine) :
        (nhds a).HasBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (↑n)⁻¹)
        theorem Counterexample.SorgenfreyLine.nhds_countable_basis_Ico_inv_pnat (a : Counterexample.SorgenfreyLine) :
        (nhds a).HasCountableBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (↑n)⁻¹)
        @[simp]
        theorem Counterexample.SorgenfreyLine.map_toReal_nhds (a : Counterexample.SorgenfreyLine) :
        Filter.map (⇑Counterexample.SorgenfreyLine.toReal) (nhds a) = nhdsWithin (Counterexample.SorgenfreyLine.toReal a) (Set.Ici (Counterexample.SorgenfreyLine.toReal a))
        theorem Counterexample.SorgenfreyLine.nhds_eq_map (a : Counterexample.SorgenfreyLine) :
        nhds a = Filter.map (⇑Counterexample.SorgenfreyLine.toReal.symm) (nhdsWithin (Counterexample.SorgenfreyLine.toReal a) (Set.Ici (Counterexample.SorgenfreyLine.toReal a)))
        theorem Counterexample.SorgenfreyLine.nhds_eq_comap (a : Counterexample.SorgenfreyLine) :
        nhds a = Filter.comap (⇑Counterexample.SorgenfreyLine.toReal) (nhdsWithin (Counterexample.SorgenfreyLine.toReal a) (Set.Ici (Counterexample.SorgenfreyLine.toReal a)))

        Sorgenfrey line is a completely normal topological space. (Hausdorff follows as TotallyDisconnectedSpace → T₁)

        Equations

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

        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.