Commit 2026-08-18 20:39 ab146e52

View on Github →

feat: API for (co)discrete sets (#42227) Establish simple but useful API for dealing with (co)discrete sets.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Roots.lean

added theorem Polynomial.eventually_cofinite_not_isRoot

added theorem Polynomial.eventually_eval_ne_zero_cofinite

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem Filter.EventuallyEq.codiscreteWithin_deriv

added theorem Filter.EventuallyEq.codiscreteWithin_derivWithin'

added theorem Filter.EventuallyEq.codiscreteWithin_derivWithin

added theorem Filter.EventuallyEq.codiscrete_deriv

added theorem Filter.EventuallyEq.codiscrete_derivWithin

Modified Mathlib/Analysis/Calculus/FDeriv/Congr.lean

added theorem Filter.EventuallyEq.codiscreteWithin_fderiv

added theorem Filter.EventuallyEq.codiscreteWithin_fderivWithin'

added theorem Filter.EventuallyEq.codiscreteWithin_fderivWithin

added theorem Filter.EventuallyEq.codiscrete_fderiv

added theorem Filter.EventuallyEq.codiscrete_fderivWithin

Modified Mathlib/Analysis/Complex/JensenFormula.lean

Modified Mathlib/Analysis/Meromorphic/IsolatedZeros.lean

Modified Mathlib/Analysis/Polynomial/Basic.lean

deleted theorem Polynomial.eventually_cofinite_not_isRoot

Modified Mathlib/Topology/Algebra/Polynomial.lean

added theorem Polynomial.eventually_eval_ne_zero_codiscrete

Modified Mathlib/Topology/DiscreteSubset.lean

modified theorem Filter.codiscreteWithin_mono

modified theorem Filter.self_mem_codiscreteWithin

modified theorem codiscreteWithin_iff_locallyEmptyComplementWithin

modified theorem codiscreteWithin_iff_locallyFiniteComplementWithin

added theorem eventuallyEq_codiscreteWithin_iff_forall_eventuallyEq_nhdsWithin

added theorem eventuallyEq_codiscreteWithin_iff_forall_eventually_nhdsNE

added theorem eventuallyEq_codiscrete_iff_forall_eventuallyEq_nhdsNE

added theorem eventually_codiscreteWithin_iff_forall_eventually_nhdsNE

added theorem eventually_codiscreteWithin_iff_forall_eventually_nhdsWithin

added theorem eventually_codiscrete_iff_forall_eventually_nhdsNE

modified theorem isClosed_sdiff_of_codiscreteWithin

added theorem mem_codiscreteWithin_iff_forall_mem_nhdsWithin

added theorem mem_codiscrete_iff_forall_mem_nhdsNE

added theorem nhdsNE_le_codiscrete

added theorem nhdsWithin_le_codiscreteWithin