Commit 2021-09-28 01:02 8c5d93b0

View on Github →

feat(analysis/special_functions/complex/log): exp ⁻¹' s is countable (#9410) Also prove that the preimage of a countable set under an injective map is countable.

Estimated changes

Modified src/analysis/special_functions/complex/log.lean

added theorem complex.countable_preimage_exp

modified theorem complex.range_exp

Modified src/data/set/countable.lean

added theorem set.countable.preimage_of_inj_on

added theorem set.maps_to.countable_of_inj_on

Modified src/data/set/function.lean

added theorem set.injective_cod_restrict