In Order_ZF we define some notions related to order relations
based on the nonstrict orders (
In this section we introduce some definitions taken from Metamath and relate them to the ones used by the standard Isabelle Order.thy.
The next definition is the strict version of the linear order.
What we write as R Orders A is written
definition
The definition of supremum for a (strict) linear order.
definition
Definition of infimum for a linear order. It is defined in terms of supremum.
definition
If relation
lemma orders_imp_tot_ord:
assumes A1:
A converse of orders_imp_tot_ord. Together with that theorem this shows that Metamath's notion of an order relation is equivalent to Isabelles tot_ord predicate.
lemma tot_ord_imp_orders:
assumes A1:
In this section we discuss the properties of strict order relations. This continues the development contained in the standard Isabelle's Order.thy with a view towards using the theorems translated from Metamath.
A relation orders a set iff the converse relation orders a set. Going
one way we can use the the lemma tot_od_converse from the standard
Isabelle's Order.thy.The other way is a bit more complicated (note that
in Isabelle for
lemma cnvso:
showsSupremum is unique, if it exists.
lemma supeu:
assumes A1:
Supremum has expected properties if it exists.
lemma sup_props:
assumes A1:
Elements greater or equal than any element of
lemma supnub:
assumes A1: