Additional lemmas about the topology on rational numbers

The structure of a metric space on ℚ (Rat.MetricSpace) is introduced elsewhere, induced from ℝ. In this file we prove some properties of this topological space and its one-point compactification.

Main statements

• Rat.TotallyDisconnectedSpace: ℚ is a totally disconnected space;

• Rat.not_countably_generated_nhds_infty_opc: the filter of neighbourhoods of infinity in OnePoint ℚ is not countably generated.

Notation

• ℚ∞ is used as a local notation for OnePoint ℚ

theorem Rat.interior_compact_eq_empty {s : Set ℚ} (hs : IsCompact s) : interior s = ∅

theorem Rat.dense_compl_compact {s : Set ℚ} (hs : IsCompact s) : Dense sᶜ

instance Rat.cocompact_inf_nhds_neBot {p : ℚ} : (Filter.cocompact ℚ ⊓ nhds p).NeBot

theorem Rat.not_countably_generated_cocompact : ¬(Filter.cocompact ℚ).IsCountablyGenerated

theorem Rat.not_countably_generated_nhds_infty_opc : ¬(nhds OnePoint.infty).IsCountablyGenerated

theorem Rat.not_firstCountableTopology_opc : ¬FirstCountableTopology (OnePoint ℚ)

theorem Rat.not_secondCountableTopology_opc : ¬SecondCountableTopology (OnePoint ℚ)

instance Rat.instTotallyDisconnectedSpace : TotallyDisconnectedSpace ℚ