logo

Theorems (or conjectures) for the theory of proveit.logic.sets.cartesian_products

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.

from proveit import ExprRange, ExprTuple, IndexedVar
from proveit import k, m, x, y, A, B, S
from proveit.core_expr_types import x_1_to_m
from proveit.logic import (in_bool, And, Forall, Equals,
                           InSet, ProperSubset, SubsetEq, CartExp, CartProd)
from proveit.numbers import NaturalPos, one
In [2]:
%begin theorems
Defining theorems for theory 'proveit.logic.sets.cartesian_products'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
cart_exp_abstract_membership_def = Forall(
    m, Forall((x, S), 
              Equals(InSet(x, CartExp(S, m)),
                     InSet(x, CartProd(ExprRange(k, S, one, m))))),
    domain=NaturalPos)
Out[3]:
cart_exp_abstract_membership_def (conjecture without proof):

In [4]:
cart_exp_explicit_membership_def = Forall(
    m, Forall((x_1_to_m, S), 
              Equals(InSet(ExprTuple(x_1_to_m), CartExp(S, m)),
                     And(ExprRange(k, InSet(IndexedVar(x, k), S),
                                   one, m)))),
    domain=NaturalPos)
Out[4]:
cart_exp_explicit_membership_def (conjecture without proof):

In [5]:
cart_exp_unfold_abstract = Forall(
    m, Forall((x, S), 
              InSet(x, CartProd(ExprRange(k, S, one, m))),
              condition=InSet(x, CartExp(S, m))),
    domain=NaturalPos)
The history saving thread hit an unexpected error (OperationalError('database is locked')).History will not be written to the database.
Out[5]:
cart_exp_unfold_abstract (conjecture without proof):

In [6]:
cart_exp_unfold_explicit = Forall(
    m, Forall((x_1_to_m, S), 
              And(ExprRange(k, InSet(IndexedVar(x, k), S), one, m)),
              condition=InSet(ExprTuple(x_1_to_m), CartExp(S, m))),
    domain=NaturalPos)
Out[6]:
cart_exp_unfold_explicit (conjecture without proof):

In [7]:
cart_exp_fold_abstract = Forall(
    m, Forall((x, S), 
              InSet(x, CartExp(S, m)),
              condition=InSet(x, CartProd(ExprRange(k, S, one, m)))),
    domain=NaturalPos)
Out[7]:
cart_exp_fold_abstract (conjecture without proof):

In [8]:
cart_exp_fold_explicit = Forall(
    m, Forall((x_1_to_m, S), 
              InSet(ExprTuple(x_1_to_m), CartExp(S, m)),
              conditions=ExprRange(k, InSet(IndexedVar(x, k), S), one, m)),
    domain=NaturalPos)
Out[8]:
cart_exp_fold_explicit (conjecture without proof):

In [9]:
in_cart_exp_is_bool = Forall(
    m, Forall((x, S), 
              in_bool(InSet(x, CartExp(S, m))),
              condition=Forall(y, in_bool(InSet(y, S)))),
    domain=NaturalPos)
Out[9]:
in_cart_exp_is_bool (conjecture without proof):

In [10]:
cart_exp_proper_subset = Forall(
    m, Forall((A, B), ProperSubset(CartExp(A, m), CartExp(B, m)),
              condition=ProperSubset(A, B)),
    domain=NaturalPos)
Out[10]:
cart_exp_proper_subset (conjecture without proof):

In [11]:
cart_exp_subset_eq = Forall(
    m, Forall((A, B), SubsetEq(CartExp(A, m), CartExp(B, m)),
              condition=SubsetEq(A, B)),
    domain=NaturalPos)
Out[11]:
cart_exp_subset_eq (conjecture without proof):

In [12]:
%end theorems
These theorems may now be imported from the theory package: proveit.logic.sets.cartesian_products