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

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

%begin theorems

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

set_equiv_unfold = Forall(
    (A, B), Forall(x, Equals(InSet(x, A), InSet(x, B))),
    condition=SetEquiv(A, B))

set_equiv_unfold (established theorem):

set_equiv_fold = Forall(
    (A, B), SetEquiv(A, B),
    condition=Forall(x, Equals(InSet(x, A), InSet(x, B))))

set_equiv_fold (established theorem):

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):

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):

set_equiv_reflexivity = Forall(A, SetEquiv(A, A))

set_equiv_reflexivity (established theorem):

set_equiv_reflection = Forall((A, B), SetEquiv(A, B), condition=Equals(A, B))

set_equiv_reflection (conjecture without proof):

set_equiv_symmetry = Forall((A, B), Equals(SetEquiv(B, A), SetEquiv(A, B)))

set_equiv_symmetry (conjecture without proof):

set_equiv_reversal = Forall((A, B), SetEquiv(B, A), conditions=[SetEquiv(A, B)])

set_equiv_reversal (established theorem):

set_equiv_transitivity = Forall((A, B, C), SetEquiv(A, C), conditions=[SetEquiv(A, B), SetEquiv(B, C)])

set_equiv_transitivity (conjecture without proof):

set_equiv_is_bool = Forall((A, B), in_bool(SetEquiv(A, B)))

set_equiv_is_bool (conjecture with conjecture-based proof):

set_not_equiv_reversal = Forall((A, B), SetNotEquiv(B, A), conditions=[SetNotEquiv(A, B)])

set_not_equiv_reversal (conjecture with conjecture-based proof):

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$

# Proven
unfold_set_not_equiv = Forall((A, B), Not(SetEquiv(A, B)), conditions=[SetNotEquiv(A, B)])

unfold_set_not_equiv (established theorem):

# 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

# 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))

sub_left_side_into = Forall((P, A, B), PofA, conditions=[PofB, SetEquiv(A, B)])

sub_left_side_into (conjecture without proof):

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:

# Proven
set_not_equiv_contradiction = Forall((A, B), FALSE, conditions=[SetEquiv(A, B), SetNotEquiv(A, B)]) 

set_not_equiv_contradiction (established theorem):

Misc Related Theorems

union_with_elem_redundancy = Forall((x, S), SetEquiv(Union(S, Set(x)), S), conditions=[InSet(x, S)])

union_with_elem_redundancy (conjecture without proof):

union_with_subset_redundancy = Forall((S, A),
                          SetEquiv(Union(S, A), S),
                          conditions=[SubsetEq(A, S)])

union_with_subset_redundancy (conjecture without proof):

%end theorems

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