import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprTuple, ExprRange
from proveit import k, m, x, S
from proveit.core_expr_types import a_1_to_m, A_1_to_m
from proveit.logic import And, Forall, InSet, Equals, CartProd, CartExp
from proveit.logic.sets.cartesian_products import a_in_A__1_to_m
from proveit.numbers import NaturalPos, one
%begin axioms
A Cartesian product set is the set of tuples whose elements are contained in the respective sets of the product.
cart_prod_def = Forall(
m, Forall((x, A_1_to_m, a_1_to_m),
Equals(InSet(x, CartProd(A_1_to_m)),
And(Equals(x, ExprTuple(a_1_to_m)),
a_in_A__1_to_m)).with_wrap_after_operator()),
domain=NaturalPos)
A Cartesian exponentiation is the set defined by the Cartesian product of the base repeated the number of times indicated by the exponent.
cart_exp_def = Forall(
m, Forall(S,
Equals(CartExp(S, m),
CartProd(ExprRange(k, S, one, m)))),
domain=NaturalPos)
%end axioms