Axioms for the theory of proveit.numbers.functions

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 Conditional, ConditionalSet
from proveit import i, j
from proveit.logic import Forall, Equals, NotEquals
from proveit.numbers import zero, one, KroneckerDelta

%begin axioms

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

# This general definition does not require i and j to be numbers.  This is deliberate.
kron_delta_def = Forall((i, j), Equals(
    KroneckerDelta(i, j), ConditionalSet(
        Conditional(one, Equals(i, j)),
        Conditional(zero, NotEquals(i, j)))))

kron_delta_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.functions