mathlib3

120cf5bc - doc(topology) add a library note about continuity lemmas (#9954)

doc(topology) add a library note about continuity lemmas (#9954) * This is a note with some tips how to formulate a continuity (or measurability, differentiability, ...) lemma. * I wanted to write this up after formulating `continuous.strans` in many "wrong" ways before discovering the "right" way. * I think many lemmas are not following this principle, and could be improved in generality and/or convenience by following this advice. * Based on experience from the sphere eversion project. * The note mentions a lemma that will be added in #9959, but I don't think we necessarily have to wait for that PR.