# Axioms for the theory of proveit.logic.sets.disjointness¶

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.logic import Forall, Iff, Equals, And, Distinct, Disjoint, Intersect, EmptySet, NotInSet, Set
from proveit import m, n, y, A, B, X
from proveit.core_expr_types import A_1_to_m, x_1_to_n
from proveit.logic.sets import x_singletons_range
from proveit.numbers import Natural, NaturalPos
%begin axioms

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


An empty collection of sets are mutually disjoint simply because there are no pairs:

In [2]:
vacuously_disjoint = Disjoint()

vacuously_disjoint:

Define disjoint for a pair of sets to mean that the intersection of the pair is the empty set:

In [3]:
disjoint_pair_def = Forall((A, B), Iff(Disjoint(A, B), Equals(Intersect(A, B), EmptySet)))

disjoint_pair_def:

Define disjoint (mutually disjoint) through induction: adding a set to a disjoint collection will maintain disjointness if and only if the new set is disjoint with all of the sets in the original collection:

In [4]:
disjoint_induction = Forall(m, Forall((A_1_to_m, B),
Iff(Disjoint(A_1_to_m, B),
And(Disjoint(A_1_to_m),
Forall(X, Disjoint(X, B),
domain=Set(A_1_to_m)))).with_wrap_after_operator()),
domain=Natural)

disjoint_induction:

Elements being distinct is the same as their associated singletons being disjoint:

In [5]:
distinct_def = Forall(n, Forall(x_1_to_n,
Equals(Distinct(x_1_to_n),
Disjoint(x_singletons_range))),
domain=NaturalPos)

distinct_def:
In [6]:
%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.disjointness