From: Claudio Sacerdoti Coen Date: Sat, 30 Dec 2006 21:00:18 +0000 (+0000) Subject: le x y ==> x \leq y (now possible because of a bug fix in coercion X-Git-Tag: 0.4.95@7852~695 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ac783aa7646c36a2c6db08ac8f21f1ec99cd55ee;p=helm.git le x y ==> x \leq y (now possible because of a bug fix in coercion serialization in .moo files) --- diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma index 07f32fade..1c3b0fe7c 100644 --- a/matita/dama/ordered_fields_ch0.ma +++ b/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/matita/dama/vector_spaces.ma b/matita/dama/vector_spaces.ma index 3165be2e6..de4af986a 100644 --- a/matita/dama/vector_spaces.ma +++ b/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;