Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-10 02:24 e25a5970

View on Github →

feat(analysis/calculus/tangent_cone): more properties of the tangent cone (#1136)

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/tangent_cone.lean

modified theorem is_open.unique_diff_within_at

added theorem mem_tangent_cone_of_segment_subset

added theorem subset_tangent_cone_prod_left

added theorem subset_tangent_cone_prod_right

modified theorem tangent_cone_at.lim_zero

added theorem tangent_cone_inter_nhds

deleted theorem tangent_cone_inter_open

added theorem unique_diff_on.prod

added theorem unique_diff_on_Icc_zero_one

added theorem unique_diff_on_convex

added theorem unique_diff_on_univ

added theorem unique_diff_within_at.inter

added theorem unique_diff_within_at.mono

added theorem unique_diff_within_at.prod

modified theorem unique_diff_within_at_inter

added theorem unique_diff_within_at_univ

deleted theorem unique_diff_within_univ_at