{f,}deriv): generalize `has_fderiv_at_filter.is_O_sub_rev` (#10897)

Commit

4 years ago

feat(analysis/calculus/{f,}deriv): generalize `has_fderiv_at_filter.is_O_sub_rev` (#10897) Also add `has_deriv_at.is_O_sub_rev`

Author

urkud

Parents