Mathlib Changelog
v4
Changelog
About
Github
Theorem
Filter.HasBasis.isCountablyGenerated
Modification history
2024-03-08 18:41
Mathlib/Order/Filter/Bases.lean
feat(UniformSpace/CompactConvergence): prove metrizability (#10942)
Added
Filter.HasBasis.isCountablyGenerated
View on Github →