Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-24 09:36
104cb177
View on Github →
feat: port Topology.Instances.RatLemmas (
#4277
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Topology/Instances/RatLemmas.lean
added
theorem
Rat.dense_compl_compact
added
theorem
Rat.interior_compact_eq_empty
added
theorem
Rat.not_countably_generated_cocompact
added
theorem
Rat.not_countably_generated_nhds_infty_alexandroff
added
theorem
Rat.not_firstCountableTopology_alexandroff
added
theorem
Rat.not_secondCountableTopology_alexandroff