+record is_integral (K) (R:archimedean_riesz_space K) (I:Type_OF_archimedean_riesz_space ? R→K) : Prop
+\def
+ { i_positive: ∀f:R. le ? R 0 f → of_le K 0 (I f);
+ i_linear1: ∀f,g:R. I (f + g) = I f + I g;
+ i_linear2: ∀f:R.∀k:K. I (emult ? R k f) = k*(I f)
+ }.
+
+definition is_weak_unit ≝
+(* This definition is by Spitters. He cites Fremlin 353P, but:
+ 1. that theorem holds only in f-algebras (as in Spitters, but we are
+ defining it on Riesz spaces)
+ 2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value?
+ λR:real.λV:archimedean_riesz_space R.λunit: V.
+ ∀x:V. meet x unit = 0 → u = 0.
+*) λR:real.λV:archimedean_riesz_space R.λe:V.True.
+
+record integration_riesz_space (R:real) : Type \def
+ { irs_archimedean_riesz_space:> archimedean_riesz_space R;
+ irs_unit: Type_OF_archimedean_riesz_space ? irs_archimedean_riesz_space;
+ irs_weak_unit: is_weak_unit ? ? irs_unit;
+ integral: Type_OF_archimedean_riesz_space ? irs_archimedean_riesz_space → R;
+ irs_integral_properties: is_integral R irs_archimedean_riesz_space integral;
+ irs_limit1:
+ ∀f:irs_archimedean_riesz_space.
+ tends_to ?
+ (λn.integral (meet ? irs_archimedean_riesz_space f
+ ((sum_field R n)*irs_unit)))
+ (integral f);
+ irs_limit2:
+ ∀f:irs_archimedean_riesz_space.
+ tends_to ?
+ (λn.
+ integral (meet ? irs_archimedean_riesz_space 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;
+ irs_quotient_space1:
+ ∀f,g:irs_archimedean_riesz_space.
+ f=g → integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0
+ }.
+