# 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
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 :
(nhds a).HasCountableBasis (fun (r : ) => a < r) fun (r : ) => Set.Ico a r
theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_inv_pnat :
(nhds a).HasBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (n)⁻¹)
theorem Counterexample.SorgenfreyLine.nhds_countable_basis_Ico_inv_pnat :
(nhds a).HasCountableBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (n)⁻¹)
theorem Counterexample.SorgenfreyLine.nhds_antitone_basis_Ico_inv_pnat :
(nhds a).HasAntitoneBasis fun (n : ℕ+) => Set.Ico a (a + (n)⁻¹)
theorem Counterexample.SorgenfreyLine.isOpen_iff :
xs, y > x, Set.Ico x y s
theorem Counterexample.SorgenfreyLine.isClosed_iff :
xs, y > x, Disjoint (Set.Ico x y) s
theorem Counterexample.SorgenfreyLine.exists_Ico_disjoint_closed (hs : ) (ha : as) :
b > a, Disjoint (Set.Ico a b) s
@[simp]
theorem Counterexample.SorgenfreyLine.map_toReal_nhds :
= nhdsWithin (Counterexample.SorgenfreyLine.toReal a) (Set.Ici (Counterexample.SorgenfreyLine.toReal a))
theorem Counterexample.SorgenfreyLine.nhds_eq_map :
nhds a = Filter.map (nhdsWithin (Counterexample.SorgenfreyLine.toReal a) (Set.Ici (Counterexample.SorgenfreyLine.toReal a)))
theorem Counterexample.SorgenfreyLine.nhds_eq_comap :
nhds a = Filter.comap (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
theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal (hs : xs, x.1 + x.2 = c) :

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

Equations
• =

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.nhds_prod_antitone_basis_inv_pnat :
(nhds (x, y)).HasAntitoneBasis fun (n : ℕ+) => Set.Ico x (x + (n)⁻¹) ×ˢ Set.Ico y (y + (n)⁻¹)
theorem Counterexample.SorgenfreyLine.not_separatedNhds_rat_irrational_antidiag :
¬SeparatedNhds {x : | x.1 + x.2 = 0 ∃ (r : ), r = x.1} {x : | x.1 + x.2 = 0 Irrational (Counterexample.SorgenfreyLine.toReal x.1)}

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.