Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-19 14:44 47ea2a6e

View on Github →

feat(topology, analysis) : add lemmas about has_neg.neg (preliminaries for L'Hopital's rule) (#3392) This PR contains a few lemmas about the has_neg.neg function, such as :

  • its limit along at_top and at_bot
  • its limit along nhds a, nhds_within a (Ioi a) and similar filters
  • its differentiability and derivative

Estimated changes

added theorem deriv.neg'
added theorem deriv.neg
added theorem deriv_neg''
modified theorem deriv_neg'
modified theorem deriv_neg
added theorem deriv_within.neg
modified theorem deriv_within_neg
added theorem differentiable_neg
added theorem differentiable_on_neg
added theorem has_deriv_at_neg'
added theorem has_deriv_at_neg
modified theorem filter.eventually_at_top
modified theorem filter.frequently_at_top'
modified theorem filter.frequently_at_top
added theorem filter.tendsto_at_bot'
added theorem filter.tendsto_at_bot
modified theorem filter.tendsto_at_top_pure
added theorem continuous_on_inv
added theorem tendsto_inv