# Axioms for the theory of proveit.numbers.ordering¶

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 b, m, n, x, y, z, Conditional, ConditionalSet
from proveit.core_expr_types import a_1_to_m
from proveit.logic import Forall, Or, Equals
from proveit.numbers import (greater, greater_eq, Less, LessEq,
Max, Min, Natural, NaturalPos, Real)

In [2]:
%begin axioms

Defining axioms for theory 'proveit.numbers.ordering'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

In [3]:
less_eq_def = Forall([x, y], Equals(LessEq(x, y), Or(Less(x, y), Equals(x, y))))

less_eq_def:
In [4]:
transitivity_less_less = Forall((x,y,z), Less(x, z),
conditions=[Less(x,y), Less(y, z)])

transitivity_less_less:
In [5]:
max_def_unary = Forall(x,
Equals(Max(x), x),
domain = Real)

max_def_unary:
In [6]:
min_def_unary = Forall(x,
Equals(Min(x), x),
domain = Real)

min_def_unary:
In [7]:
max_def_bin = (
Forall((x, y),
Equals(Max(x, y),
ConditionalSet(Conditional(x, greater_eq(x, y)),
Conditional(y, greater(y, x)))),
domain = Real))

max_def_bin:
In [8]:
min_def_bin = (
Forall((x, y),
Equals(Min(x, y),
ConditionalSet(Conditional(x, LessEq(x, y)),
Conditional(y, Less(y, x)))),
domain = Real))

min_def_bin:
In [9]:
max_def_multi = (
Forall(m,
Forall((a_1_to_m, b),
Equals(Max(a_1_to_m, b), Max(Max(a_1_to_m), b)),
domain=Real),
domain=NaturalPos))

max_def_multi:
In [10]:
min_def_multi = (
Forall(m,
Forall((a_1_to_m, b),
Equals(Min(a_1_to_m, b), Min(Min(a_1_to_m), b)),
domain=Real),
domain=NaturalPos))

min_def_multi:
In [11]:
%end axioms

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