Axioms for the theory of proveit.logic.sets.equivalence

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import x, A, B, X
from proveit.logic import And, Equals, Forall, in_bool, Not, InSet
from proveit.logic.sets import SubsetEq, SetEquiv, SetNotEquiv
In [2]:
%begin axioms
Defining axioms for theory 'proveit.logic.sets.equivalence'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

**By definition, two sets are equivalent if they contain the same elements.

In [3]:
set_equiv_def = Forall((A, B), Equals(SetEquiv(A, B), Forall(x, Equals(InSet(x, A), InSet(x, B)))))

Define $A \ncong B$ as $\lnot (A \cong B)$:

In [4]:
set_not_equiv_def = Forall((A, B), Equals(SetNotEquiv(A, B), Not(SetEquiv(A, B))))
In [5]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.sets.equivalence