Theorem mem_codiscreteWithin_accPt

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_codiscreteWithin_accPt View on Github →