Hereditary separability of linear orders

In this file we prove some results about a separable linearly ordered topological space.

Main results

• exists_isOpen_ordConnected_mem_subset: every point of an open set has an open order connected neighbourhood contained in that set.
• isTopologicalBasis_isOpen_ordConnected: the open order connected sets form a topological basis.
• countable_ofPred_isolated_subtype: in a separable linearly ordered topological space, the points of a subset that are isolated in the subspace topology form a countable set.
• countable_ofPred_isolated_within: the same statement for the points x ∈ s with 𝓝[s \ {x}] x = ⊥, as a set in α.
• Set.separableSpace: a separable linearly ordered topological space is hereditarily separable.

TODO

Define the class of GO-spaces and generalize the hereditary separability result.

theorem exists_isOpen_ordConnected_mem_subset {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {U : Set α} (hU : IsOpen U) {x : α} (hx : x ∈ U) : ∃ (V : Set α), IsOpen V ∧ V.OrdConnected ∧ x ∈ V ∧ V ⊆ U

Every point x of an open set U has an open order connected neighbourhood contained in U.

theorem isTopologicalBasis_isOpen_ordConnected {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : TopologicalSpace.IsTopologicalBasis {V : Set α | IsOpen V ∧ V.OrdConnected}

The open order connected sets form a topological basis of a linearly ordered topological space.

theorem nhds_basis_isOpen_ordConnected {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] (x : α) : (nhds x).HasBasis (fun (V : Set α) => (IsOpen V ∧ V.OrdConnected) ∧ x ∈ V) id

The open order connected sets containing a point form a basis of its neighbourhood filter.

theorem countable_ofPred_isolated_subtype {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace.SeparableSpace α] (s : Set α) : {x : ↑s | IsOpen {x}}.Countable

In a separable linearly ordered topological space, the points of a subset s that are isolated in the subspace s form a countable set.

theorem countable_ofPred_isolated_within {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace.SeparableSpace α] {s : Set α} : {x : α | x ∈ s ∧ nhdsWithin x (s \ {x}) = ⊥}.Countable

In a separable linearly ordered topological space, the points of a subset s that are isolated within s form a countable set.

instance Set.separableSpace {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace.SeparableSpace α] (s : Set α) : TopologicalSpace.SeparableSpace ↑s

A separable linearly ordered topological space is hereditarily separable: every subset, equipped with the subspace topology, is a separable space.