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