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.

Notation

• ℝₗ: Sorgenfrey line.

TODO

Prove that the Sorgenfrey line is a paracompact space.

def Counterexample.SorgenfreyLine : Type

The Sorgenfrey line (denoted as ℝₗ within the SorgenfreyLine namespace). It is the real line with the topology space structure generated by half-open intervals Set.Ico a b.

Equations

• Counterexample.SorgenfreyLine = ℝ

@[implicit_reducible]

noncomputable instance Counterexample.instConditionallyCompleteLinearOrderSorgenfreyLine : ConditionallyCompleteLinearOrder SorgenfreyLine

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance Counterexample.instFieldSorgenfreyLine : Field SorgenfreyLine

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance Counterexample.instIsStrictOrderedRingSorgenfreyLine : IsStrictOrderedRing SorgenfreyLine

Equations

• Counterexample.instIsStrictOrderedRingSorgenfreyLine = Counterexample.instIsStrictOrderedRingSorgenfreyLine._proof_1

@[implicit_reducible]

noncomputable instance Counterexample.instArchimedeanSorgenfreyLine : Archimedean SorgenfreyLine

Equations

• Counterexample.instArchimedeanSorgenfreyLine = Counterexample.instArchimedeanSorgenfreyLine._proof_1

def SorgenfreyLine.termℝₗ : Lean.ParserDescr

The Sorgenfrey line (denoted as ℝₗ within the SorgenfreyLine namespace). 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 "ℝₗ")

def Counterexample.SorgenfreyLine.toReal : SorgenfreyLine ≃+* ℝ

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

Equations

• Counterexample.SorgenfreyLine.toReal = RingEquiv.refl ℝ

@[implicit_reducible]

instance Counterexample.SorgenfreyLine.instTopologicalSpace : TopologicalSpace SorgenfreyLine

Equations

• One or more equations did not get rendered due to their size.

theorem Counterexample.SorgenfreyLine.isOpen_Ico (a b : SorgenfreyLine) : IsOpen (Set.Ico a b)

theorem Counterexample.SorgenfreyLine.isOpen_Ici (a : SorgenfreyLine) : IsOpen (Set.Ici a)

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico (a : SorgenfreyLine) : (nhds a).HasBasis (fun (x : SorgenfreyLine) => a < x) fun (x : SorgenfreyLine) => Set.Ico a x

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_rat (a : SorgenfreyLine) : (nhds a).HasCountableBasis (fun (r : ℚ) => a < ↑r) fun (r : ℚ) => Set.Ico a ↑r

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_inv_pnat (a : SorgenfreyLine) : (nhds a).HasBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.nhds_countable_basis_Ico_inv_pnat (a : SorgenfreyLine) : (nhds a).HasCountableBasis (fun (x : ℕ+) => True) fun (n : ℕ+) => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.nhds_antitone_basis_Ico_inv_pnat (a : SorgenfreyLine) : (nhds a).HasAntitoneBasis fun (n : ℕ+) => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.isOpen_iff {s : Set SorgenfreyLine} : IsOpen s ↔ ∀ x ∈ s, ∃ y > x, Set.Ico x y ⊆ s

theorem Counterexample.SorgenfreyLine.isClosed_iff {s : Set SorgenfreyLine} : IsClosed s ↔ ∀ x ∉ s, ∃ y > x, Disjoint (Set.Ico x y) s

theorem Counterexample.SorgenfreyLine.exists_Ico_disjoint_closed {a : SorgenfreyLine} {s : Set SorgenfreyLine} (hs : IsClosed s) (ha : a ∉ s) : ∃ b > a, Disjoint (Set.Ico a b) s

@[simp]

theorem Counterexample.SorgenfreyLine.map_toReal_nhds (a : SorgenfreyLine) : Filter.map (⇑toReal) (nhds a) = nhdsWithin (toReal a) (Set.Ici (toReal a))

