mathlib documentation

topology.instances.rat_lemmas

Additional lemmas about the topology on rational numbers #

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 #

Notation #

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 ℚ