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.NeBot (Filter.cocompact ℚ ⊓ nhds p)

Equations

• (_ : Filter.NeBot (Filter.cocompact ℚ ⊓ nhds p)) = (_ : Filter.NeBot (Filter.cocompact ℚ ⊓ nhds p))

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

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

theorem Rat.not_firstCountableTopology_opc : ¬FirstCountableTopology (OnePoint ℚ)

theorem Rat.not_secondCountableTopology_opc : ¬SecondCountableTopology (OnePoint ℚ)

instance Rat.instTotallyDisconnectedSpaceRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRat : TotallyDisconnectedSpace ℚ

Equations

• Rat.instTotallyDisconnectedSpaceRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRat = (_ : TotallyDisconnectedSpace ℚ)