Theorems (or conjectures) for the theory of proveit.logic.sets.comprehension

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import And, Implies, Forall, Equals, InSet, SetOfAll, Exists, SubsetEq
from proveit import f, n, x, y, S, Q, R, fx, Qx, Qy, Rx
from proveit.core_expr_types import (x_1_to_n, y_1_to_n, f__x_1_to_n, f__y_1_to_n, 
                                     Q__x_1_to_n, Q__y_1_to_n, R__x_1_to_n, R__y_1_to_n, S_1_to_n)
from proveit.logic.sets import basic_comprehension_y, general_comprehension_fyn
from proveit.numbers import NaturalPos

%begin theorems

Defining theorems for theory 'proveit.logic.sets.comprehension'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

# original, replaced below
# maintained here temporarily until replacement verified
# unfold = Forall((k, l), Forall((S, iter_q1k, f, x), 
#                                Implies(InSet(x, general_comprehension_fy),
#                                        Exists(yy, Equals(x, f_y_iter1l),
#                                               domain=Exp(S, l),
#                                               conditions=[iter_q1k_y_iter1l])).with_wrap_before_operator()),
#                 domains=(Natural, NaturalPos))

unfold = \
    Forall(n,
    Forall((S_1_to_n, Q, f, x),
        Implies(
            InSet(x, general_comprehension_fyn),
            Exists(y_1_to_n, Equals(x, f__y_1_to_n), domains=[S_1_to_n], conditions=[Q__y_1_to_n])
        ).with_wrap_before_operator()
    ),
    domain=NaturalPos
    )

unfold (established theorem):

# original, replaced below
# maintained here temporarily until replacement verified
# fold = Forall((k, l),
#               Forall((S, iter_q1k, f, x), 
#                      Implies(Exists(yy, Equals(x, f_y_iter1l),
#               domain=Exp(S, l),
#               conditions=[iter_q1k_y_iter1l]),
#               InSet(x, general_comprehension_fy)).with_wrap_after_operator()),
#        domains=(Natural, NaturalPos))

fold = \
    Forall(n,
    Forall((S_1_to_n, Q, f, x),
        Implies(
            Exists(y_1_to_n, Equals(x, f__y_1_to_n), domains=[S_1_to_n], conditions=[Q__y_1_to_n]),
            InSet(x, general_comprehension_fyn)
        ).with_wrap_before_operator()
    ),
    domain=NaturalPos
    )

fold (established theorem):

# original, replaced below
# maintained here temporarily until replacement verified
# basic_comprehension = Forall((k, l),
#     Forall((S, iter_q1k, x),
#            Equals(InSet(x, basic_comprehension_y),
#                   And(InSet(x, S), iter_q1k_x)).with_wrap_before_operator()),
# domains=(Natural, NaturalPos))

basic_comprehension = \
    Forall((S, Q, x),
        Equals(InSet(x, basic_comprehension_y),
               And(InSet(x, S), Qx))
    )

basic_comprehension (conjecture without proof):

# original, replaced below
# maintained here temporarily until replacement verified
# unfold_basic_comprehension = Forall(k, Forall((S, iter_q1k), 
#                                             Forall(x, And(InSet(x, S), iter_q1k_x),
#                                                    domain=basic_comprehension_y)),
#                                   domain=NaturalPos)

unfold_basic_comprehension = \
    Forall((S, Q), 
    Forall(x, And(InSet(x, S), Qx),
        domain=basic_comprehension_y)
    )

unfold_basic_comprehension (conjecture without proof):

# original, replaced below
# maintained here temporarily until replacement verified
# in_superset_if_in_comprehension = \
#     Forall(k,
#     Forall((S, iter_q1k), 
#     Forall(x, InSet(x, S), 
#         domain=basic_comprehension_y)),
#         domain=NaturalPos)

in_superset_if_in_comprehension = \
    Forall((S, Q), 
    Forall(x, InSet(x, S), 
        domain=basic_comprehension_y))

in_superset_if_in_comprehension (conjecture without proof):

# original, replaced below
# maintained here temporarily until replacement verified
# comprehension_is_subset = \
#     Forall(k,
#     Forall((S, iter_q1k), 
#         SubsetEq(basic_comprehension_y, S)),
#         domain=NaturalPos)

comprehension_is_subset = \
    Forall((S, Q), SubsetEq(basic_comprehension_y, S))

comprehension_is_subset (conjecture without proof):

subset_via_condition_constraint = \
    Forall(
    n, Forall((f, Q, R, S_1_to_n), 
              Implies(Forall(x_1_to_n, Q__x_1_to_n, domains=[S_1_to_n], condition=R__x_1_to_n),
                      SubsetEq(SetOfAll(x_1_to_n, f__x_1_to_n, domains=[S_1_to_n], condition=R__x_1_to_n), 
                               SetOfAll(y_1_to_n, f__y_1_to_n, domains=[S_1_to_n], condition=Q__y_1_to_n))
                      .with_wrap_after_operator())
              .with_wrap_after_operator()),
    domain=NaturalPos)

subset_via_condition_constraint (conjecture without proof):

# original, replaced below
# maintained here temporarily until replacement verified
# fold_basic_comprehension = \
#     Forall(k,
#     Forall((S, iter_q1k), 
#     Forall(x,
#         InSet(x, basic_comprehension_y),
#         domain=S, conditions=[iter_q1k_x])))

fold_basic_comprehension = \
    Forall((S, Q), 
    Forall(x,
        InSet(x, basic_comprehension_y),
        domain=S, conditions=[Qx]))

fold_basic_comprehension (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.sets.comprehension