logo

Axioms for the theory of proveit.numbers.number_sets.real_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, r, x
from proveit.logic import And, Equals, Forall, InSet, SetOfAll
from proveit.numbers import greater, Less, LessEq, number_ordering
from proveit.numbers import (zero, IntervalOO, IntervalCO, IntervalOC,
                            IntervalCC, Real, RealPos)
In [2]:
%begin axioms

Defining axioms for theory 'proveit.numbers.number_sets.real_numbers'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [3]:
real_pos_def = Equals(RealPos,
                       SetOfAll(r, r, conditions=[greater(r, zero)],
                                  domain=Real))
real_pos_def:

Being in a real interval means being real and being bound appropriately between the lower and upper bounds of the interval, and we define this for each of the 4 possible types of (finite) real intervals:

In [4]:
in_IntervalOO_def = Forall((a, b),
       Forall(x,
              Equals(InSet(x, IntervalOO(a, b)),
                     And(InSet(x, Real),
                         number_ordering(Less(a, x), Less(x, b))))),
       domain=Real)
in_IntervalOO_def:
In [5]:
in_IntervalOC_def = \
    Forall((a, b),
           Forall(x,
                  Equals(InSet(x, IntervalOC(a, b)),
                         And(InSet(x, Real),
                             number_ordering(Less(a, x), LessEq(x, b))))),
           domain=Real)
in_IntervalOC_def:
In [6]:
in_IntervalCO_def = \
    Forall((a, b),
           Forall(x,
                  Equals(InSet(x, IntervalCO(a, b)),
                         And(InSet(x, Real),
                             number_ordering(LessEq(a, x), Less(x, b))))),
           domain=Real)
in_IntervalCO_def:
In [7]:
in_IntervalCC_def = \
    Forall((a, b),
           Forall(x,
                  Equals(InSet(x, IntervalCC(a, b)),
                         And(InSet(x, Real),
                             number_ordering(LessEq(a, x), LessEq(x, b))))),
           domain=Real)
in_IntervalCC_def:
In [8]:
%end axioms

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