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

In [1]:
import proveit
from proveit import ExprTuple
from proveit import a, b, c, x
from proveit.logic import in_bool, InSet, CartExp
from proveit.numbers import Real, three
%begin demonstrations


### CartExp membership proofs with an 'abstract' element¶

In [2]:
x_in_R3_def = InSet(x, CartExp(Real, three)).definition()

Out[2]:
x_in_R3_def:
In [3]:
x_in_R3_def.lhs.unfold(assumptions=[x_in_R3_def.lhs])

Out[3]:
In [4]:
x_in_R3_def.lhs.fold(assumptions=[x_in_R3_def.rhs])

Out[4]:
In [5]:
x_in_R3_def.lhs.prove(assumptions=[x_in_R3_def.rhs])

Out[5]:
In [6]:
in_bool(x_in_R3_def.lhs).prove()

Out[6]:

### CartExp membership proofs with an 'explicit' element¶

In [7]:
abc = ExprTuple(a, b, c)

Out[7]:
abc:
In [8]:
abc_in_R3_def = InSet(abc, CartExp(Real, three)).definition()

Out[8]:
abc_in_R3_def:
In [9]:
abc_in_R3_def.lhs.unfold(assumptions=[abc_in_R3_def.lhs])

Out[9]:
In [10]:
abc_in_R3_def.lhs.fold(assumptions=[abc_in_R3_def.rhs])

Out[10]:
In [11]:
abc_in_R3_def.lhs.prove(assumptions=[abc_in_R3_def.rhs])

Out[11]:
In [12]:
in_bool(abc_in_R3_def.lhs).prove()

Out[12]:
In [13]:
%end demonstrations