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

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, Forall, Exists, Implies, in_bool, InSet, Equals, Not, NotInSet
from proveit.logic import SetEquiv, SetNotEquiv, SubsetEq, NotSubsetEq, superset_eq
from proveit.logic import ProperSubset, NotProperSubset
from proveit import A, B, C, x, y, P, Px, Py
%begin theorems

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

# Proven
unfold_subset_eq = Forall((A, B), Forall(x, InSet(x, B), domain=A), conditions=SubsetEq(A, B))

unfold_subset_eq (established theorem):

unfold_subset_eq_contrapositive = Forall((A, B), Forall(x, NotInSet(x, A), conditions=NotInSet(x, B)), conditions=SubsetEq(A, B))

unfold_subset_eq_contrapositive (conjecture without proof):

# Proven
fold_subset_eq = Forall((A, B), SubsetEq(A, B), condition=Forall(x, InSet(x, B), domain=A))

fold_subset_eq (established theorem):

# Proven
unfold_not_subset_eq = Forall((A, B), Not(SubsetEq(A, B)), conditions=[NotSubsetEq(A, B)])

unfold_not_subset_eq (established theorem):

# Proven
fold_not_subset_eq = Forall((A, B), NotSubsetEq(A, B), conditions=[Not(SubsetEq(A, B))])

fold_not_subset_eq (established theorem):

refined_nonmembership = Forall((A, B, x), NotInSet(x, A), 
                              conditions=[SubsetEq(A, B),
                                         NotInSet(x, B)])

refined_nonmembership (conjecture without proof):

# Proven
unfold_proper_subset = Forall((A, B), And(SubsetEq(A, B), SetNotEquiv(B, A)), conditions=[ProperSubset(A, B)])

unfold_proper_subset (established theorem):

# Proven
fold_proper_subset = Forall((A, B), ProperSubset(A, B), conditions=[And(SubsetEq(A, B), SetNotEquiv(B, A))])

fold_proper_subset (established theorem):

# Proven
unfold_not_proper_subset = Forall((A, B), Not(ProperSubset(A, B)), condition=NotProperSubset(A, B))

unfold_not_proper_subset (established theorem):

# Proven
fold_not_proper_subset = Forall((A, B), NotProperSubset(A, B), condition=Not(ProperSubset(A, B)))

fold_not_proper_subset (established theorem):

superset_membership_from_proper_subset = Forall((A, B), Forall(x, InSet(x, B), domain=A),
                                      condition=ProperSubset(A, B))

superset_membership_from_proper_subset (established theorem):

# Proven
subset_eq_reflexive = Forall(A, SubsetEq(A, A))

subset_eq_reflexive (established theorem):

# Proven
relax_proper_subset = Forall((A, B), SubsetEq(A, B), conditions=[ProperSubset(A, B)])

relax_proper_subset (established theorem):

subset_eq_via_equivalence = Forall((A, B), SubsetEq(A, B), conditions=[SetEquiv(A, B)])

subset_eq_via_equivalence (conjecture without proof):

subset_eq_via_equality = Forall((A, B), SubsetEq(A, B), conditions=[Equals(A, B)])

subset_eq_via_equality (established theorem):

Transitivity Theorems

# working
transitivity_subset_subset = Forall((A, B, C), ProperSubset(A, C), conditions=[ProperSubset(A, B), ProperSubset(B, C)])

transitivity_subset_subset (conjecture without proof):

transitivity_subset_eq_subset = Forall((A, B, C), ProperSubset(A, C), conditions=[SubsetEq(A, B), ProperSubset(B, C)])

transitivity_subset_eq_subset (conjecture without proof):

transitivity_subset_subset_eq = Forall((A, B, C), ProperSubset(A, C), conditions=[ProperSubset(A, B), SubsetEq(B, C)])

transitivity_subset_subset_eq (conjecture without proof):

# Proven
transitivity_subset_eq_subset_eq = Forall((A, B, C), SubsetEq(A, C), conditions=[SubsetEq(A, B), SubsetEq(B, C)])

transitivity_subset_eq_subset_eq (established theorem):

Misc Identities.

inclusive_universal_quantification = Forall(
    (A, B, P), Implies(Forall(x, Px, domain=A),
                       Forall(y, Py, domain=B)),
    condition = superset_eq(A, B))

inclusive_universal_quantification (conjecture without proof):

inclusive_existential_quantification = Forall(
    (A, B, P), Implies(Exists(x, Px, domain=A), 
                       Exists(y, Py, domain=B)),
    condition = SubsetEq(A, B))

inclusive_existential_quantification (conjecture without proof):

Theorems establishing containment claims as being Boolean (i.e. T or F).

subset_eq_is_bool = Forall((A, B), in_bool(SubsetEq(A, B)))

subset_eq_is_bool (conjecture without proof):

not_subset_eq_is_bool = Forall((A, B), in_bool(NotSubsetEq(A, B)))

not_subset_eq_is_bool (conjecture without proof):

proper_subset_is_bool = Forall((A, B), in_bool(ProperSubset(A, B)))

proper_subset_is_bool (conjecture without proof):

not_proper_subset_is_bool = Forall((A, B), in_bool(NotProperSubset(A, B)))

not_proper_subset_is_bool (conjecture without proof):

%end theorems

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