Commit 2024-08-24 16:50 8b65e4b6

View on Github →

feat(Topology/DiscreteSubset): prove lemmas about the codiscrete filter, and define codiscreteWithin (#14837) Prove lemmas about the codiscrete filter.

Estimated changes

Modified Mathlib/Topology/DiscreteSubset.lean

modified def Filter.codiscrete

added def Filter.codiscreteWithin

added theorem mem_codiscrete'

added theorem mem_codiscrete

added theorem mem_codiscreteWithin

added theorem mem_codiscreteWithin_accPt

added theorem mem_codiscrete_accPt

added theorem mem_codiscrete_subtype_iff_mem_codiscreteWithin