# mathlibdocumentation

topology.instances.rat_lemmas

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

## Main statements #

• rat.totally_disconnected_space: ℚ is a totally disconnected space;

• rat.not_countably_generated_nhds_infty_alexandroff: the filter of neighbourhoods of infinity in alexandroff ℚ is not countably generated.

## Notation #

• ℚ∞ is used as a local notation for alexandroff ℚ
theorem rat.dense_compl_compact {s : set } (hs : is_compact s) :
@[protected, instance]
@[protected, instance]