From f3ad825f16c02c0c5fca620980882e409871e6f1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Jun 2008 12:42:38 +0000 Subject: [PATCH] typo --- helm/software/matita/contribs/dama/dama/supremum.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 468c1d506..6d5879a83 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -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)⌋). -- 2.39.5