Add monotone_of_tendsto and monotone_of_tendsto_of_eventually lemmas - #6

Add monotone_of_tendsto and monotone_of_tendsto_of_eventually lemmas#6

CoolRmal wants to merge 1 commit into

mainCoolRmal/mathlib4:mainfrom

codex/create-branch-for-monotone-functions-proofCoolRmal/mathlib4:codex/create-branch-for-monotone-functions-proofCopy head branch name to clipboard