From 810db29f760117d933ee1f74328043b8fce43847 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 3 Jan 2007 17:33:22 +0000
Subject: [PATCH] Notation is finally fully working everywhere. What a great
 day!

---
 matita/dama/fields.ma               |  2 +-
 matita/dama/integration_algebras.ma | 18 +++++++-----------
 matita/dama/ordered_sets.ma         |  2 +-
 matita/dama/reals.ma                |  2 +-
 4 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/matita/dama/fields.ma b/matita/dama/fields.ma
index 305c49764..5ab17edae 100644
--- a/matita/dama/fields.ma
+++ b/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/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma
index 6d4e7c3c9..78b41cc10 100644
--- a/matita/dama/integration_algebras.ma
+++ b/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/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma
index 27b10aeef..1ca191339 100644
--- a/matita/dama/ordered_sets.ma
+++ b/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/matita/dama/reals.ma b/matita/dama/reals.ma
index c03fdf26b..87bbee5fd 100644
--- a/matita/dama/reals.ma
+++ b/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;
-- 
2.39.2