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

In [1]:
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

In [2]:
# Proven
unfold_subset_eq = Forall((A, B), Forall(x, InSet(x, B), domain=A), conditions=SubsetEq(A, B))

unfold_subset_eq (established theorem):

In [3]:
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):

In [4]:
# Proven
fold_subset_eq = Forall((A, B), SubsetEq(A, B), condition=Forall(x, InSet(x, B), domain=A))

fold_subset_eq (established theorem):

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

unfold_not_subset_eq (established theorem):

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

fold_not_subset_eq (established theorem):

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

refined_nonmembership (conjecture without proof):

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

unfold_proper_subset (established theorem):

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

fold_proper_subset (established theorem):

In [10]:
# Proven
unfold_not_proper_subset = Forall((A, B), Not(ProperSubset(A, B)), condition=NotProperSubset(A, B))

unfold_not_proper_subset (established theorem):

In [11]:
# Proven
fold_not_proper_subset = Forall((A, B), NotProperSubset(A, B), condition=Not(ProperSubset(A, B)))

fold_not_proper_subset (established theorem):

In [12]:
superset_membership_from_proper_subset = Forall((A, B), Forall(x, InSet(x, B), domain=A),
condition=ProperSubset(A, B))

In [13]:
# Proven
subset_eq_reflexive = Forall(A, SubsetEq(A, A))

subset_eq_reflexive (established theorem):

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

relax_proper_subset (established theorem):

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

subset_eq_via_equivalence (conjecture without proof):

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

subset_eq_via_equality (established theorem):

### Transitivity Theorems¶

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

transitivity_subset_subset (conjecture without proof):

In [18]:
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):

In [19]:
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):

In [20]:
# 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.¶

In [21]:
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):

In [22]:
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).¶

In [23]:
subset_eq_is_bool = Forall((A, B), in_bool(SubsetEq(A, B)))

subset_eq_is_bool (conjecture without proof):

In [24]:
not_subset_eq_is_bool = Forall((A, B), in_bool(NotSubsetEq(A, B)))

not_subset_eq_is_bool (conjecture without proof):

In [25]:
proper_subset_is_bool = Forall((A, B), in_bool(ProperSubset(A, B)))

proper_subset_is_bool (conjecture without proof):

In [26]:
not_proper_subset_is_bool = Forall((A, B), in_bool(NotProperSubset(A, B)))

not_proper_subset_is_bool (conjecture without proof):

In [27]:
%end theorems

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