Documentation

Mathlib.Topology.Instances.RatLemmas

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 #

Notation #

Equations
  • =
theorem Rat.not_countably_generated_nhds_infty_opc :
¬(nhds OnePoint.infty).IsCountablyGenerated