Theorem Filter.codiscreteWithin.mono

Modification history

2025-02-26 18:08
Mathlib/Topology/DiscreteSubset.lean
feat: preimages of codiscrete sets under analytic function in one variable (#21594) …
Added Filter.codiscreteWithin.monoView on Github →