Commit 2023-08-25 14:43 e561ee7a
View on Github →chore: remove duplicate lemma HasFDerivWithinAt.nhdsWithin (#6773)
This is a perfect duplicate of HasFDerivWithinAt.mono_of_mem.
Same thing with Deriv instead of FDeriv.
chore: remove duplicate lemma HasFDerivWithinAt.nhdsWithin (#6773)
This is a perfect duplicate of HasFDerivWithinAt.mono_of_mem.
Same thing with Deriv instead of FDeriv.