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

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