Commit 2024-12-24 00:34 0c3ebf27

View on Github →

refactor: allow deriv to be used on topological vector spaces (#19108) Notably, this allows us to state results about derivatives of matrices, without the statement encoding a choice of norm. For now, it is not possible to prove any of these statements without locally constructing a norm. This generalizes:

  • HasFDerivAtFilter
  • HasFDerivWithinAt
  • HasFDerivAt
  • HasStrictFDerivAt
  • DifferentiableWithinAt
  • DifferentiableAt
  • fderivWithin
  • fderiv
  • DifferentiableOn
  • Differentiable
  • HasDerivAtFilter
  • HasDerivWithinAt
  • HasDerivAt
  • HasStrictDerivAt
  • derivWithin
  • deriv Continues from this Zulip thread.

Estimated changes