logo
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 a, b, q
from proveit.logic import Equals, InSet, NotEquals, SetOfAll
from proveit.numbers import Integer, frac, zero, Natural, NaturalPos
from proveit.numbers import Rational, RationalPos, RationalNeg, RationalNonNeg
from proveit.numbers import greater, greater_eq, Less
from proveit import x, a, b
from proveit.logic import Forall, InSet, Exists, Equals, NotEquals, Iff
from proveit.numbers import Integer, Real, frac, zero, NaturalPos
from proveit.numbers.number_sets.rational_numbers import Rational, RationalPos
In [2]:
%begin axioms
Defining axioms for theory 'proveit.numbers.number_sets.rational_numbers'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [3]:
rationals_def = Equals(
        Rational,
        SetOfAll([a, b],
                 frac(a, b),
                 conditions=[NotEquals(b, zero)],
                 domain=Integer
        ))
rationals_def:
In [4]:
rationals_pos_def = Equals(RationalPos,
                         SetOfAll(q, q, conditions=[greater(q, zero)],
                                  domain=Rational))
rationals_pos_def:
In [5]:
rationals_neg_def = Equals(RationalNeg,
                         SetOfAll(q, q, conditions=[Less(q, zero)],
                                  domain=Rational))
rationals_neg_def:
In [6]:
rationals_non_neg_def = Equals(RationalNonNeg,
                            SetOfAll(q, q, conditions=[greater_eq(q, zero)],
                                     domain=Rational))
rationals_non_neg_def:
In [7]:
%end axioms
These axioms may now be imported from the theory package: proveit.numbers.number_sets.rational_numbers