Skip to content

feat(Analysis/Calculus): monotonicity from nonnegative lower right Dini derivative outside a countable set#41552

Draft
benjub wants to merge 1 commit into
leanprover-community:masterfrom
benjub:monotone
Draft

feat(Analysis/Calculus): monotonicity from nonnegative lower right Dini derivative outside a countable set#41552
benjub wants to merge 1 commit into
leanprover-community:masterfrom
benjub:monotone