]> matita.cs.unibo.it Git - helm.git/commitdiff
reverted error committed by mistake
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 7 Dec 2006 18:20:52 +0000 (18:20 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 7 Dec 2006 18:20:52 +0000 (18:20 +0000)
helm/software/matita/dama/integration_algebras.ma

index dc0ad9d3277cd1274da16cc8caa748e92b77aa2a..46bebc0e9da6745255d64691b99f5fe6a00eb7e2 100644 (file)
@@ -146,7 +146,7 @@ record integration_riesz_space (R:real) : Type \def
          ) * irs_unit))) 0;
    irs_quotient_space1:
     ∀f,g:irs_archimedean_riesz_space.
-     integral (absolute_value irs_archimedean_riesz_space (f - g)) = 0 → f=g
+     integral (absolute_value irs_archimedean_riesz_space (f - g)) = 0 → f=g
  }.
 
 definition induced_norm_fun ≝