logo

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

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 import x, A, B, C, P, S, PofA, PofB
from proveit.logic import FALSE, Forall, Equals, in_bool, InSet, Not
from proveit.logic.sets import SubsetEq
from proveit.logic.sets import Set, SetEquiv, SetNotEquiv, Union
In [2]:
%begin theorems
Defining theorems for theory 'proveit.logic.sets.equivalence'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
set_equiv_unfold = Forall(
    (A, B), Forall(x, Equals(InSet(x, A), InSet(x, B))),
    condition=SetEquiv(A, B))
set_equiv_unfold (established theorem):

In [4]:
set_equiv_fold = Forall(
    (A, B), SetEquiv(A, B),
    condition=Forall(x, Equals(InSet(x, A), InSet(x, B))))
set_equiv_fold (established theorem):

In [5]:
left_membership_via_right = Forall(
    (A, B), Forall(x, InSet(x, A), domain=B), condition=SetEquiv(A, B))
left_membership_via_right (conjecture without proof):

In [6]:
right_membership_via_left = Forall(
    (A, B), Forall(x, InSet(x, B), domain=A), condition=SetEquiv(A, B))
right_membership_via_left (conjecture without proof):

In [7]:
set_equiv_reflexivity = Forall(A, SetEquiv(A, A))
set_equiv_reflexivity (established theorem):

In [8]:
set_equiv_reflection = Forall((A, B), SetEquiv(A, B), condition=Equals(A, B))
set_equiv_reflection (conjecture without proof):

In [9]:
set_equiv_symmetry = Forall((A, B), Equals(SetEquiv(B, A), SetEquiv(A, B)))
set_equiv_symmetry (conjecture without proof):

In [10]:
set_equiv_reversal = Forall((A, B), SetEquiv(B, A), conditions=[SetEquiv(A, B)])
set_equiv_reversal (established theorem):

In [11]:
set_equiv_transitivity = Forall((A, B, C), SetEquiv(A, C), conditions=[SetEquiv(A, B), SetEquiv(B, C)])
set_equiv_transitivity (conjecture without proof):

In [12]:
set_equiv_is_bool = Forall((A, B), in_bool(SetEquiv(A, B)))
set_equiv_is_bool (conjecture with conjecture-based proof):

In [13]:
set_not_equiv_reversal = Forall((A, B), SetNotEquiv(B, A), conditions=[SetNotEquiv(A, B)])
set_not_equiv_reversal (conjecture with conjecture-based proof):

In [14]:
set_not_equiv_is_bool = Forall((A, B), in_bool(SetNotEquiv(A, B)))
set_not_equiv_is_bool (conjecture with conjecture-based proof):

Folding and unfolding the definition of $\ncong$

In [15]:
# Proven
unfold_set_not_equiv = Forall((A, B), Not(SetEquiv(A, B)), conditions=[SetNotEquiv(A, B)])
unfold_set_not_equiv (established theorem):

In [16]:
# Proven
fold_set_not_equiv = Forall((A, B), SetNotEquiv(A, B), conditions=[Not(SetEquiv(A, B))])
fold_set_not_equiv (established theorem):

Substitution With An Equivalent Set

In [17]:
# Not clear what to do here — ambiguous what the resulting forms of
# fof_a and fof_b are — could be sets, could be something else …
# substitution = Forall((f, A, B), SetEquiv(fof_a, fof_b), conditions=SetEquiv(x, y))
In [18]:
sub_left_side_into = Forall((P, A, B), PofA, conditions=[PofB, SetEquiv(A, B)])
sub_left_side_into (conjecture without proof):

In [19]:
sub_right_side_into = Forall((P, A, B), PofB, conditions=[PofA, SetEquiv(A, B)])
sub_right_side_into (conjecture without proof):

Contradictions

If two sets are both equivalent and not equivalent, there is a contradiction:

In [20]:
# Proven
set_not_equiv_contradiction = Forall((A, B), FALSE, conditions=[SetEquiv(A, B), SetNotEquiv(A, B)]) 
set_not_equiv_contradiction (established theorem):

In [21]:
union_with_elem_redundancy = Forall((x, S), SetEquiv(Union(S, Set(x)), S), conditions=[InSet(x, S)])
union_with_elem_redundancy (conjecture without proof):

In [22]:
union_with_subset_redundancy = Forall((S, A),
                          SetEquiv(Union(S, A), S),
                          conditions=[SubsetEq(A, S)])
union_with_subset_redundancy (conjecture without proof):

In [23]:
%end theorems
These theorems may now be imported from the theory package: proveit.logic.sets.equivalence