LessEq

class proveit.numbers.LessEq(a, b, *, styles=None)

Bases: proveit.numbers.NumberOrderingRelation

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

add(self, relation, \*\*defaults_config)	From a <= b, derive and return a + c <= b + d given c <= d (and a, b, c, d are all Real).
add_left(self, addend, \*[, strong])	From a <= b, derive and return a + c <= b given c <= 0 Or from a >= b, derive and return a + c >= b given 0 <= c (and a, b, c are all Real) where c is the given ‘addend’.
add_right(self, addend, \*[, strong])	From a <= b, derive and return a <= b + c given 0 <= c Or from a >= b, derive and return a >= b + c given c <= 0 (and a, b, c are all Real) where c is the given ‘addend’.
apply_transitivity(self, other, …)	Apply a transitivity rule to derive from this x<=y expression and something of the form y<z, y<=z, z>y, z>=y, or y=z to obtain x<z or x<=z as appropriate.
conclude_via_equality(self, \*\*defaults_config)	Conclude a ≤ b from a = b.
deduce_in_bool(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
derive_negated(self, \*\*defaults_config)	From a <= b, derive and return -b <= -a.
derive_shifted(self, addend[, addend_side])	From a <= b, derive and return a + c <= b + c where c is the given ‘addend’.
divide_both_sides(self, divisor, …)	Divide both sides of the relation by the ‘divisor’.
exponentiate_both_sides(self, exponent, …)	Exponentiate both sides of the relation by the ‘exponent’.
left_add_both_sides(self, addend, …)	Add to both sides of the relation by the ‘addend’ on the left.
left_mult_both_sides(self, multiplier, …)	Multiply both sides of the relation by the ‘multiplier’ on the left.
remake_constructor(self)	Method to call to reconstruct this Expression.
reversed_operator_str(formatType)	Reversing ‘<=’ gives ‘>=’.
right_add_both_sides(self, addend, …)	Add to both sides of the relation by the ‘addend’ on the right.
right_mult_both_sides(self, multiplier, …)	Multiply both sides of the relation by the ‘multiplier’ on the right.
unfold(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

Attributes Documentation

known_left_sides = {0: OrderedSet([{_a in Natural} |- 0 <= _a, {n in Natural} |- n >= 0, |- 0 >= 0, |- 1 >= 0, {_a in RationalNonNeg} |- 0 <= _a, {q in RationalNonNeg} |- q >= 0, {_a in RealNonNeg} |- 0 <= _a, {x in RealNonNeg} |- x >= 0, |- 2 >= 0, |- 3 >= 0, |- 4 >= 0, |- 5 >= 0, |- 6 >= 0, |- 7 >= 0, |- 8 >= 0, |- 9 >= 0, |- e >= 0, |- pi >= 0]), _b: OrderedSet([{_b <= _a} |- _b <= _a, {_b < _a} |- _b <= _a]), x: OrderedSet([{x <= y} |- x <= y, {x in RealNonPos} |- x <= 0, {x < y} |- x <= y]), _a: OrderedSet([{_a in IntegerNonPos} |- _a <= 0, {_a in RationalNonPos} |- _a <= 0, {_a in RealNonPos} |- _a <= 0, {_b in Real, _a in Real, [not](_b < _a)} |- _a <= _b]), a: OrderedSet([{a in IntegerNonPos} |- a <= 0]), q: OrderedSet([{q in RationalNonPos} |- q <= 0]), y: OrderedSet([{x in Real, y in Real, [not](x < y)} |- y <= x]), 1: OrderedSet([|- 1 <= 2, {_a in NaturalPos} |- 1 <= _a, {n in NaturalPos} |- n >= 1, |- 1 >= 1, |- 3 >= 1, |- 4 >= 1, |- 5 >= 1, |- 6 >= 1, |- 7 >= 1, |- 8 >= 1, |- 9 >= 1]), 2: OrderedSet([|- 2 <= 3]), 3: OrderedSet([|- 3 <= 4]), 4: OrderedSet([|- 4 <= 5]), 5: OrderedSet([|- 5 <= 6]), 6: OrderedSet([|- 6 <= 7]), 7: OrderedSet([|- 7 <= 8]), 8: OrderedSet([|- 8 <= 9])}

known_right_sides = {_a: OrderedSet([{_a in Natural} |- 0 <= _a, {_b <= _a} |- _b <= _a, {_a in RationalNonNeg} |- 0 <= _a, {_a in RealNonNeg} |- 0 <= _a, {_b < _a} |- _b <= _a, {_a in NaturalPos} |- 1 <= _a]), n: OrderedSet([{n in Natural} |- n >= 0, {n in NaturalPos} |- n >= 1]), 0: OrderedSet([|- 0 >= 0, {_a in IntegerNonPos} |- _a <= 0, {a in IntegerNonPos} |- a <= 0, {_a in RationalNonPos} |- _a <= 0, {q in RationalNonPos} |- q <= 0, {_a in RealNonPos} |- _a <= 0, {x in RealNonPos} |- x <= 0]), y: OrderedSet([{x <= y} |- x <= y, {x < y} |- x <= y]), 1: OrderedSet([|- 1 >= 0, |- 1 >= 1]), q: OrderedSet([{q in RationalNonNeg} |- q >= 0]), x: OrderedSet([{x in RealNonNeg} |- x >= 0, {x in Real, y in Real, [not](x < y)} |- y <= x]), 2: OrderedSet([|- 2 >= 0, |- 1 <= 2]), 3: OrderedSet([|- 3 >= 0, |- 2 <= 3, |- 3 >= 1]), 4: OrderedSet([|- 4 >= 0, |- 3 <= 4, |- 4 >= 1]), 5: OrderedSet([|- 5 >= 0, |- 4 <= 5, |- 5 >= 1]), 6: OrderedSet([|- 6 >= 0, |- 5 <= 6, |- 6 >= 1]), 7: OrderedSet([|- 7 >= 0, |- 6 <= 7, |- 7 >= 1]), 8: OrderedSet([|- 8 >= 0, |- 7 <= 8, |- 8 >= 1]), 9: OrderedSet([|- 9 >= 0, |- 8 <= 9, |- 9 >= 1]), _b: OrderedSet([{_b in Real, _a in Real, [not](_b < _a)} |- _a <= _b]), e: OrderedSet([|- e >= 0]), pi: OrderedSet([|- pi >= 0])}

Methods Documentation

add(self, relation, \*\*defaults_config)

From a <= b, derive and return a + c <= b + d given c <= d (and a, b, c, d are all Real). c and d are determined from the given ‘relation’.

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

add_left(self, addend, \*, strong=False, \*\*defaults_config)

From a <= b, derive and return a + c <= b given c <= 0 Or from a >= b, derive and return a + c >= b given 0 <= c (and a, b, c are all Real) where c is the given ‘addend’.

If ‘strong’ is True, we derive the strong < (>) form and c must be provably non-zero.

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

add_right(self, addend, \*, strong=False, \*\*defaults_config)

From a <= b, derive and return a <= b + c given 0 <= c Or from a >= b, derive and return a >= b + c given c <= 0 (and a, b, c are all Real) where c is the given ‘addend’.

If ‘strong’ is True, we derive the strong < (>) form and c must be provably non-zero.

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

apply_transitivity(self, other, \*\*defaults_config)

Apply a transitivity rule to derive from this x<=y expression and something of the form y<z, y<=z, z>y, z>=y, or y=z to obtain x<z or x<=z as appropriate. In the special case of x<=y and y<=x (or x>=y), derive x=z.

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

conclude_via_equality(self, \*\*defaults_config)

Conclude a ≤ b from a = b.

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

deduce_in_bool(self, \*\*defaults_config)

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

derive_negated(self, \*\*defaults_config)

From a <= b, derive and return -b <= -a.

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

derive_shifted(self, addend, addend_side='right', \*\*defaults_config)

From a <= b, derive and return a + c <= b + c where c is the given ‘addend’. Assumptions may be required to prove that a, b, and c are in Real.

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

divide_both_sides(self, divisor, \*\*defaults_config)

Divide both sides of the relation by the ‘divisor’.

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

exponentiate_both_sides(self, exponent, \*\*defaults_config)

Exponentiate both sides of the relation by the ‘exponent’.

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

left_add_both_sides(self, addend, \*\*defaults_config)

Add to both sides of the relation by the ‘addend’ on the left.

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

left_mult_both_sides(self, multiplier, \*\*defaults_config)

Multiply both sides of the relation by the ‘multiplier’ on the left.

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

remake_constructor(self)

Method to call to reconstruct this Expression. The default is the class name itself to use the __init__ method, but sometimes a different method is more appropriate for setting the proper style (e.g. the Frac method in proveit.numbers.division.divide which constructs a Div object with a different style). This constructor method must be in the same module as the class.

static reversed_operator_str(formatType)

Reversing ‘<=’ gives ‘>=’.

right_add_both_sides(self, addend, \*\*defaults_config)

Add to both sides of the relation by the ‘addend’ on the right.

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

right_mult_both_sides(self, multiplier, \*\*defaults_config)

Multiply both sides of the relation by the ‘multiplier’ on the right.

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

unfold(self, \*\*defaults_config)

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