 # Common expressions for context proveit.logic.set_theory¶

In :
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 :
EmptySet = EmptySetLiteral()

In :
each_x_in_S = Iter(i, InSet(Indexed(xx, i), S), one, n)

In :
x_equals_any_y = Or(Iter(i, Equals(x, Indexed(yy, i)), one, l))

Out:
In :
x_notequals_all_y = And(Iter(i, NotEquals(x, Indexed(yy, i)), one, l))

Out:
In :
x_in_any_A = Or(Iter(i, InSet(x, Indexed(AA, i)), one, m))

In :
x_notin_all_A = And(Iter(i, NotInSet(x, Indexed(AA, i)), one, m))

In :
x_in_every_A = And(Iter(i, InSet(x, Indexed(AA, i)), one, m))

In :
x_notin_some_A = Or(Iter(i, NotInSet(x, Indexed(AA, i)), one, m))

Out:
In :
iter_x_singletons = Iter(i, Set(Indexed(xx, i)), one, l)

Out:
In :
generalComprehension_fy = SetOfAll(y, fy, S, conditions=[iterQ1k_y])

In :
basicComprehension_y = SetOfAll(y, y, S, conditions=[iterQ1k_y])

Out:
In :
%end common

Common expressions may be imported from autogenerated _common_.py