Def Filter.codiscrete

Modification history

2024-08-24 16:50
Mathlib/Topology/DiscreteSubset.lean
feat(Topology/DiscreteSubset): prove lemmas about the codiscrete filter, and define codiscreteWithin (#14837) …
Modified Filter.codiscreteView on Github →
2023-10-11 21:40
Mathlib/Topology/Compactness/Compact.lean
chore(Topology/SubsetProperties): Refactor SubsetProperties.lean (#7628) …
Modified Filter.codiscreteView on Github →
2023-10-09 21:43
Mathlib/Topology/SubsetProperties.lean
feat(Topology/Separation): filter of codiscrete sets (#7456) …
Added Filter.codiscreteView on Github →