mathlib

d0f392e1 - feat(analysis/calculus/inverse): a map which approximates a linear map on a set admits a nice global extension (#11568)

feat(analysis/calculus/inverse): a map which approximates a linear map on a set admits a nice global extension (#11568) And several other results on maps that are well approximated by linear maps on some subset of the space (not necessarily open).