mathlib3
8fb92bf1 - feat(measure_theory/integral/circle_integral): add lemma `circle_map_nmem_ball` (#14643)

Commit
3 years ago
feat(measure_theory/integral/circle_integral): add lemma `circle_map_nmem_ball` (#14643) The lemma `set.ne_of_mem_nmem` is unrelated except that both of these should be helpful for: https://github.com/leanprover-community/mathlib/pull/13885
Author
Parents
Loading