Less

class proveit.numbers.Less(lhs, rhs, *, 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 or 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.
conclude(self, \*\*defaults_config)	Conclude something of the form a < b.
deduce_in_bool(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
derive_relaxed(self, \*\*defaults_config)	Relax a < b to a <= b, deducing the latter from the former (self) and returning the latter.
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.

Attributes Documentation

known_left_sides = {0: OrderedSet([|- 0 < 1, {_a in NaturalPos} |- 0 < _a, {n in NaturalPos} |- n > 0, {_a in RationalPos} |- 0 < _a, {q in RationalPos} |- q > 0, {_a in RealPos} |- 0 < _a, {x in RealPos} |- 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]), x: OrderedSet([{x < y} |- x < y]), a: OrderedSet([{a < b} |- a < b]), _a: OrderedSet([{_b in Real, _a in Real, [not](_b <= _a)} |- _a < _b]), y: OrderedSet([{x in Real, y in Real, [not](x <= y)} |- y < x]), 1: OrderedSet([|- 1 < 2]), 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 = {1: OrderedSet([|- 0 < 1]), _a: OrderedSet([{_b < _a} |- _b < _a, {_a in NaturalPos} |- 0 < _a, {_a in RationalPos} |- 0 < _a, {_a in RealPos} |- 0 < _a]), y: OrderedSet([{x < y} |- x < y]), b: OrderedSet([{a < b} |- a < b]), _b: OrderedSet([{_b in Real, _a in Real, [not](_b <= _a)} |- _a < _b]), x: OrderedSet([{x in Real, y in Real, [not](x <= y)} |- y < x, {x in RealPos} |- x > 0]), 2: OrderedSet([|- 1 < 2, |- 2 > 0]), 3: OrderedSet([|- 2 < 3, |- 3 > 0]), 4: OrderedSet([|- 3 < 4, |- 4 > 0]), 5: OrderedSet([|- 4 < 5, |- 5 > 0]), 6: OrderedSet([|- 5 < 6, |- 6 > 0]), 7: OrderedSet([|- 6 < 7, |- 7 > 0]), 8: OrderedSet([|- 7 < 8, |- 8 > 0]), 9: OrderedSet([|- 8 < 9, |- 9 > 0]), n: OrderedSet([{n in NaturalPos} |- n > 0]), q: OrderedSet([{q in RationalPos} |- q > 0]), 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 or 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=True, \*\*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 False, we derive the weak ≤ (≥) form (same as if we use the derive_relaxed method on the result).

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

add_right(self, addend, \*, strong=True, \*\*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 False, we derive the weak ≤ (≥) form (same as if we use the derive_relaxed method on the result).

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.

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

conclude(self, \*\*defaults_config)

Conclude something of the form 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_relaxed(self, \*\*defaults_config)

Relax a < b to a <= b, deducing the latter from the former (self) and returning the latter. Assumptions may be required to deduce that a and b are in Real.

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.