logo

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