From 7eef54e605b0ce74d406bb5b6ad72a494ca54388 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 7 Dec 2006 18:20:52 +0000 Subject: [PATCH] reverted error committed by mistake --- matita/dama/integration_algebras.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ≝ -- 2.39.2