deduce_as_mon_dec_func

proveit.numbers.deduce_as_mon_dec_func(fxn, \*, domain=None, strict=False, \*\*defaults_config)

Prove that the Lambda-map specified by fxn is contained in the set of monotonically-decreasing functions defined over the domain. Unless strict is True, the returned proven membership may be over a broader domain (that is, a stronger statement than required).

For example, we might have fxn = Lambda(x, 1/x^2) and domain = RealPos, in which case we try to prove that Lambda(x, 1/x^2) is in the set of MonDecFuncs(RealPos).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.