Commit 2022-04-29 06:35 992e26fa

View on Github →

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.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem vadd_vsub_eq_sub_vsub

added theorem vsub_ne_zero

Modified src/analysis/normed/group/basic.lean

added theorem ball_eq

added theorem normed_group.nhds_basis_norm_lt

added theorem normed_group.nhds_zero_basis_norm_lt

Modified src/analysis/normed_space/add_torsor.lean

modified theorem affine_subspace.is_closed_direction_iff

modified theorem antilipschitz_with_line_map

added theorem eventually_homothety_image_subset_of_finite_subset_interior

added theorem eventually_homothety_mem_of_mem_interior