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.