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()
x_in_R3_def: ⊢ 
In [3]:
x_in_R3_def.lhs.unfold(assumptions=[x_in_R3_def.lhs])
In [4]:
x_in_R3_def.lhs.fold(assumptions=[x_in_R3_def.rhs])
In [5]:
x_in_R3_def.lhs.prove(assumptions=[x_in_R3_def.rhs])
In [6]:
in_bool(x_in_R3_def.lhs).prove()
CartExp membership proofs with an 'explicit' element¶
In [7]:
abc = ExprTuple(a, b, c)
abc: 
In [8]:
abc_in_R3_def = InSet(abc, CartExp(Real, three)).definition()
abc_in_R3_def: ⊢ 
In [9]:
abc_in_R3_def.lhs.unfold(assumptions=[abc_in_R3_def.lhs])
In [10]:
abc_in_R3_def.lhs.fold(assumptions=[abc_in_R3_def.rhs])
In [11]:
abc_in_R3_def.lhs.prove(assumptions=[abc_in_R3_def.rhs])
In [12]:
in_bool(abc_in_R3_def.lhs).prove()
In [13]:
%end demonstrations