Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-16 08:11 05457fdd

View on Github →

feat(analysis/calculus/tangent_cone): define and use tangent_cone_congr (#1886)

  • feat(analysis/calculus/tangent_cone): define and use tangent_cone_congr This way some proofs become shorter and hopefully more readable.
  • Add a docstring

Estimated changes

added theorem tangent_cone_congr
added theorem tangent_cone_mono_nhds