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