Additional lemmas about the topology on rational numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ℚ

source

theorem rat.interior_compact_eq_empty {s : set ℚ} (hs : is_compact s) :

interior s = ∅

source

theorem rat.dense_compl_compact {s : set ℚ} (hs : is_compact s) :

dense sᶜ

source

@[protected, instance]

def rat.cocompact_inf_nhds_ne_bot {p : ℚ} :

(filter.cocompact ℚ ⊓ nhds p).ne_bot

source

theorem rat.not_countably_generated_cocompact :

¬(filter.cocompact ℚ).is_countably_generated

source

theorem rat.not_countably_generated_nhds_infty_alexandroff :

¬(nhds alexandroff.infty).is_countably_generated

source

theorem rat.not_first_countable_topology_alexandroff :

¬topological_space.first_countable_topology (alexandroff ℚ)

source

theorem rat.not_second_countable_topology_alexandroff :

¬topological_space.second_countable_topology (alexandroff ℚ)

source

@[protected, instance]

def rat.totally_disconnected_space :

totally_disconnected_space ℚ