From ddc91018331d65f4c43b7c051c6fd07b614ea46b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Nov 2008 12:13:44 +0000 Subject: [PATCH 1/1] ... --- .../contribs/dama/dama/models/nat_dedekind_sigma_complete.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index 73211e023..9a43d186d 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -27,7 +27,7 @@ coercion hint1 nocomposites. alias symbol "pi1" = "exT \fst". alias symbol "N" = "ordered set N". -lemma nat_dedekind_sigma_complete: +lemma increasing_supremum_stabilizes: ∀sg:‡ℕ.∀a:sequence {[sg]}. a is_increasing → ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j). @@ -133,6 +133,6 @@ qed. coercion hint2 nocomposites. alias symbol "N" = "ordered set N". -axiom nat_dedekind_sigma_complete_r: +axiom increasing_supremum_stabilizes_r: ∀s:‡ℕ.∀a:sequence {[s]}.a is_decreasing → ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j). -- 2.39.2