Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 00:42 a7410df0

View on Github →

feat(analysis/calculus/tangent_cone): add unique_diff_on.pi (#6577)

Estimated changes

Modified src/analysis/calculus/tangent_cone.lean

added theorem maps_to_tangent_cone_pi

added theorem unique_diff_on.pi

added theorem unique_diff_on.univ_pi

added theorem unique_diff_within_at.pi

added theorem unique_diff_within_at.univ_pi

Modified src/analysis/normed_space/basic.lean

added theorem eventually_nhds_norm_smul_sub_lt