From: Stefano Zacchiroli Date: Thu, 7 Dec 2006 18:20:52 +0000 (+0000) Subject: reverted error committed by mistake X-Git-Tag: 0.4.95@7852~743 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7eef54e605b0ce74d406bb5b6ad72a494ca54388;p=helm.git reverted error committed by mistake --- diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma index dc0ad9d32..46bebc0e9 100644 --- a/matita/dama/integration_algebras.ma +++ b/matita/dama/integration_algebras.ma @@ -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 ≝