logo

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)
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)
cart_exp_def:
In [5]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.sets.cartesian_products