Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-17 13:09 d8d25e9a

View on Github →

refactor(analysis/normed_space/deriv): split and move to calculus folder (#1135)

Estimated changes

deleted theorem is_open.unique_diff_on
deleted theorem tangent_cone_at.lim_zero
deleted def tangent_cone_at
deleted theorem tangent_cone_inter_open
deleted theorem tangent_cone_mono
deleted theorem tangent_cone_univ
deleted def unique_diff_on
deleted theorem unique_diff_on_inter
added theorem is_open.unique_diff_on
added def tangent_cone_at
added theorem tangent_cone_mono
added theorem tangent_cone_univ
added def unique_diff_on
added theorem unique_diff_on_inter