CartExp

class proveit.logic.CartExp(base, exponent, *, styles=None)

Bases: proveit.Operation

CartExp represents an exponentiation of a set by a positive, natural number to denote repeated Cartesion products.

Methods Summary

deduce_subset_eq_relation(self, subset, …)	Prove that this CartExp is a SubsetEq of ‘subset’ if the ‘subset’ is also a CartExp with the same exponent, and the base of self is a SubsetEq of the base of ‘subset’.
formatted(self, format_type, \*\*kwargs)	Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’).
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
membership_object(self, element)
string(self, \*\*kwargs)	Return a string representation of the Expression.

Methods Documentation

deduce_subset_eq_relation(self, subset, \*\*defaults_config)

Prove that this CartExp is a SubsetEq of ‘subset’ if the ‘subset’ is also a CartExp with the same exponent, and the base of self is a SubsetEq of the base of ‘subset’.

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

formatted(self, format_type, \*\*kwargs)

Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’). In the keyword arguments, fence=True indicates that parenthesis around the sub-expression may be necessary to avoid ambiguity.

latex(self, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

membership_object(self, element)

string(self, \*\*kwargs)

Return a string representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).