]> matita.cs.unibo.it Git - helm.git/commitdiff
typo
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Jun 2008 12:42:38 +0000 (12:42 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Jun 2008 12:42:38 +0000 (12:42 +0000)
helm/software/matita/contribs/dama/dama/supremum.ma

index 468c1d5060be04c7f0a803b01dc14581668590d9..6d5879a8378e6fcd92c71dfeeba7785af5942580 100644 (file)
@@ -216,7 +216,7 @@ qed.
 (* Definition 2.7 *)
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
-   ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
+   exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
      (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
                    (u i) is_supremum ⌊w,a (w+i)⌋).