Commit 2023-10-30 11:10 b71f1c84
View on Github →feat: add Set.InjOn.exists_mem_nhdsSet (#7947)
A continuous function injective on a compact set
and injective on a neighborhood of each point of this set
is injective on a neighborhood of this set.
From the Mandelbrot set connectedness project.