affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766)

Commit

3 years ago

feat(topology/algebra/affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

b4cad379

mathlib3 992e26fa - feat(topology/algebra/affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766)

mathlib3
992e26fa - feat(topology/algebra/affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766)