1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/ordered_set/".
17 include "excedence.ma".
19 record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ {
20 por_reflexive: reflexive ? le;
21 por_transitive: transitive ? le;
22 por_antisimmetric: antisymmetric ? le eq
25 record pordered_set: Type ≝ {
27 pos_order_relation_properties:> is_porder_relation ? (le pos_carr) (eq pos_carr)
30 lemma pordered_set_of_excedence: excedence → pordered_set.
31 intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation);
32 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
35 alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con".
36 alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con".
37 alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con".
39 definition total_order_property : ∀E:excedence. Type ≝
40 λE:excedence. ∀a,b:E. a ≰ b → b < a.
42 record tordered_set : Type ≝ {
43 tos_poset:> pordered_set;
44 tos_totality: total_order_property tos_poset