logo

Common expressions for context proveit.logic.set_theory

In [1]:
import proveit
from proveit import Lambda, Iter, Indexed
from proveit._common_ import i, l, m, n, x, y, xx, yy, S, AA, fy
from proveit.logic import And, Or, Equals, NotEquals, Set, InSet, NotInSet, SetOfAll
from proveit.logic._common_ import yIter1l, f_yIter1l, iterA1m, iterQ1k_y
from proveit.number import one
from empty_set import EmptySetLiteral
%begin common
Defining common sub-expressions for context 'proveit.logic.set_theory'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [2]:
EmptySet = EmptySetLiteral()
Out[2]:
EmptySet:
In [3]:
each_x_in_S = Iter(i, InSet(Indexed(xx, i), S), one, n)
Out[3]:
each_x_in_S:
In [4]:
x_equals_any_y = Or(Iter(i, Equals(x, Indexed(yy, i)), one, l))
Out[4]:
x_equals_any_y:
In [5]:
x_notequals_all_y = And(Iter(i, NotEquals(x, Indexed(yy, i)), one, l))
Out[5]:
x_notequals_all_y:
In [6]:
x_in_any_A = Or(Iter(i, InSet(x, Indexed(AA, i)), one, m))
Out[6]:
x_in_any_A:
In [7]:
x_notin_all_A = And(Iter(i, NotInSet(x, Indexed(AA, i)), one, m))
Out[7]:
x_notin_all_A:
In [8]:
x_in_every_A = And(Iter(i, InSet(x, Indexed(AA, i)), one, m))
Out[8]:
x_in_every_A:
In [9]:
x_notin_some_A = Or(Iter(i, NotInSet(x, Indexed(AA, i)), one, m))
Out[9]:
x_notin_some_A:
In [10]:
iter_x_singletons = Iter(i, Set(Indexed(xx, i)), one, l)
Out[10]:
iter_x_singletons:
In [11]:
generalComprehension_fy = SetOfAll(y, fy, S, conditions=[iterQ1k_y])
Out[11]:
generalComprehension_fy:
In [12]:
basicComprehension_y = SetOfAll(y, y, S, conditions=[iterQ1k_y])
Out[12]:
basicComprehension_y:
In [13]:
%end common
Common expressions may be imported from autogenerated _common_.py