NumberOperation¶
-
class
proveit.numbers.
NumberOperation
(operator, operand_or_operands, *, styles=None)[source]¶ Bases:
proveit.Operation
Base class for number operation (i.e. arithmetic operations).
Methods Summary
bound_via_operand_bound
(self, operand_bound, …)Return a bound of this arithmetic expression based upon the bound of one of its operands.
deduce_bound
(self, inner_expr_bound_or_bounds)Return a bound of this arithmetic expression based upon the bounds of any number of inner expressions.
Methods Documentation
-
bound_via_operand_bound
(self, operand_bound, \*\*defaults_config)[source]¶ Return a bound of this arithmetic expression based upon the bound of one of its operands. The operand should appear on the left side of the operand_bound which should be a number ordering relation (< or <=). The returned, proven bound will have this expression on the left-hand side.
Also see NumberOperation.deduce_bound.
Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
-
deduce_bound
(self, inner_expr_bound_or_bounds, inner_exprs_to_bound=None, \*\*defaults_config)[source]¶ Return a bound of this arithmetic expression based upon the bounds of any number of inner expressions. The inner expression should appear on the left side of the corresponding bound which should be a number ordering relation (< or <=). The returned, proven bound will have this expression on the left-hand side. The bounds of the inner expressions will be processed in the order they are provided.
If inner_exprs_to_bound is provided, restrict the bounding to these particular InnerExpr objects. Otherwise, all inner expressions are fair game.
Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
-