From c156170ba340354ea3da250b4d6c35d80c855849 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 30 Dec 2006 21:00:18 +0000 Subject: [PATCH] le x y ==> x \leq y (now possible because of a bug fix in coercion serialization in .moo files) --- helm/software/matita/dama/ordered_fields_ch0.ma | 4 ++-- helm/software/matita/dama/vector_spaces.ma | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma index 07f32fade..1c3b0fe7c 100644 --- a/helm/software/matita/dama/ordered_fields_ch0.ma +++ b/helm/software/matita/dama/ordered_fields_ch0.ma @@ -121,7 +121,7 @@ axiom lt_zero_to_le_inv_zero: definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop. apply (λF:ordered_field_ch0.λf:nat → F.λl:F. - ∀n:nat.∃m:nat.∀j:nat. le m j → + ∀n:nat.∃m:nat.∀j:nat.m ≤ j → l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧ f j ≤ l + (inv F (sum_field ? (S n)) ?)); apply not_eq_sum_field_zero; @@ -143,7 +143,7 @@ definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop. apply (λF:ordered_field_ch0.λf:nat→F. ∀m:nat. - ∃n:nat.∀N. le n N → + ∃n:nat.∀N.n ≤ N → -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧ f N - f n ≤ inv ? (sum_field F (S m)) ?); apply not_eq_sum_field_zero; diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/vector_spaces.ma index 3165be2e6..de4af986a 100644 --- a/helm/software/matita/dama/vector_spaces.ma +++ b/helm/software/matita/dama/vector_spaces.ma @@ -123,7 +123,7 @@ definition tends_to : ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop. apply (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V. - ∀n:nat.∃m:nat.∀j:nat. le m j → + ∀n:nat.∃m:nat.∀j:nat. m ≤ j → d (f j) l ≤ inv R (sum_field ? (S n)) ?); apply not_eq_sum_field_zero; unfold; @@ -136,7 +136,7 @@ definition is_cauchy_seq : ∀R:real.\forall V:vector_space R. (λR:real.λV: vector_space R. \lambda d:distance ? V. \lambda f:nat→V. ∀m:nat. - ∃n:nat.∀N. le n N → + ∃n:nat.∀N. n ≤ N → -(inv R (sum_field ? (S m)) ?) ≤ d (f N) (f n) ∧ d (f N) (f n)≤ inv R (sum_field R (S m)) ?); apply not_eq_sum_field_zero; -- 2.39.2