# Axioms for the theory of proveit.logic.sets.cartesian_products¶

In [1]:
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

In [2]:
%begin axioms

Defining axioms for theory 'proveit.logic.sets.cartesian_products'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


A Cartesian product set is the set of tuples whose elements are contained in the respective sets of the product.

In [3]:
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)

Out[3]:
cart_prod_def:

A Cartesian exponentiation is the set defined by the Cartesian product of the base repeated the number of times indicated by the exponent.

In [4]:
cart_exp_def = Forall(
m, Forall(S,
Equals(CartExp(S, m),
CartProd(ExprRange(k, S, one, m)))),
domain=NaturalPos)

Out[4]:
cart_exp_def:
In [5]:
%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.cartesian_products