mathlib3 documentation

topology.instances.rat_lemmas

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 #

Notation #

@[protected, instance]