Commit 2025-02-26 18:08 b4e9bce0

feat: preimages of codiscrete sets under analytic function in one variable (#21594) Establish corollary of the "principle of isolated zeros": for analytic functions in one variable, the preimage of a set that is codiscrete within the range is codiscrete within the domain. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. More precisely, it is used when replacing meromorphic functions by their continuous extension, and functions of the form log |f*g| by log |f| + log |g|. In both instances, the functions remain unchanged along codiscrete sets, which makes the change irrelevant for integration.