Notation is finally fully working everywhere.

What a great day!

diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/fields.ma
index 305c49764e9b651f368171ce00db323b29568956..5ab17edae98c7e2eafd4a3a94e65125ab9e7c433 100644 (file)
--- a/helm/software/matita/dama/fields.ma
+++ b/helm/software/matita/dama/fields.ma
@@ -21,7 +21,7 @@ record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
  {  (* multiplicative abelian properties *)
     mult_comm_: symmetric ? (mult R);
     (* multiplicative group properties *)
-    inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = 1
+    inv_inverse_: ∀x.∀p: x ≠ 0. inv x p * x = 1
  }.
 
 lemma opp_opp: ∀R:ring. ∀x:R. --x=x.

diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma
index 6d4e7c3c9dacace84caabf3591daecd0c97bf308..78b41cc105459b90a5709daf297f190e1596bda3 100644 (file)
--- a/helm/software/matita/dama/integration_algebras.ma
+++ b/helm/software/matita/dama/integration_algebras.ma
@@ -102,7 +102,7 @@ qed.
 coercion cic:/matita/integration_algebras/rs_ordered_abelian_group.con.
 
 record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
- { rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → zero V≤f → zero V≤a*f
+ { rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f
  }.
 
 record riesz_space (K:ordered_field_ch0) : Type \def
@@ -122,7 +122,7 @@ record sequentially_order_continuous (K) (V:riesz_space K) (T:V→K) : Prop ≝
      is_increasing K (λn.T (a n)) ∧ tends_to ? (λn.T (a n)) (T l)
  }.
 
-definition absolute_value \def λK.λS:riesz_space K.λf.l_join S f (-f).   
+definition absolute_value ≝ λK.λS:riesz_space K.λf:S.f ∨ -f.   
 
 (**************** Normed Riesz spaces ****************************)
 
@@ -175,7 +175,7 @@ definition is_weak_unit ≝
   3. Fremlin proves u > 0 implies x /\ u > 0  > 0 for Archimedean spaces
    only. We pick this definition for now.
 *) λR:real.λV:archimedean_riesz_space R.λe:V.
-    ∀v:V. lt V 0 v → lt V 0 (l_meet V v e).
+    ∀v:V. 0<v → 0 < (v ∧ e).
 
 (* Here we are avoiding a construction (the quotient space to define
    f=g iff I(|f-g|)=0 *)
@@ -188,14 +188,13 @@ record integration_riesz_space (R:real) : Type \def
    irs_limit1:
     ∀f:irs_archimedean_riesz_space.
      tends_to ?
-      (λn.integral (l_meet irs_archimedean_riesz_space f
-       ((sum_field R n)*irs_unit)))
+      (λn.integral (f ∧ ((sum_field R n)*irs_unit)))
        (integral f);
    irs_limit2:
     ∀f:irs_archimedean_riesz_space.
      tends_to ?
       (λn.
-        integral (l_meet irs_archimedean_riesz_space f
+        integral (f ∧
          ((inv ? (sum_field R (S n))
            (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))
          ) * irs_unit))) 0;
@@ -342,12 +341,9 @@ lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K.
 coercion cic:/matita/integration_algebras/fa_algebra.con.
 
 record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝ 
-{ compat_mult_le:
-   ∀f,g:A.
-    zero A ≤ f → zero A ≤ g → zero A ≤ a_mult ? A f g;
+{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g;
   compat_mult_meet:
-   ∀f,g,h:A.
-    l_meet A f g = (zero A) → l_meet A (a_mult ? A h f) g = (zero A)
+   ∀f,g,h:A.(f ∧ g) = 0 → ((h*f) ∧ g) = 0
 }.
 
 record f_algebra (K:ordered_field_ch0) : Type ≝ 

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index 27b10aeefbac510bfc7d65a7d4ae70873a6483a0..1ca191339b697514c39b171ed9111ef8c6a1003c 100644 (file)
--- a/helm/software/matita/dama/ordered_sets.ma
+++ b/helm/software/matita/dama/ordered_sets.ma
@@ -692,4 +692,4 @@ qed.
 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
 
 interpretation "Ordered set lt" 'lt a b =
- (cic:/matita/ordered_sets/lt.con _ _ a b).
+ (cic:/matita/ordered_sets/lt.con _ a b).

diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index c03fdf26bf6c4d6ef3a6eefecb57f5bdc4f41116..87bbee5fd0d2e84de0a9e49d8ee066f4d826e8b8 100644 (file)
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -147,7 +147,7 @@ lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
  elim daemon.
 qed.
  
-lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x.
+lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x.
  intros;
  unfold abs;
  unfold max;