MonDecFuncs

class proveit.numbers.MonDecFuncs(domain, *, codomain=Real, styles=None, _operator=None)

Bases: proveit.Function

MonDecFuncs denotes the set of monotonically-decreasing functions on some domain D and codomain C and is meant to capture and articulate properties of functions such as 1/x^2 on (0, infty).

The initial development here is based on some analogous code and related concepts/structures in the VecSpaces() class, some pieces of which remain below despite their relevance still being questionable. This comment paragraph can eventually be deleted.

We might eventually include a user-specifiable ordering for the domain, but assume for the time being that all orderings use the standard less than ordering < .

Attributes Summary

default_domain
is_proper_class	The collection of monotonically-decreasing functions over a domain D with codomain C consistitutes a set instead of a proper class.
known_mon_dec_funcs_memberships

Methods Summary

membership_object(self, element)

Attributes Documentation

default_domain = None

is_proper_class

The collection of monotonically-decreasing functions over a domain D with codomain C consistitutes a set instead of a proper class. Thus we can use the standard InSet when considering the collection as a domain.

known_mon_dec_funcs_memberships = {}

Methods Documentation

membership_object(self, element)