Theorem Filter.isCountablyGenerated_seq

Modification history

2024-03-08 18:41

Mathlib/Order/Filter/Bases.lean

feat(UniformSpace/CompactConvergence): prove metrizability (#10942)

Modified Filter.isCountablyGenerated_seq View on Github →

2023-01-24 07:28

Mathlib/Order/Filter/Bases.lean

Feat: port Order.Filter.Bases (#1791)

Added Filter.isCountablyGenerated_seq View on Github →