Common expressions for the theory of proveit.logic.sets

import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import Lambda, ExprRange, IndexedVar
from proveit import i, l, m, n, x, y, A, S, fy, Qy
from proveit.core_expr_types import y_1_to_n, f__y_1_to_n, Q__y_1_to_n, S_1_to_n, R__y_1_to_n
from proveit.logic import (And, Or, Equals, NotEquals, Set, InSet, NotInSet, SubsetEq,
                           SetOfAll, UnionAll, IntersectAll)
from proveit.numbers import one
from proveit.logic.sets.empty_set import EmptySetLiteral
%begin common

Defining common sub-expressions for theory 'proveit.logic.sets'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

EmptySet = EmptySetLiteral()

EmptySet:

each_x_in_S = ExprRange(i, InSet(IndexedVar(x, i), S), one, n)

each_x_in_S:

x_equals_any_y = Or(ExprRange(i, Equals(x, IndexedVar(y, i)), one, n))

x_equals_any_y:

x_notequals_all_y = And(ExprRange(i, NotEquals(x, IndexedVar(y, i)), one, n))

x_notequals_all_y:

x_in_any_A = Or(ExprRange(i, InSet(x, IndexedVar(A, i)), one, m))

x_in_any_A:

x_notin_all_A = And(ExprRange(i, NotInSet(x, IndexedVar(A, i)), one, m))

x_notin_all_A:

x_in_every_A = And(ExprRange(i, InSet(x, IndexedVar(A, i)), one, m))

x_in_every_A:

x_notin_some_A = Or(ExprRange(i, NotInSet(x, IndexedVar(A, i)), one, m))

x_notin_some_A:

x_singletons_range = ExprRange(i, Set(IndexedVar(x, i)), one, n)

x_singletons_range:

each_A_in_S = And(ExprRange(i, SubsetEq(IndexedVar(A, i), S), one, m))

each_A_in_S:

general_comprehension_fy = SetOfAll(y, fy, S, conditions=[Qy])

general_comprehension_fy:

general_comprehension_fyn = SetOfAll(y_1_to_n, f__y_1_to_n, domains=[S_1_to_n], 
                                     conditions=[Q__y_1_to_n])

general_comprehension_fyn:

basic_comprehension_y = SetOfAll(y, y, S, conditions=[Qy])

basic_comprehension_y:

general_unionall_Ryn = UnionAll(y_1_to_n, R__y_1_to_n, domains=[S_1_to_n], 
                                conditions=[Q__y_1_to_n])

general_unionall_Ryn:

general_intersectall_Ryn = IntersectAll(y_1_to_n, R__y_1_to_n, domains=[S_1_to_n], 
                                        conditions=[Q__y_1_to_n])

general_intersectall_Ryn:

%end common

These common expressions may now be imported from the theory package: proveit.logic.sets