Axioms for the theory of proveit.numbers.number_sets.rational_numbers

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

%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

rationals_def = Equals(
        Rational,
        SetOfAll([a, b],
                 frac(a, b),
                 conditions=[NotEquals(b, zero)],
                 domain=Integer
        ))

rationals_def:

rationals_pos_def = Equals(RationalPos,
                         SetOfAll(q, q, conditions=[greater(q, zero)],
                                  domain=Rational))

rationals_pos_def:

rationals_neg_def = Equals(RationalNeg,
                         SetOfAll(q, q, conditions=[Less(q, zero)],
                                  domain=Rational))

rationals_neg_def:

rationals_non_neg_def = Equals(RationalNonNeg,
                            SetOfAll(q, q, conditions=[greater_eq(q, zero)],
                                     domain=Rational))

rationals_non_neg_def:

%end axioms

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