theorem Counterexample.SorgenfreyLine.nhds_eq_map (a : SorgenfreyLine) : nhds a = Filter.map (⇑toReal.symm) (nhdsWithin (toReal a) (Set.Ici (toReal a)))

theorem Counterexample.SorgenfreyLine.nhds_eq_comap (a : SorgenfreyLine) : nhds a = Filter.comap (⇑toReal) (nhdsWithin (toReal a) (Set.Ici (toReal a)))

theorem Counterexample.SorgenfreyLine.continuous_toReal : Continuous ⇑toReal

instance Counterexample.SorgenfreyLine.instOrderClosedTopology : OrderClosedTopology SorgenfreyLine

instance Counterexample.SorgenfreyLine.instContinuousAdd : ContinuousAdd SorgenfreyLine

theorem Counterexample.SorgenfreyLine.isClopen_Ici (a : SorgenfreyLine) : IsClopen (Set.Ici a)

theorem Counterexample.SorgenfreyLine.isClopen_Iio (a : SorgenfreyLine) : IsClopen (Set.Iio a)

theorem Counterexample.SorgenfreyLine.isClopen_Ico (a b : SorgenfreyLine) : IsClopen (Set.Ico a b)

instance Counterexample.SorgenfreyLine.instTotallyDisconnectedSpace : TotallyDisconnectedSpace SorgenfreyLine

instance Counterexample.SorgenfreyLine.instFirstCountableTopology : FirstCountableTopology SorgenfreyLine

instance Counterexample.SorgenfreyLine.instCompletelyNormalSpace : CompletelyNormalSpace SorgenfreyLine

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

theorem Counterexample.SorgenfreyLine.denseRange_ratCast : DenseRange Rat.cast

instance Counterexample.SorgenfreyLine.instSeparableSpace : TopologicalSpace.SeparableSpace SorgenfreyLine

theorem Counterexample.SorgenfreyLine.isClosed_antidiagonal (c : SorgenfreyLine) : IsClosed {x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = c}

theorem Counterexample.SorgenfreyLine.isClopen_Ici_prod (x : SorgenfreyLine × SorgenfreyLine) : IsClopen (Set.Ici x)

theorem Counterexample.SorgenfreyLine.cardinal_antidiagonal (c : SorgenfreyLine) : Cardinal.mk ↑{x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = c} = Cardinal.continuum

theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal {s : Set (SorgenfreyLine × SorgenfreyLine)} {c : SorgenfreyLine} (hs : ∀ x ∈ s, x.1 + x.2 = c) : IsClosed s

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

instance Counterexample.SorgenfreyLine.instDiscreteTopologyElemProdSetOfEqHAddFstSnd (c : SorgenfreyLine) : DiscreteTopology ↑{x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = c}

theorem Counterexample.SorgenfreyLine.not_normalSpace_prod : ¬NormalSpace (SorgenfreyLine × SorgenfreyLine)

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

theorem Counterexample.SorgenfreyLine.isSeparable_antidiagonal (c : SorgenfreyLine) : TopologicalSpace.IsSeparable {x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = c}

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

theorem Counterexample.SorgenfreyLine.not_separableSpace_antidiagonal (c : SorgenfreyLine) : ¬TopologicalSpace.SeparableSpace ↑{x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = c}

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

theorem Counterexample.SorgenfreyLine.nhds_prod_antitone_basis_inv_pnat (x y : SorgenfreyLine) : (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 : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = 0 ∧ ∃ (r : ℚ), ↑r = x.1} {x : SorgenfreyLine × SorgenfreyLine | x.1 + x.2 = 0 ∧ Irrational (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.

theorem Counterexample.SorgenfreyLine.not_metrizableSpace : ¬TopologicalSpace.MetrizableSpace SorgenfreyLine

Topology on the Sorgenfrey line is not metrizable.

theorem Counterexample.SorgenfreyLine.not_secondCountableTopology : ¬SecondCountableTopology SorgenfreyLine

Topology on the Sorgenfrey line is not second countable.