Mathlib Changelog
v4
Changelog
About
Github
Theorem
mem_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) …
Added
mem_codiscrete'
View on Github →