Axioms for the theory of proveit.numbers.ordering

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)

%begin axioms

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

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

less_eq_def:

transitivity_less_less = Forall((x,y,z), Less(x, z),
                              conditions=[Less(x,y), Less(y, z)])

transitivity_less_less:

max_def_unary = Forall(x,
       Equals(Max(x), x),
       domain = Real)

max_def_unary:

min_def_unary = Forall(x,
       Equals(Min(x), x),
       domain = Real)

min_def_unary:

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:

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:

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:

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:

%end axioms

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