how to prove this by calculating derivatives?

Stream: general

[Zihao Zhang]

how to prove this by calculating derivatives?

import Mathlib
example : (fun x : ℝ => Real.exp x) >= (fun x => x+1) := by

[Edward van de Meent]

@loogle "fderiv", "mono"

[loogle]

:search: HasFDerivWithinAt.mono, HasFDerivAtFilter.mono, and 13 more

[Edward van de Meent]

i was slightly off with my loogle... you will find a relevant theorem around docs#strictMonoOn_of_hasDerivWithinAt_pos

[Edward van de Meent]

TIL the difference between docs#deriv and docs#fderiv