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
rationals_def = Equals(
Rational,
SetOfAll([a, b],
frac(a, b),
conditions=[NotEquals(b, zero)],
domain=Integer
))
rationals_pos_def = Equals(RationalPos,
SetOfAll(q, q, conditions=[greater(q, zero)],
domain=Rational))
rationals_neg_def = Equals(RationalNeg,
SetOfAll(q, q, conditions=[Less(q, zero)],
domain=Rational))
rationals_non_neg_def = Equals(RationalNonNeg,
SetOfAll(q, q, conditions=[greater_eq(q, zero)],
domain=Rational))
%end axioms