tt('const/lebesgue/RADON_F', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > $o)))).
tt('const/lebesgue/RADON_F_integrals', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ('type/extreal/extreal' > $o)))).
tt('const/lebesgue/finite_space_integral', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > 'type/extreal/extreal'))).
tt('const/lebesgue/fn_seq', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > ('type/num/num' > (A > 'type/extreal/extreal'))))).
tt('const/lebesgue/fn_seq_integral', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > ('type/num/num' > 'type/extreal/extreal')))).
tt('const/lebesgue/integrable', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > $o))).
tt('const/lebesgue/integral', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > 'type/extreal/extreal'))).
tt('const/lebesgue/max_fn_seq', ty, ![A : $t]: (('type/num/num' > (A > 'type/extreal/extreal')) > ('type/num/num' > (A > 'type/extreal/extreal')))).
tt('const/lebesgue/measure_absolutely_continuous', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o))).
tt('const/lebesgue/negative_set', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > $o) > $o))).
tt('const/lebesgue/pos_fn_integral', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > 'type/extreal/extreal'))).
tt('const/lebesgue/pos_simple_fn_integral', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/num/num' > $o) > (('type/num/num' > (A > $o)) > (('type/num/num' > 'type/realax/real') > 'type/extreal/extreal'))))).
tt('const/lebesgue/prod_measure', ty, ![A : $t, B : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) > ((('type/pair/prod' A B) > $o) > 'type/realax/real')))).
tt('const/lebesgue/prod_measure3', ty, ![A : $t, B : $t, C : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) > (('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real'))) > ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real'))))).
tt('const/lebesgue/prod_measure_space', ty, ![A : $t, B : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) > ('type/pair/prod' (('type/pair/prod' A B) > $o) ('type/pair/prod' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real')))))).
tt('const/lebesgue/prod_measure_space3', ty, ![A : $t, B : $t, C : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) > (('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real'))) > ('type/pair/prod' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) ('type/pair/prod' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real'))))))).
tt('const/lebesgue/prod_sets3', ty, ![A : $t, B : $t, C : $t]: (((A > $o) > $o) > (((B > $o) > $o) > (((C > $o) > $o) > ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o))))).
tt('const/lebesgue/psfis', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > ('type/extreal/extreal' > $o)))).
tt('const/lebesgue/psfs', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > 'type/extreal/extreal') > (('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) > $o)))).
tt('const/lebesgue/seq_sup', ty, (('type/extreal/extreal' > $o) > ('type/num/num' > 'type/extreal/extreal'))).
tt('const/lebesgue/signed_measure_space', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('thm/lebesgue/pos_simple_fn_integral_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = ('const/extreal/Normal' (('const/real_sigma/REAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/realax/real_mul' (x i) (('const/measure/measure' A) m (a i)))) s))))).
tt('thm/lebesgue/psfs_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/psfs' A) m f) = (('const/pred_set/GSPEC' ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real')))) (('const/pair/UNCURRY' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real')) ('type/pair/prod' ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) $o)) (^[s : ('type/num/num' > $o)]: (('const/pair/UNCURRY' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real') ('type/pair/prod' ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) $o)) (^[a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (('const/pair/,' ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) $o) (('const/pair/,' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) s (('const/pair/,' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real')) a x)) (('const/measure/pos_simple_fn' A) m f s a x)))))))))).
tt('thm/lebesgue/psfis_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/psfis' A) m f) = (('const/pred_set/IMAGE' ('type/pair/prod' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real'))) 'type/extreal/extreal') (('const/pair/UNCURRY' ('type/num/num' > $o) ('type/pair/prod' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real')) 'type/extreal/extreal') (^[s : ('type/num/num' > $o)]: (('const/pair/UNCURRY' ('type/num/num' > (A > $o)) ('type/num/num' > 'type/realax/real') 'type/extreal/extreal') (^[a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (('const/lebesgue/pos_simple_fn_integral' A) m s a x))))) (('const/lebesgue/psfs' A) m f))))).
tt('thm/lebesgue/pos_fn_integral_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/pos_fn_integral' A) m f) = ('const/extreal/extreal_sup' (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) r (?[g : (A > 'type/extreal/extreal')]: ((('const/bool/IN' 'type/extreal/extreal') r (('const/lebesgue/psfis' A) m g)) & (![x : A]: ('const/extreal/extreal_le' (g x) (f x)))))))))))).
tt('thm/lebesgue/integral_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/integral' A) m f) = ('const/extreal/extreal_sub' (('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_plus' A) f)) (('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_minus' A) f)))))).
tt('thm/lebesgue/integrable_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/integrable' A) m f) = ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((~ ((('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_plus' A) f)) = 'const/extreal/PosInf')) & (~ ((('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_minus' A) f)) = 'const/extreal/PosInf'))))))).
tt('thm/lebesgue/finite_space_integral_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/finite_space_integral' A) m f) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ('const/extreal/extreal_mul' r ('const/extreal/Normal' (('const/measure/measure' A) m (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A 'type/extreal/extreal') f (('const/pred_set/INSERT' 'type/extreal/extreal') r ('const/pred_set/EMPTY' 'type/extreal/extreal'))) (('const/measure/m_space' A) m)))))) (('const/pred_set/IMAGE' A 'type/extreal/extreal') f (('const/measure/m_space' A) m)))))).
tt('thm/lebesgue/prod_measure_def_', def, ![A : $t, B : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: ((('const/lebesgue/prod_measure' A B) m0 m1) = (^[a : (('type/pair/prod' A B) > $o)]: ('const/extreal/real' (('const/lebesgue/integral' A) m0 (^[s0 : A]: ('const/extreal/Normal' (('const/measure/measure' B) m1 (('const/util_prob/PREIMAGE' B ('type/pair/prod' A B)) (^[s1 : B]: (('const/pair/,' A B) s0 s1)) a)))))))))).
tt('thm/lebesgue/prod_measure_space_def_', def, ![B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: ((('const/lebesgue/prod_measure_space' A B) m0 m1) = (('const/pair/,' (('type/pair/prod' A B) > $o) ('type/pair/prod' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A B) (('const/measure/m_space' A) m0) (('const/measure/m_space' B) m1)) (('const/pair/,' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real')) (('const/measure/subsets' ('type/pair/prod' A B)) (('const/measure/sigma' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) (('const/measure/m_space' A) m0) (('const/measure/m_space' B) m1)) (('const/util_prob/prod_sets' A B) (('const/measure/measurable_sets' A) m0) (('const/measure/measurable_sets' B) m1)))) (('const/lebesgue/prod_measure' A B) m0 m1)))))).
tt('thm/lebesgue/prod_sets3_def_', def, ![C : $t, B : $t, A : $t]: (![a : ((A > $o) > $o), b : ((B > $o) > $o), c : ((C > $o) > $o)]: ((('const/lebesgue/prod_sets3' A B C) a b c) = (('const/pred_set/GSPEC' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) ('type/pair/prod' (A > $o) ('type/pair/prod' (B > $o) (C > $o)))) (('const/pair/UNCURRY' (A > $o) ('type/pair/prod' (B > $o) (C > $o)) ('type/pair/prod' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) $o)) (^[s : (A > $o)]: (('const/pair/UNCURRY' (B > $o) (C > $o) ('type/pair/prod' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) $o)) (^[t : (B > $o), u : (C > $o)]: (('const/pair/,' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) $o) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) s (('const/pred_set/CROSS' B C) t u)) ((('const/bool/IN' (A > $o)) s a) & ((('const/bool/IN' (B > $o)) t b) & (('const/bool/IN' (C > $o)) u c)))))))))))).
tt('thm/lebesgue/prod_measure3_def_', def, ![C : $t, B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real')))]: ((('const/lebesgue/prod_measure3' A B C) m0 m1 m2) = (('const/lebesgue/prod_measure' A ('type/pair/prod' B C)) m0 (('const/lebesgue/prod_measure_space' B C) m1 m2))))).
tt('thm/lebesgue/prod_measure_space3_def_', def, ![C : $t, B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real')))]: ((('const/lebesgue/prod_measure_space3' A B C) m0 m1 m2) = (('const/pair/,' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) ('type/pair/prod' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) (('const/measure/m_space' A) m0) (('const/pred_set/CROSS' B C) (('const/measure/m_space' B) m1) (('const/measure/m_space' C) m2))) (('const/pair/,' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real')) (('const/measure/subsets' ('type/pair/prod' A ('type/pair/prod' B C))) (('const/measure/sigma' ('type/pair/prod' A ('type/pair/prod' B C))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) (('const/measure/m_space' A) m0) (('const/pred_set/CROSS' B C) (('const/measure/m_space' B) m1) (('const/measure/m_space' C) m2))) (('const/lebesgue/prod_sets3' A B C) (('const/measure/measurable_sets' A) m0) (('const/measure/measurable_sets' B) m1) (('const/measure/measurable_sets' C) m2)))) (('const/lebesgue/prod_measure3' A B C) m0 m1 m2)))))).
tt('thm/lebesgue/pos_simple_fn_integral_present_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), 's\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g 's\'' b y))) => (?[z : ('type/num/num' > 'type/realax/real'), 'z\'' : ('type/num/num' > 'type/realax/real'), c : ('type/num/num' > (A > $o)), k : ('type/num/num' > $o)]: ((![t : A]: ((('const/bool/IN' A) t (('const/measure/m_space' A) m)) => ((f t) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' (z i)) (('const/measure/indicator_fn' A) (c i) t))) k)))) & ((![t : A]: ((('const/bool/IN' A) t (('const/measure/m_space' A) m)) => ((g t) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' ('z\'' i)) (('const/measure/indicator_fn' A) (c i) t))) k)))) & (((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = (('const/lebesgue/pos_simple_fn_integral' A) m k c z)) & (((('const/lebesgue/pos_simple_fn_integral' A) m 's\'' b y) = (('const/lebesgue/pos_simple_fn_integral' A) m k c 'z\'')) & ((('const/pred_set/FINITE' 'type/num/num') k) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (z i)))) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('z\'' i)))) & ((![i : 'type/num/num', j : 'type/num/num']: (((('const/bool/IN' 'type/num/num') i k) & ((('const/bool/IN' 'type/num/num') j k) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (c i) (c j)))) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => (('const/bool/IN' (A > $o)) (c i) (('const/measure/measurable_sets' A) m)))) & ((('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) c k)) = (('const/measure/m_space' A) m))))))))))))))).
tt('thm/lebesgue/psfis_present_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & (('const/bool/IN' 'type/extreal/extreal') b (('const/lebesgue/psfis' A) m g)))) => (?[z : ('type/num/num' > 'type/realax/real'), 'z\'' : ('type/num/num' > 'type/realax/real'), c : ('type/num/num' > (A > $o)), k : ('type/num/num' > $o)]: ((![t : A]: ((('const/bool/IN' A) t (('const/measure/m_space' A) m)) => ((f t) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' (z i)) (('const/measure/indicator_fn' A) (c i) t))) k)))) & ((![t : A]: ((('const/bool/IN' A) t (('const/measure/m_space' A) m)) => ((g t) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' ('z\'' i)) (('const/measure/indicator_fn' A) (c i) t))) k)))) & ((a = (('const/lebesgue/pos_simple_fn_integral' A) m k c z)) & ((b = (('const/lebesgue/pos_simple_fn_integral' A) m k c 'z\'')) & ((('const/pred_set/FINITE' 'type/num/num') k) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (z i)))) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('z\'' i)))) & ((![i : 'type/num/num', j : 'type/num/num']: (((('const/bool/IN' 'type/num/num') i k) & ((('const/bool/IN' 'type/num/num') j k) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (c i) (c j)))) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i k) => (('const/bool/IN' (A > $o)) (c i) (('const/measure/measurable_sets' A) m)))) & ((('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) c k)) = (('const/measure/m_space' A) m))))))))))))))).
tt('thm/lebesgue/pos_simple_fn_thm1_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), i : 'type/num/num', y : A]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & ((('const/bool/IN' 'type/num/num') i s) & (('const/bool/IN' A) y (a i))))) => ((f y) = ('const/extreal/Normal' (x i)))))).
tt('thm/lebesgue/pos_simple_fn_le_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), 'x\'' : ('type/num/num' > 'type/realax/real'), i : 'type/num/num']: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & ((('const/measure/pos_simple_fn' A) m g s a 'x\'') & ((![x0 : A]: ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' (g x0) (f x0)))) & ((('const/bool/IN' 'type/num/num') i s) & (~ ((a i) = ('const/pred_set/EMPTY' A)))))))) => ('const/extreal/extreal_le' ('const/extreal/Normal' ('x\'' i)) ('const/extreal/Normal' (x i)))))).
tt('thm/lebesgue/pos_simple_fn_cmul_', ax, ![A : $t]: (![x : ('type/num/num' > 'type/realax/real'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), z : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z))) => (?['s\'' : ('type/num/num' > $o), 'a\'' : ('type/num/num' > (A > $o)), 'x\'' : ('type/num/num' > 'type/realax/real')]: (('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f t))) 's\'' 'a\'' 'x\''))))).
tt('thm/lebesgue/pos_simple_fn_cmul_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), z : 'type/realax/real']: (((('const/measure/measure_space' A) m) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z) & (('const/measure/pos_simple_fn' A) m f s a x))) => (('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f t))) s a (^[i : 'type/num/num']: ('const/realax/real_mul' z (x i))))))).
tt('thm/lebesgue/pos_simple_fn_add_', ax, ![A : $t]: (!['x\'' : ('type/num/num' > 'type/realax/real'), x : ('type/num/num' > 'type/realax/real'), 's\'' : ('type/num/num' > $o), s : ('type/num/num' > $o), 'a\'' : ('type/num/num' > (A > $o)), a : ('type/num/num' > (A > $o)), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g 's\'' 'a\'' 'x\''))) => (?['s\'\'' : ('type/num/num' > $o), 'a\'\'' : ('type/num/num' > (A > $o)), 'x\'\'' : ('type/num/num' > 'type/realax/real')]: (('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_add' (f t) (g t))) 's\'\'' 'a\'\'' 'x\'\''))))).
tt('thm/lebesgue/pos_simple_fn_add_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g s a y))) => (('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_add' (f t) (g t))) s a (^[i : 'type/num/num']: ('const/realax/real_add' (x i) (y i))))))).
tt('thm/lebesgue/pos_simple_fn_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), A0 : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m))) => (?[s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (('const/measure/pos_simple_fn' A) m (('const/measure/indicator_fn' A) A0) s a x))))).
tt('thm/lebesgue/pos_simple_fn_indicator_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => (('const/measure/pos_simple_fn' A) m (('const/measure/indicator_fn' A) s) (('const/pred_set/INSERT' 'type/num/num') 'const/num/0' (('const/pred_set/INSERT' 'type/num/num') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/pred_set/EMPTY' 'type/num/num'))) (^[i : 'type/num/num']: (('const/bool/COND' (A > $o)) (i = 'const/num/0') (('const/pred_set/DIFF' A) (('const/measure/m_space' A) m) s) s)) (^[i : 'type/num/num']: (('const/bool/COND' 'type/realax/real') (i = 'const/num/0') ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/lebesgue/pos_simple_fn_max_', ax, ![A : $t, B : $t]: (!['s\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), 's\'b' : B, y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g 's\'' b y))) => (?['s\'\'' : ('type/num/num' > $o), 'a\'\'' : ('type/num/num' > (A > $o)), 'x\'\'' : ('type/num/num' > 'type/realax/real')]: (('const/measure/pos_simple_fn' A) m (^[x0 : A]: ('const/extreal/extreal_max' (f x0) (g x0))) 's\'\'' 'a\'\'' 'x\'\''))))).
tt('thm/lebesgue/pos_simple_fn_not_infty_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m f s a x) => (![x0 : A]: ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) => ((~ ((f x0) = 'const/extreal/NegInf')) & (~ ((f x0) = 'const/extreal/PosInf')))))))).
tt('thm/lebesgue/pos_simple_fn_integral_add_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), 's\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g 's\'' b y))) => (?['s\'\'' : ('type/num/num' > $o), c : ('type/num/num' > (A > $o)), z : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m (^[x0 : A]: ('const/extreal/extreal_add' (f x0) (g x0))) 's\'\'' c z) & (('const/extreal/extreal_add' (('const/lebesgue/pos_simple_fn_integral' A) m s a x) (('const/lebesgue/pos_simple_fn_integral' A) m 's\'' b y)) = (('const/lebesgue/pos_simple_fn_integral' A) m 's\'\'' c z))))))).
tt('thm/lebesgue/pos_simple_fn_integral_add_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g s a y))) => (('const/extreal/extreal_add' (('const/lebesgue/pos_simple_fn_integral' A) m s a x) (('const/lebesgue/pos_simple_fn_integral' A) m s a y)) = (('const/lebesgue/pos_simple_fn_integral' A) m s a (^[i : 'type/num/num']: ('const/realax/real_add' (x i) (y i)))))))).
tt('thm/lebesgue/psfis_add_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & (('const/bool/IN' 'type/extreal/extreal') b (('const/lebesgue/psfis' A) m g)))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_add' a b) (('const/lebesgue/psfis' A) m (^[x : A]: ('const/extreal/extreal_add' (f x) (g x)))))))).
tt('thm/lebesgue/pos_simple_fn_integral_mono_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), 's\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & ((('const/measure/pos_simple_fn' A) m g 's\'' b y) & (![x0 : A]: ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' (f x0) (g x0))))))) => ('const/extreal/extreal_le' (('const/lebesgue/pos_simple_fn_integral' A) m s a x) (('const/lebesgue/pos_simple_fn_integral' A) m 's\'' b y))))).
tt('thm/lebesgue/psfis_mono_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & ((('const/bool/IN' 'type/extreal/extreal') b (('const/lebesgue/psfis' A) m g)) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' (f x) (g x))))))) => ('const/extreal/extreal_le' a b)))).
tt('thm/lebesgue/pos_simple_fn_integral_unique_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), 's\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m f 's\'' b y))) => ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = (('const/lebesgue/pos_simple_fn_integral' A) m 's\'' b y))))).
tt('thm/lebesgue/psfis_unique_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & (('const/bool/IN' 'type/extreal/extreal') b (('const/lebesgue/psfis' A) m f)))) => (a = b)))).
tt('thm/lebesgue/pos_simple_fn_integral_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), A0 : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m))) => (?[s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m (('const/measure/indicator_fn' A) A0) s a x) & ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = ('const/extreal/Normal' (('const/measure/measure' A) m A0)))))))).
tt('thm/lebesgue/psfis_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), A0 : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/Normal' (('const/measure/measure' A) m A0)) (('const/lebesgue/psfis' A) m (('const/measure/indicator_fn' A) A0)))))).
tt('thm/lebesgue/pos_simple_fn_integral_cmul_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), z : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m f s a x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z))) => ((('const/measure/pos_simple_fn' A) m (^[x0 : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f x0))) s a (^[i : 'type/num/num']: ('const/realax/real_mul' z (x i)))) & ((('const/lebesgue/pos_simple_fn_integral' A) m s a (^[i : 'type/num/num']: ('const/realax/real_mul' z (x i)))) = ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (('const/lebesgue/pos_simple_fn_integral' A) m s a x))))))).
tt('thm/lebesgue/psfis_cmul_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', z : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_mul' ('const/extreal/Normal' z) a) (('const/lebesgue/psfis' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f x)))))))).
tt('thm/lebesgue/pos_simple_fn_integral_cmul_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), z : 'type/realax/real']: (((('const/measure/measure_space' A) m) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z) & (('const/measure/pos_simple_fn' A) m f s a x))) => (?['s\'' : ('type/num/num' > $o), 'a\'' : ('type/num/num' > (A > $o)), 'x\'' : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f t))) 's\'' 'a\'' 'x\'') & ((('const/lebesgue/pos_simple_fn_integral' A) m 's\'' 'a\'' 'x\'') = ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (('const/lebesgue/pos_simple_fn_integral' A) m s a x)))))))).
tt('thm/lebesgue/IN_psfis_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), r : 'type/extreal/extreal', f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' 'type/extreal/extreal') r (('const/lebesgue/psfis' A) m f)) => (?[s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m f s a x) & (r = (('const/lebesgue/pos_simple_fn_integral' A) m s a x))))))).
tt('thm/lebesgue/IN_psfis_eq_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), r : 'type/extreal/extreal', f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' 'type/extreal/extreal') r (('const/lebesgue/psfis' A) m f)) = (?[s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m f s a x) & (r = (('const/lebesgue/pos_simple_fn_integral' A) m s a x))))))).
tt('thm/lebesgue/psfis_pos_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & (('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f))) => (![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))))).
tt('thm/lebesgue/pos_simple_fn_integral_zero_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & (('const/measure/pos_simple_fn' A) m (^[t : A]: ('const/extreal/extreal_of_num' 'const/num/0')) s a x)) => ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/lebesgue/pos_simple_fn_integral_zero_alt_', ax, ![A : $t]: (![g : (A > 'type/extreal/extreal'), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/measure/pos_simple_fn' A) m g s a x) & (![x0 : A]: ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) => ((g x0) = ('const/extreal/extreal_of_num' 'const/num/0')))))) => ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/lebesgue/psfis_zero_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), a : 'type/extreal/extreal']: ((('const/measure/measure_space' A) m) => ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0')))) = (a = ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/lebesgue/pos_simple_fn_integral_not_infty_0', ax, ![A : $t]: (![x : ('type/num/num' > 'type/realax/real'), s : ('type/num/num' > $o), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), a : ('type/num/num' > (A > $o))]: (~ ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = 'const/extreal/NegInf')))).
tt('thm/lebesgue/pos_simple_fn_integral_not_infty_e1', ax, ![A : $t]: (![x : ('type/num/num' > 'type/realax/real'), s : ('type/num/num' > $o), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), a : ('type/num/num' > (A > $o))]: (~ ((('const/lebesgue/pos_simple_fn_integral' A) m s a x) = 'const/extreal/PosInf')))).
tt('thm/lebesgue/psfis_not_infty_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) => ((~ (a = 'const/extreal/NegInf')) & (~ (a = 'const/extreal/PosInf')))))).
tt('thm/lebesgue/pos_simple_fn_integral_sum_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (B > (A > 'type/extreal/extreal')), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : (B > ('type/num/num' > 'type/realax/real')), P : (B > $o)]: (((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i P) => (('const/measure/pos_simple_fn' A) m (f i) s a (x i)))) & ((('const/pred_set/FINITE' B) P) & (~ (P = ('const/pred_set/EMPTY' B)))))) => ((('const/measure/pos_simple_fn' A) m (^[t : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (f i t)) P)) s a (^[i : 'type/num/num']: (('const/real_sigma/REAL_SUM_IMAGE' B) (^[j : B]: (x j i)) P))) & ((('const/lebesgue/pos_simple_fn_integral' A) m s a (^[j : 'type/num/num']: (('const/real_sigma/REAL_SUM_IMAGE' B) (^[i : B]: (x i j)) P))) = (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (('const/lebesgue/pos_simple_fn_integral' A) m s a (x i))) P)))))).
tt('thm/lebesgue/pos_simple_fn_integral_sum_alt_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (B > (A > 'type/extreal/extreal')), s : (B > ('type/num/num' > $o)), a : (B > ('type/num/num' > (A > $o))), x : (B > ('type/num/num' > 'type/realax/real')), P : (B > $o)]: (((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i P) => (('const/measure/pos_simple_fn' A) m (f i) (s i) (a i) (x i)))) & ((('const/pred_set/FINITE' B) P) & (~ (P = ('const/pred_set/EMPTY' B)))))) => (?[c : ('type/num/num' > (A > $o)), k : ('type/num/num' > $o), z : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m (^[t : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (f i t)) P)) k c z) & ((('const/lebesgue/pos_simple_fn_integral' A) m k c z) = (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (('const/lebesgue/pos_simple_fn_integral' A) m (s i) (a i) (x i))) P))))))).
tt('thm/lebesgue/psfis_sum_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (B > (A > 'type/extreal/extreal')), a : (B > 'type/extreal/extreal'), P : (B > $o)]: (((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i P) => (('const/bool/IN' 'type/extreal/extreal') (a i) (('const/lebesgue/psfis' A) m (f i))))) & (('const/pred_set/FINITE' B) P))) => (('const/bool/IN' 'type/extreal/extreal') (('const/extreal/EXTREAL_SUM_IMAGE' B) a P) (('const/lebesgue/psfis' A) m (^[t : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (f i t)) P))))))).
tt('thm/lebesgue/psfis_intro_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), a : (B > (A > $o)), x : (B > 'type/realax/real'), P : (B > $o)]: (((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i P) => (('const/bool/IN' (A > $o)) (a i) (('const/measure/measurable_sets' A) m)))) & ((![i : B]: ((('const/bool/IN' B) i P) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (x i)))) & (('const/pred_set/FINITE' B) P)))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/Normal' (('const/real_sigma/REAL_SUM_IMAGE' B) (^[i : B]: ('const/realax/real_mul' (x i) (('const/measure/measure' A) m (a i)))) P)) (('const/lebesgue/psfis' A) m (^[t : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: ('const/extreal/extreal_mul' ('const/extreal/Normal' (x i)) (('const/measure/indicator_fn' A) (a i) t))) P))))))).
tt('thm/lebesgue/pos_simple_fn_integral_sub_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real'), g : (A > 'type/extreal/extreal'), 's\'' : ('type/num/num' > $o), b : ('type/num/num' > (A > $o)), y : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((![x0 : A]: ('const/extreal/extreal_le' (g x0) (f x0))) & ((![x0 : A]: (~ ((g x0) = 'const/extreal/PosInf'))) & ((('const/measure/pos_simple_fn' A) m f s a x) & (('const/measure/pos_simple_fn' A) m g 's\'' b y))))) => (?['s\'\'' : ('type/num/num' > $o), c : ('type/num/num' > (A > $o)), z : ('type/num/num' > 'type/realax/real')]: ((('const/measure/pos_simple_fn' A) m (^[x0 : A]: ('const/extreal/extreal_sub' (f x0) (g x0))) 's\'\'' c z) & (('const/extreal/extreal_sub' (('const/lebesgue/pos_simple_fn_integral' A) m s a x) (('const/lebesgue/pos_simple_fn_integral' A) m 's\'' b y)) = (('const/lebesgue/pos_simple_fn_integral' A) m 's\'\'' c z))))))).
tt('thm/lebesgue/psfis_sub_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((![x : A]: ('const/extreal/extreal_le' (g x) (f x))) & ((![x : A]: (~ ((g x) = 'const/extreal/PosInf'))) & ((('const/bool/IN' 'type/extreal/extreal') a (('const/lebesgue/psfis' A) m f)) & (('const/bool/IN' 'type/extreal/extreal') b (('const/lebesgue/psfis' A) m g)))))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_sub' a b) (('const/lebesgue/psfis' A) m (^[x : A]: ('const/extreal/extreal_sub' (f x) (g x)))))))).
tt('thm/lebesgue/pos_fn_integral_pos_simple_fn_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & (('const/measure/pos_simple_fn' A) m f s a x)) => ((('const/lebesgue/pos_fn_integral' A) m f) = (('const/lebesgue/pos_simple_fn_integral' A) m s a x))))).
tt('thm/lebesgue/pos_fn_integral_mspace_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) => ((('const/lebesgue/pos_fn_integral' A) m f) = (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/measure/m_space' A) m) x)))))))).
tt('thm/lebesgue/pos_fn_integral_zero_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/measure_space' A) m) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0'))) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/lebesgue/pos_fn_integral_mono_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: ((![x : A]: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) & ('const/extreal/extreal_le' (f x) (g x)))) => ('const/extreal/extreal_le' (('const/lebesgue/pos_fn_integral' A) m f) (('const/lebesgue/pos_fn_integral' A) m g))))).
tt('thm/lebesgue/pos_fn_integral_mono_mspace_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' (g x) (f x)))) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x)))))) => ('const/extreal/extreal_le' (('const/lebesgue/pos_fn_integral' A) m g) (('const/lebesgue/pos_fn_integral' A) m f))))).
tt('thm/lebesgue/pos_fn_integral_pos_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (('const/lebesgue/pos_fn_integral' A) m f))))).
tt('thm/lebesgue/pos_fn_integral_cmul_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/lebesgue/pos_fn_integral' A) m f)))))).
tt('thm/lebesgue/pos_fn_integral_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => ((('const/lebesgue/pos_fn_integral' A) m (('const/measure/indicator_fn' A) s)) = ('const/extreal/Normal' (('const/measure/measure' A) m s)))))).
tt('thm/lebesgue/pos_fn_integral_cmul_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), c : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/measure/indicator_fn' A) s x)))) = ('const/extreal/Normal' ('const/realax/real_mul' c (('const/measure/measure' A) m s))))))).
tt('thm/lebesgue/pos_fn_integral_sum_cmul_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > $o), a : ('type/num/num' > (A > $o)), x : ('type/num/num' > 'type/realax/real')]: (((('const/measure/measure_space' A) m) & ((('const/pred_set/FINITE' 'type/num/num') s) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i s) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (x i)))) & (![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i s) => (('const/bool/IN' (A > $o)) (a i) (('const/measure/measurable_sets' A) m))))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[t : A]: (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' (x i)) (('const/measure/indicator_fn' A) (a i) t))) s))) = ('const/extreal/Normal' (('const/real_sigma/REAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/realax/real_mul' (x i) (('const/measure/measure' A) m (a i)))) s)))))).
tt('thm/lebesgue/lebesgue_monotone_convergence_lemma_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), fi : ('type/num/num' > (A > 'type/extreal/extreal')), g : (A > 'type/extreal/extreal'), 'r\'' : 'type/extreal/extreal']: (((('const/measure/measure_space' A) m) & ((![i : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (fi i) (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))) & ((![x : A]: ('const/extreal/ext_mono_increasing' (^[i : 'type/num/num']: (fi i x)))) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (fi i x)) ('const/pred_set/UNIV' 'type/num/num'))) = (f x)))) & ((('const/bool/IN' 'type/extreal/extreal') 'r\'' (('const/lebesgue/psfis' A) m g)) & ((![x : A]: ('const/extreal/extreal_le' (g x) (f x))) & (![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (fi i x))))))))) => ('const/extreal/extreal_le' 'r\'' ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (fi i))) ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/lebesgue/lebesgue_monotone_convergence_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), fi : ('type/num/num' > (A > 'type/extreal/extreal'))]: (((('const/measure/measure_space' A) m) & ((![i : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (fi i) (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (fi i x))) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((![x : A]: ('const/extreal/ext_mono_increasing' (^[i : 'type/num/num']: (fi i x)))) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (fi i x)) ('const/pred_set/UNIV' 'type/num/num'))) = (f x))))))))) => ((('const/lebesgue/pos_fn_integral' A) m f) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (fi i))) ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/lebesgue/lebesgue_monotone_convergence_subset_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), fi : ('type/num/num' > (A > 'type/extreal/extreal')), A0 : (A > $o)]: (((('const/measure/measure_space' A) m) & ((![i : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (fi i) (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (fi i x))) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (fi i x)) ('const/pred_set/UNIV' 'type/num/num'))) = (f x)))) & ((![x : A]: ('const/extreal/ext_mono_increasing' (^[i : 'type/num/num']: (fi i x)))) & (('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)))))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) A0 x)))) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (fi i x) (('const/measure/indicator_fn' A) A0 x))))) ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/lebesgue/fn_seq_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/fn_seq' A) m f) = (^[n : 'type/num/num', x : A]: ('const/extreal/extreal_add' (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[k : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (('const/measure/indicator_fn' A) (('const/pred_set/GSPEC' A A) (^[x0 : A]: (('const/pair/,' A $o) x0 ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) & (('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (f x0)) & ('const/extreal/extreal_lt' (f x0) ('const/extreal/extreal_div' ('const/extreal/extreal_add' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))))) x))) ('const/pred_set/count' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n))) ('const/extreal/extreal_mul' ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (('const/measure/indicator_fn' A) (('const/pred_set/GSPEC' A A) (^[x0 : A]: (('const/pair/,' A $o) x0 ((('const/bool/IN' A) x0 (('const/measure/m_space' A) m)) & ('const/extreal/extreal_le' ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (f x0)))))) x))))))).
tt('thm/lebesgue/fn_seq_integral_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/lebesgue/fn_seq_integral' A) m f) = (^[n : 'type/num/num']: ('const/extreal/Normal' ('const/realax/real_add' (('const/real_sigma/REAL_SUM_IMAGE' 'type/num/num') (^[k : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' k) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (('const/measure/measure' A) m (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & (('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (f x)) & ('const/extreal/extreal_lt' (f x) ('const/extreal/extreal_div' ('const/extreal/extreal_add' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n))))))))))) ('const/pred_set/count' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (('const/measure/measure' A) m (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ('const/extreal/extreal_le' ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (f x)))))))))))))).
tt('thm/lebesgue/lemma_fn_1_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A, k : 'type/num/num']: (((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ((('const/bool/IN' 'type/num/num') k ('const/pred_set/count' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n))) & (('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (f x)) & ('const/extreal/extreal_lt' (f x) ('const/extreal/extreal_div' ('const/extreal/extreal_add' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))) => ((('const/lebesgue/fn_seq' A) m f n x) = ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))).
tt('thm/lebesgue/lemma_fn_2_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A]: (((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ('const/extreal/extreal_le' ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (f x))) => ((('const/lebesgue/fn_seq' A) m f n x) = ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n))))).
tt('thm/lebesgue/lemma_fn_3_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A]: (((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) => (('const/extreal/extreal_le' ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n) (f x)) | (?[k : 'type/num/num']: ((('const/bool/IN' 'type/num/num') k ('const/pred_set/count' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n))) & (('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) (f x)) & ('const/extreal/extreal_lt' (f x) ('const/extreal/extreal_div' ('const/extreal/extreal_add' ('const/extreal/extreal_of_num' k) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))))))).
tt('thm/lebesgue/lemma_fn_4_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A]: ((~ (('const/bool/IN' A) x (('const/measure/m_space' A) m))) => ((('const/lebesgue/fn_seq' A) m f n x) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/lebesgue/lemma_fn_5_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A]: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (('const/lebesgue/fn_seq' A) m f n x))))).
tt('thm/lebesgue/lemma_fn_mono_increasing_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), x : A]: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) => ('const/extreal/ext_mono_increasing' (^[n : 'type/num/num']: (('const/lebesgue/fn_seq' A) m f n x)))))).
tt('thm/lebesgue/lemma_fn_upper_bounded_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num', x : A]: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) => ('const/extreal/extreal_le' (('const/lebesgue/fn_seq' A) m f n x) (f x))))).
tt('thm/lebesgue/lemma_fn_sup_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), x : A]: (((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (('const/lebesgue/fn_seq' A) m f n x)) ('const/pred_set/UNIV' 'type/num/num'))) = (f x))))).
tt('thm/lebesgue/lemma_fn_in_psfis_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), n : 'type/num/num']: (((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')))) => (('const/bool/IN' 'type/extreal/extreal') (('const/lebesgue/fn_seq_integral' A) m f n) (('const/lebesgue/psfis' A) m (('const/lebesgue/fn_seq' A) m f n)))))).
tt('thm/lebesgue/integral_sequence_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')))) => ((('const/lebesgue/pos_fn_integral' A) m f) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (('const/lebesgue/fn_seq' A) m f i))) ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/lebesgue/measurable_sequence_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))) => ((?[fi : ('type/num/num' > (A > 'type/extreal/extreal')), ri : ('type/num/num' > 'type/extreal/extreal')]: ((![x : A]: ('const/extreal/ext_mono_increasing' (^[i : 'type/num/num']: (fi i x)))) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (fi i x)) ('const/pred_set/UNIV' 'type/num/num'))) = (('const/measure/fn_plus' A) f x)))) & ((![i : 'type/num/num']: (('const/bool/IN' 'type/extreal/extreal') (ri i) (('const/lebesgue/psfis' A) m (fi i)))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' (fi i x) (('const/measure/fn_plus' A) f x))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (fi i x))) & ((('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_plus' A) f)) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (fi i))) ('const/pred_set/UNIV' 'type/num/num')))))))))) & (?[gi : ('type/num/num' > (A > 'type/extreal/extreal')), vi : ('type/num/num' > 'type/extreal/extreal')]: ((![x : A]: ('const/extreal/ext_mono_increasing' (^[i : 'type/num/num']: (gi i x)))) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (gi i x)) ('const/pred_set/UNIV' 'type/num/num'))) = (('const/measure/fn_minus' A) f x)))) & ((![i : 'type/num/num']: (('const/bool/IN' 'type/extreal/extreal') (vi i) (('const/lebesgue/psfis' A) m (gi i)))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' (gi i x) (('const/measure/fn_minus' A) f x))) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (gi i x))) & ((('const/lebesgue/pos_fn_integral' A) m (('const/measure/fn_minus' A) f)) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (gi i))) ('const/pred_set/UNIV' 'type/num/num')))))))))))))).
tt('thm/lebesgue/pos_fn_integral_add_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((![x : A]: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x)))) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_add' (f x) (g x)))) = ('const/extreal/extreal_add' (('const/lebesgue/pos_fn_integral' A) m f) (('const/lebesgue/pos_fn_integral' A) m g)))))).
tt('thm/lebesgue/pos_fn_integral_sum_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (B > (A > 'type/extreal/extreal')), s : (B > $o)]: (((('const/pred_set/FINITE' B) s) & ((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i s) => (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f i x))))) & (![i : B]: ((('const/bool/IN' B) i s) => (('const/bool/IN' (A > 'type/extreal/extreal')) (f i) (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (f i x)) s))) = (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (('const/lebesgue/pos_fn_integral' A) m (f i))) s))))).
tt('thm/lebesgue/pos_fn_integral_disjoint_sets_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : (A > $o), t : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('const/pred_set/DISJOINT' A) s t) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & ((('const/bool/IN' (A > $o)) t (('const/measure/measurable_sets' A) m)) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/pred_set/UNION' A) s t) x)))) = ('const/extreal/extreal_add' (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) s x)))) (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) t x))))))))).
tt('thm/lebesgue/pos_fn_integral_disjoint_sets_sum_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : (B > $o), a : (B > (A > $o))]: (((('const/pred_set/FINITE' B) s) & ((('const/measure/measure_space' A) m) & ((![i : B]: ((('const/bool/IN' B) i s) => (('const/bool/IN' (A > $o)) (a i) (('const/measure/measurable_sets' A) m)))) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((![i : B, j : B]: (((('const/bool/IN' B) i s) & ((('const/bool/IN' B) j s) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (a i) (a j)))) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' B (A > $o)) a s)) x)))) = (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (a i) x))))) s))))).
tt('thm/lebesgue/pos_fn_integral_split_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))))) => ((('const/lebesgue/pos_fn_integral' A) m f) = ('const/extreal/extreal_add' (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) s x)))) (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/pred_set/DIFF' A) (('const/measure/m_space' A) m) s) x))))))))).
tt('thm/lebesgue/pos_fn_integral_cmul_infty_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' 'const/extreal/PosInf' (('const/measure/indicator_fn' A) s x)))) = ('const/extreal/extreal_mul' 'const/extreal/PosInf' ('const/extreal/Normal' (('const/measure/measure' A) m s))))))).
tt('thm/lebesgue/pos_fn_integral_suminf_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : ('type/num/num' > (A > 'type/extreal/extreal'))]: (((('const/measure/measure_space' A) m) & ((![i : 'type/num/num', x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f i x))) & (![i : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (f i) (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel'))))) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/ext_suminf' (^[i : 'type/num/num']: (f i x))))) = ('const/extreal/ext_suminf' (^[i : 'type/num/num']: (('const/lebesgue/pos_fn_integral' A) m (f i)))))))).
tt('thm/lebesgue/integral_pos_fn_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) => ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/pos_fn_integral' A) m f))))).
tt('thm/lebesgue/integrable_pos_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) => ((('const/lebesgue/integrable' A) m f) = ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & (~ ((('const/lebesgue/pos_fn_integral' A) m f) = 'const/extreal/PosInf'))))))).
tt('thm/lebesgue/integrable_infty_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & (![x : A]: ((('const/bool/IN' A) x s) => ((f x) = 'const/extreal/PosInf')))))) => ((('const/measure/measure' A) m s) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/lebesgue/integrable_infty_null_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => (('const/measure/null_set' A) m (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) & ((f x) = 'const/extreal/PosInf'))))))))).
tt('thm/lebesgue/integrable_bounded_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & ((('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_abs' (g x)) (f x)))))) => (('const/lebesgue/integrable' A) m g)))).
tt('thm/lebesgue/integrable_fn_plus_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => (('const/lebesgue/integrable' A) m (('const/measure/fn_plus' A) f))))).
tt('thm/lebesgue/integrable_fn_minus_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => (('const/lebesgue/integrable' A) m (('const/measure/fn_minus' A) f))))).
tt('thm/lebesgue/integrable_const_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), c : 'type/realax/real']: ((('const/measure/measure_space' A) m) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/Normal' c)))))).
tt('thm/lebesgue/integrable_zero_', ax, ![A : $t, B : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), c : B]: ((('const/measure/measure_space' A) m) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/lebesgue/integrable_plus_minus_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/measure/measure_space' A) m) => ((('const/lebesgue/integrable' A) m f) = ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((('const/lebesgue/integrable' A) m (('const/measure/fn_plus' A) f)) & (('const/lebesgue/integrable' A) m (('const/measure/fn_minus' A) f)))))))).
tt('thm/lebesgue/integrable_add_pos_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & ((('const/lebesgue/integrable' A) m g) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x))))))) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_add' (f x) (g x))))))).
tt('thm/lebesgue/integrable_add_lemma_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & (('const/lebesgue/integrable' A) m g))) => ((('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_add' (('const/measure/fn_plus' A) f x) (('const/measure/fn_plus' A) g x)))) & (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_add' (('const/measure/fn_minus' A) f x) (('const/measure/fn_minus' A) g x)))))))).
tt('thm/lebesgue/integrable_add_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f1 : (A > 'type/extreal/extreal'), f2 : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f1) & (('const/lebesgue/integrable' A) m f2))) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_add' (f1 x) (f2 x))))))).
tt('thm/lebesgue/integrable_cmul_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x))))))).
tt('thm/lebesgue/integrable_sub_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f1 : (A > 'type/extreal/extreal'), f2 : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f1) & (('const/lebesgue/integrable' A) m f2))) => (('const/lebesgue/integrable' A) m (^[x : A]: ('const/extreal/extreal_sub' (f1 x) (f2 x))))))).
tt('thm/lebesgue/integrable_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => (('const/lebesgue/integrable' A) m (('const/measure/indicator_fn' A) s))))).
tt('thm/lebesgue/integrable_not_infty_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => (?[g : (A > 'type/extreal/extreal')]: ((('const/lebesgue/integrable' A) m g) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x))) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => (~ ((g x) = 'const/extreal/PosInf')))) & ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/integral' A) m g))))))))).
tt('thm/lebesgue/integrable_not_infty_alt_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => ((('const/lebesgue/integrable' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ((f x) = 'const/extreal/PosInf') ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) & ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/integral' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ((f x) = 'const/extreal/PosInf') ('const/extreal/extreal_of_num' 'const/num/0') (f x))))))))).
tt('thm/lebesgue/integrable_not_infty_alt2_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => ((('const/lebesgue/integrable' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ((f x) = 'const/extreal/PosInf') ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) & ((('const/lebesgue/pos_fn_integral' A) m f) = (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ((f x) = 'const/extreal/PosInf') ('const/extreal/extreal_of_num' 'const/num/0') (f x))))))))).
tt('thm/lebesgue/integrable_not_infty_alt3_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => ((('const/lebesgue/integrable' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (((f x) = 'const/extreal/NegInf') | ((f x) = 'const/extreal/PosInf')) ('const/extreal/extreal_of_num' 'const/num/0') (f x)))) & ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/integral' A) m (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (((f x) = 'const/extreal/NegInf') | ((f x) = 'const/extreal/PosInf')) ('const/extreal/extreal_of_num' 'const/num/0') (f x))))))))).
tt('thm/lebesgue/integral_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => ((('const/lebesgue/integral' A) m (('const/measure/indicator_fn' A) s)) = ('const/extreal/Normal' (('const/measure/measure' A) m s)))))).
tt('thm/lebesgue/integral_add_lemma_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), f1 : (A > 'type/extreal/extreal'), f2 : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & ((('const/lebesgue/integrable' A) m f1) & ((('const/lebesgue/integrable' A) m f2) & ((f = (^[x : A]: ('const/extreal/extreal_sub' (f1 x) (f2 x)))) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f1 x))) & (![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f2 x))))))))) => ((('const/lebesgue/integral' A) m f) = ('const/extreal/extreal_sub' (('const/lebesgue/pos_fn_integral' A) m f1) (('const/lebesgue/pos_fn_integral' A) m f2)))))).
tt('thm/lebesgue/integral_add_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/lebesgue/integrable' A) m f) & (('const/lebesgue/integrable' A) m g))) => ((('const/lebesgue/integral' A) m (^[x : A]: ('const/extreal/extreal_add' (f x) (g x)))) = ('const/extreal/extreal_add' (('const/lebesgue/integral' A) m f) (('const/lebesgue/integral' A) m g)))))).
tt('thm/lebesgue/integral_cmul_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (((('const/measure/measure_space' A) m) & (('const/lebesgue/integrable' A) m f)) => ((('const/lebesgue/integral' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/lebesgue/integral' A) m f)))))).
tt('thm/lebesgue/integral_cmul_indicator_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), c : 'type/realax/real']: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))) => ((('const/lebesgue/integral' A) m (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/measure/indicator_fn' A) s x)))) = ('const/extreal/Normal' ('const/realax/real_mul' c (('const/measure/measure' A) m s))))))).
tt('thm/lebesgue/integral_zero_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/measure_space' A) m) => ((('const/lebesgue/integral' A) m (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0'))) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/lebesgue/integral_mspace_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: ((('const/measure/measure_space' A) m) => ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/measure/m_space' A) m) x)))))))).
tt('thm/lebesgue/integral_mono_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f1 : (A > 'type/extreal/extreal'), f2 : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (![t : A]: ((('const/bool/IN' A) t (('const/measure/m_space' A) m)) => ('const/extreal/extreal_le' (f1 t) (f2 t))))) => ('const/extreal/extreal_le' (('const/lebesgue/integral' A) m f1) (('const/lebesgue/integral' A) m f2))))).
tt('thm/lebesgue/finite_space_integral_reduce_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ((~ ((f x) = 'const/extreal/NegInf')) & (~ ((f x) = 'const/extreal/PosInf'))))) & (('const/pred_set/FINITE' A) (('const/measure/m_space' A) m))))) => ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/finite_space_integral' A) m f))))).
tt('thm/lebesgue/finite_support_integral_reduce_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ((~ ((f x) = 'const/extreal/NegInf')) & (~ ((f x) = 'const/extreal/PosInf'))))) & (('const/pred_set/FINITE' 'type/extreal/extreal') (('const/pred_set/IMAGE' A 'type/extreal/extreal') f (('const/measure/m_space' A) m)))))) => ((('const/lebesgue/integral' A) m f) = (('const/lebesgue/finite_space_integral' A) m f))))).
tt('thm/lebesgue/finite_space_POW_integral_reduce_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > 'type/extreal/extreal')]: (((('const/measure/measure_space' A) m) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m)) = (('const/measure/measurable_sets' A) m)) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m)) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/m_space' A) m)) => ((~ ((f x) = 'const/extreal/NegInf')) & (~ ((f x) = 'const/extreal/PosInf')))))))) => ((('const/lebesgue/integral' A) m f) = (('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_mul' (f x) ('const/extreal/Normal' (('const/measure/measure' A) m (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))))) (('const/measure/m_space' A) m)))))).
tt('thm/lebesgue/finite_POW_prod_measure_reduce_', ax, ![B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m0) & ((('const/measure/measure_space' B) m1) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m0)) & ((('const/pred_set/FINITE' B) (('const/measure/m_space' B) m1)) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m0)) = (('const/measure/measurable_sets' A) m0)) & ((('const/pred_set/POW' B) (('const/measure/m_space' B) m1)) = (('const/measure/measurable_sets' B) m1))))))) => (![a0 : (A > $o), a1 : (B > $o)]: (((('const/bool/IN' (A > $o)) a0 (('const/measure/measurable_sets' A) m0)) & (('const/bool/IN' (B > $o)) a1 (('const/measure/measurable_sets' B) m1))) => ((('const/lebesgue/prod_measure' A B) m0 m1 (('const/pred_set/CROSS' A B) a0 a1)) = ('const/realax/real_mul' (('const/measure/measure' A) m0 a0) (('const/measure/measure' B) m1 a1)))))))).
tt('thm/lebesgue/measure_space_finite_prod_measure_POW1_', ax, ![B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m0) & ((('const/measure/measure_space' B) m1) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m0)) & ((('const/pred_set/FINITE' B) (('const/measure/m_space' B) m1)) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m0)) = (('const/measure/measurable_sets' A) m0)) & ((('const/pred_set/POW' B) (('const/measure/m_space' B) m1)) = (('const/measure/measurable_sets' B) m1))))))) => (('const/measure/measure_space' ('type/pair/prod' A B)) (('const/lebesgue/prod_measure_space' A B) m0 m1))))).
tt('thm/lebesgue/measure_space_finite_prod_measure_POW2_', ax, ![B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m0) & ((('const/measure/measure_space' B) m1) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m0)) & ((('const/pred_set/FINITE' B) (('const/measure/m_space' B) m1)) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m0)) = (('const/measure/measurable_sets' A) m0)) & ((('const/pred_set/POW' B) (('const/measure/m_space' B) m1)) = (('const/measure/measurable_sets' B) m1))))))) => (('const/measure/measure_space' ('type/pair/prod' A B)) (('const/pair/,' (('type/pair/prod' A B) > $o) ('type/pair/prod' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A B) (('const/measure/m_space' A) m0) (('const/measure/m_space' B) m1)) (('const/pair/,' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real')) (('const/pred_set/POW' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) (('const/measure/m_space' A) m0) (('const/measure/m_space' B) m1))) (('const/lebesgue/prod_measure' A B) m0 m1))))))).
tt('thm/lebesgue/finite_prod_measure_space_POW_', ax, ![B : $t, A : $t]: (![s1 : (A > $o), s2 : (B > $o), u : ((A > $o) > 'type/realax/real'), v : ((B > $o) > 'type/realax/real')]: (((('const/pred_set/FINITE' A) s1) & (('const/pred_set/FINITE' B) s2)) => ((('const/lebesgue/prod_measure_space' A B) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s1 (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) s1) u)) (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) s2 (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) (('const/pred_set/POW' B) s2) v))) = (('const/pair/,' (('type/pair/prod' A B) > $o) ('type/pair/prod' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A B) s1 s2) (('const/pair/,' ((('type/pair/prod' A B) > $o) > $o) ((('type/pair/prod' A B) > $o) > 'type/realax/real')) (('const/pred_set/POW' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s1 s2)) (('const/lebesgue/prod_measure' A B) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s1 (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) s1) u)) (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) s2 (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) (('const/pred_set/POW' B) s2) v))))))))).
tt('thm/lebesgue/finite_POW_prod_measure_reduce3_', ax, ![C : $t, B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m0) & ((('const/measure/measure_space' B) m1) & ((('const/measure/measure_space' C) m2) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m0)) & ((('const/pred_set/FINITE' B) (('const/measure/m_space' B) m1)) & ((('const/pred_set/FINITE' C) (('const/measure/m_space' C) m2)) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m0)) = (('const/measure/measurable_sets' A) m0)) & (((('const/pred_set/POW' B) (('const/measure/m_space' B) m1)) = (('const/measure/measurable_sets' B) m1)) & ((('const/pred_set/POW' C) (('const/measure/m_space' C) m2)) = (('const/measure/measurable_sets' C) m2)))))))))) => (![a0 : (A > $o), a1 : (B > $o), a2 : (C > $o)]: (((('const/bool/IN' (A > $o)) a0 (('const/measure/measurable_sets' A) m0)) & ((('const/bool/IN' (B > $o)) a1 (('const/measure/measurable_sets' B) m1)) & (('const/bool/IN' (C > $o)) a2 (('const/measure/measurable_sets' C) m2)))) => ((('const/lebesgue/prod_measure3' A B C) m0 m1 m2 (('const/pred_set/CROSS' A ('type/pair/prod' B C)) a0 (('const/pred_set/CROSS' B C) a1 a2))) = ('const/realax/real_mul' ('const/realax/real_mul' (('const/measure/measure' A) m0 a0) (('const/measure/measure' B) m1 a1)) (('const/measure/measure' C) m2 a2)))))))).
tt('thm/lebesgue/measure_space_finite_prod_measure_POW3_', ax, ![C : $t, B : $t, A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m0) & ((('const/measure/measure_space' B) m1) & ((('const/measure/measure_space' C) m2) & ((('const/pred_set/FINITE' A) (('const/measure/m_space' A) m0)) & ((('const/pred_set/FINITE' B) (('const/measure/m_space' B) m1)) & ((('const/pred_set/FINITE' C) (('const/measure/m_space' C) m2)) & (((('const/pred_set/POW' A) (('const/measure/m_space' A) m0)) = (('const/measure/measurable_sets' A) m0)) & (((('const/pred_set/POW' B) (('const/measure/m_space' B) m1)) = (('const/measure/measurable_sets' B) m1)) & ((('const/pred_set/POW' C) (('const/measure/m_space' C) m2)) = (('const/measure/measurable_sets' C) m2)))))))))) => (('const/measure/measure_space' ('type/pair/prod' A ('type/pair/prod' B C))) (('const/pair/,' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) ('type/pair/prod' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) (('const/measure/m_space' A) m0) (('const/pred_set/CROSS' B C) (('const/measure/m_space' B) m1) (('const/measure/m_space' C) m2))) (('const/pair/,' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real')) (('const/pred_set/POW' ('type/pair/prod' A ('type/pair/prod' B C))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) (('const/measure/m_space' A) m0) (('const/pred_set/CROSS' B C) (('const/measure/m_space' B) m1) (('const/measure/m_space' C) m2)))) (('const/lebesgue/prod_measure3' A B C) m0 m1 m2))))))).
tt('thm/lebesgue/finite_prod_measure_space_POW3_', ax, ![C : $t, B : $t, A : $t]: (![s1 : (A > $o), s2 : (B > $o), s3 : (C > $o), u : ((A > $o) > 'type/realax/real'), v : ((B > $o) > 'type/realax/real'), w : ((C > $o) > 'type/realax/real')]: (((('const/pred_set/FINITE' A) s1) & ((('const/pred_set/FINITE' B) s2) & (('const/pred_set/FINITE' C) s3))) => ((('const/lebesgue/prod_measure_space3' A B C) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s1 (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) s1) u)) (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) s2 (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) (('const/pred_set/POW' B) s2) v)) (('const/pair/,' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real'))) s3 (('const/pair/,' ((C > $o) > $o) ((C > $o) > 'type/realax/real')) (('const/pred_set/POW' C) s3) w))) = (('const/pair/,' (('type/pair/prod' A ('type/pair/prod' B C)) > $o) ('type/pair/prod' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real'))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) s1 (('const/pred_set/CROSS' B C) s2 s3)) (('const/pair/,' ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > $o) ((('type/pair/prod' A ('type/pair/prod' B C)) > $o) > 'type/realax/real')) (('const/pred_set/POW' ('type/pair/prod' A ('type/pair/prod' B C))) (('const/pred_set/CROSS' A ('type/pair/prod' B C)) s1 (('const/pred_set/CROSS' B C) s2 s3))) (('const/lebesgue/prod_measure3' A B C) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s1 (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) s1) u)) (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) s2 (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) (('const/pred_set/POW' B) s2) v)) (('const/pair/,' (C > $o) ('type/pair/prod' ((C > $o) > $o) ((C > $o) > 'type/realax/real'))) s3 (('const/pair/,' ((C > $o) > $o) ((C > $o) > 'type/realax/real')) (('const/pred_set/POW' C) s3) w))))))))).
tt('thm/lebesgue/seq_sup_def_0', def, (![P : ('type/extreal/extreal' > $o)]: (('const/lebesgue/seq_sup' P 'const/num/0') = (('const/min/@' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r P) & ('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' r ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/lebesgue/seq_sup_def_e1', def, (![P : ('type/extreal/extreal' > $o), n : 'type/num/num']: (('const/lebesgue/seq_sup' P ('const/num/SUC' n)) = (('const/min/@' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r P) & (('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' r ('const/extreal/Normal' ('const/real/pow' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/num/SUC' n))))) & (('const/extreal/extreal_lt' ('const/lebesgue/seq_sup' P n) r) & ('const/extreal/extreal_lt' r ('const/extreal/extreal_sup' P)))))))))).
tt('thm/lebesgue/seq_sup_def_compute_0', ax, (![P : ('type/extreal/extreal' > $o)]: (('const/lebesgue/seq_sup' P 'const/num/0') = (('const/min/@' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r P) & ('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' r ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/lebesgue/seq_sup_def_compute_1', ax, (![P : ('type/extreal/extreal' > $o), n : 'type/num/num']: (('const/lebesgue/seq_sup' P ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = (('const/min/@' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r P) & (('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' r ('const/extreal/Normal' ('const/real/pow' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))) & (('const/extreal/extreal_lt' ('const/lebesgue/seq_sup' P ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) r) & ('const/extreal/extreal_lt' r ('const/extreal/extreal_sup' P)))))))))).
tt('thm/lebesgue/seq_sup_def_compute_e2', ax, (![P : ('type/extreal/extreal' > $o), n : 'type/num/num']: (('const/lebesgue/seq_sup' P ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = (('const/min/@' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r P) & (('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' r ('const/extreal/Normal' ('const/real/pow' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))) & (('const/extreal/extreal_lt' ('const/lebesgue/seq_sup' P ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) r) & ('const/extreal/extreal_lt' r ('const/extreal/extreal_sup' P)))))))))).
tt('thm/lebesgue/EXTREAL_SUP_SEQ_', ax, (![P : ('type/extreal/extreal' > $o)]: (((?[x : 'type/extreal/extreal']: (P x)) & (?[z : 'type/extreal/extreal']: ((~ (z = 'const/extreal/PosInf')) & (![x : 'type/extreal/extreal']: ((P x) => ('const/extreal/extreal_le' x z)))))) => (?[x : ('type/num/num' > 'type/extreal/extreal')]: ((![n : 'type/num/num']: (('const/bool/IN' 'type/extreal/extreal') (x n) P)) & ((![n : 'type/num/num']: ('const/extreal/extreal_le' (x n) (x ('const/num/SUC' n)))) & (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') x ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_sup' P)))))))).
tt('thm/lebesgue/EXTREAL_SUP_FUN_SEQ_IMAGE_', ax, ![A : $t]: (![P : ('type/extreal/extreal' > $o), 'P\'' : ((A > 'type/extreal/extreal') > $o), f : ((A > 'type/extreal/extreal') > 'type/extreal/extreal')]: (((?[x : 'type/extreal/extreal']: (P x)) & ((?[z : 'type/extreal/extreal']: ((~ (z = 'const/extreal/PosInf')) & (![x : 'type/extreal/extreal']: ((P x) => ('const/extreal/extreal_le' x z))))) & (P = (('const/pred_set/IMAGE' (A > 'type/extreal/extreal') 'type/extreal/extreal') f 'P\'')))) => (?[g : ('type/num/num' > (A > 'type/extreal/extreal'))]: ((![n : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (g n) 'P\'')) & (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (f (g n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_sup' P))))))).
tt('thm/lebesgue/max_fn_seq_def_0', def, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), x : A]: ((('const/lebesgue/max_fn_seq' A) g 'const/num/0' x) = (g 'const/num/0' x)))).
tt('thm/lebesgue/max_fn_seq_def_e1', def, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), n : 'type/num/num', x : A]: ((('const/lebesgue/max_fn_seq' A) g ('const/num/SUC' n) x) = ('const/extreal/extreal_max' (('const/lebesgue/max_fn_seq' A) g n x) (g ('const/num/SUC' n) x))))).
tt('thm/lebesgue/max_fn_seq_def_compute_0', ax, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), x : A]: ((('const/lebesgue/max_fn_seq' A) g 'const/num/0' x) = (g 'const/num/0' x)))).
tt('thm/lebesgue/max_fn_seq_def_compute_1', ax, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), n : 'type/num/num', x : A]: ((('const/lebesgue/max_fn_seq' A) g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) x) = ('const/extreal/extreal_max' (('const/lebesgue/max_fn_seq' A) g ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) (g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) x))))).
tt('thm/lebesgue/max_fn_seq_def_compute_e2', ax, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), n : 'type/num/num', x : A]: ((('const/lebesgue/max_fn_seq' A) g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) x) = ('const/extreal/extreal_max' (('const/lebesgue/max_fn_seq' A) g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) x) (g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) x))))).
tt('thm/lebesgue/max_fn_seq_mono_', ax, ![A : $t]: (![g : ('type/num/num' > (A > 'type/extreal/extreal')), n : 'type/num/num', x : A]: ('const/extreal/extreal_le' (('const/lebesgue/max_fn_seq' A) g n x) (('const/lebesgue/max_fn_seq' A) g ('const/num/SUC' n) x)))).
tt('thm/lebesgue/EXTREAL_SUP_FUN_SEQ_MONO_IMAGE_', ax, ![A : $t]: (![f : ((A > 'type/extreal/extreal') > 'type/extreal/extreal'), P : ('type/extreal/extreal' > $o), 'P\'' : ((A > 'type/extreal/extreal') > $o)]: (((?[x : 'type/extreal/extreal']: (P x)) & ((?[z : 'type/extreal/extreal']: ((~ (z = 'const/extreal/PosInf')) & (![x : 'type/extreal/extreal']: ((P x) => ('const/extreal/extreal_le' x z))))) & ((P = (('const/pred_set/IMAGE' (A > 'type/extreal/extreal') 'type/extreal/extreal') f 'P\'')) & ((![g1 : (A > 'type/extreal/extreal'), g2 : (A > 'type/extreal/extreal')]: (((('const/bool/IN' (A > 'type/extreal/extreal')) g1 'P\'') & ((('const/bool/IN' (A > 'type/extreal/extreal')) g2 'P\'') & (![x : A]: ('const/extreal/extreal_le' (g1 x) (g2 x))))) => ('const/extreal/extreal_le' (f g1) (f g2)))) & (![g1 : (A > 'type/extreal/extreal'), g2 : (A > 'type/extreal/extreal')]: (((('const/bool/IN' (A > 'type/extreal/extreal')) g1 'P\'') & (('const/bool/IN' (A > 'type/extreal/extreal')) g2 'P\'')) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_max' (g1 x) (g2 x))) 'P\''))))))) => (?[g : ('type/num/num' > (A > 'type/extreal/extreal'))]: ((![n : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (g n) 'P\'')) & ((![x : A, n : 'type/num/num']: ('const/extreal/extreal_le' (g n x) (g ('const/num/SUC' n) x))) & (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (f (g n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_sup' P)))))))).
tt('thm/lebesgue/signed_measure_space_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/lebesgue/signed_measure_space' A) m) = ((('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & (('const/measure/countably_additive' A) m))))).
tt('thm/lebesgue/negative_set_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), A0 : (A > $o)]: ((('const/lebesgue/negative_set' A) m A0) = ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) & (![s : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & (('const/pred_set/SUBSET' A) s A0)) => ('const/real/real_lte' (('const/measure/measure' A) m s) ('const/real/real_of_num' 'const/num/0')))))))).
tt('thm/lebesgue/RADON_F_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/lebesgue/RADON_F' A) m v) = (('const/pred_set/GSPEC' (A > 'type/extreal/extreal') (A > 'type/extreal/extreal')) (^[f : (A > 'type/extreal/extreal')]: (('const/pair/,' (A > 'type/extreal/extreal') $o) f ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & (![A0 : (A > $o)]: ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) => ('const/extreal/extreal_le' (('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) A0 x)))) ('const/extreal/Normal' (('const/measure/measure' A) v A0))))))))))))).
tt('thm/lebesgue/RADON_F_integrals_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/lebesgue/RADON_F_integrals' A) m v) = (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[r : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) r (?[f : (A > 'type/extreal/extreal')]: ((r = (('const/lebesgue/pos_fn_integral' A) m f)) & (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/lebesgue/RADON_F' A) m v)))))))))).
tt('thm/lebesgue/measure_absolutely_continuous_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/lebesgue/measure_absolutely_continuous' A) m v) = (![A0 : (A > $o)]: (((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) & ((('const/measure/measure' A) v A0) = ('const/real/real_of_num' 'const/num/0'))) => ((('const/measure/measure' A) m A0) = ('const/real/real_of_num' 'const/num/0'))))))).
tt('thm/lebesgue/lemma_radon_max_in_F_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & ((('const/measure/measure_space' A) v) & (((('const/measure/m_space' A) v) = (('const/measure/m_space' A) m)) & (((('const/measure/measurable_sets' A) v) = (('const/measure/measurable_sets' A) m)) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/lebesgue/RADON_F' A) m v)) & (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/lebesgue/RADON_F' A) m v))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_max' (f x) (g x))) (('const/lebesgue/RADON_F' A) m v))))).
tt('thm/lebesgue/lemma_radon_seq_conv_sup_', ax, ![B : $t, A : $t]: (![f : A, m : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), v : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' B) m) & ((('const/measure/measure_space' B) v) & (((('const/measure/m_space' B) v) = (('const/measure/m_space' B) m)) & ((('const/measure/measurable_sets' B) v) = (('const/measure/measurable_sets' B) m))))) => (?[f_n : ('type/num/num' > (B > 'type/extreal/extreal'))]: ((![n : 'type/num/num']: (('const/bool/IN' (B > 'type/extreal/extreal')) (f_n n) (('const/lebesgue/RADON_F' B) m v))) & ((![x : B, n : 'type/num/num']: ('const/extreal/extreal_le' (f_n n x) (f_n ('const/num/SUC' n) x))) & (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (('const/lebesgue/pos_fn_integral' B) m (f_n n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_sup' (('const/lebesgue/RADON_F_integrals' B) m v))))))))).
tt('thm/lebesgue/RN_lemma1_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), e : 'type/realax/real']: (((('const/measure/measure_space' A) m) & ((('const/measure/measure_space' A) v) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) & (((('const/measure/m_space' A) v) = (('const/measure/m_space' A) m)) & ((('const/measure/measurable_sets' A) v) = (('const/measure/measurable_sets' A) m)))))) => (?[A0 : (A > $o)]: ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) & (('const/real/real_lte' ('const/real/real_sub' (('const/measure/measure' A) m (('const/measure/m_space' A) m)) (('const/measure/measure' A) v (('const/measure/m_space' A) m))) ('const/real/real_sub' (('const/measure/measure' A) m A0) (('const/measure/measure' A) v A0))) & (![B : (A > $o)]: (((('const/bool/IN' (A > $o)) B (('const/measure/measurable_sets' A) m)) & (('const/pred_set/SUBSET' A) B A0)) => ('const/realax/real_lt' ('const/realax/real_neg' e) ('const/real/real_sub' (('const/measure/measure' A) m B) (('const/measure/measure' A) v B))))))))))).
tt('thm/lebesgue/RN_lemma2_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & ((('const/measure/measure_space' A) v) & (((('const/measure/m_space' A) v) = (('const/measure/m_space' A) m)) & ((('const/measure/measurable_sets' A) v) = (('const/measure/measurable_sets' A) m))))) => (?[A0 : (A > $o)]: ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) & (('const/real/real_lte' ('const/real/real_sub' (('const/measure/measure' A) m (('const/measure/m_space' A) m)) (('const/measure/measure' A) v (('const/measure/m_space' A) m))) ('const/real/real_sub' (('const/measure/measure' A) m A0) (('const/measure/measure' A) v A0))) & (![B : (A > $o)]: (((('const/bool/IN' (A > $o)) B (('const/measure/measurable_sets' A) m)) & (('const/pred_set/SUBSET' A) B A0)) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/real_sub' (('const/measure/measure' A) m B) (('const/measure/measure' A) v B))))))))))).
tt('thm/lebesgue/Radon_Nikodym_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & ((('const/measure/measure_space' A) v) & (((('const/measure/m_space' A) v) = (('const/measure/m_space' A) m)) & (((('const/measure/measurable_sets' A) v) = (('const/measure/measurable_sets' A) m)) & (('const/lebesgue/measure_absolutely_continuous' A) v m))))) => (?[f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & (![A0 : (A > $o)]: ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) A0 x)))) = ('const/extreal/Normal' (('const/measure/measure' A) v A0))))))))))).
tt('thm/lebesgue/Radon_Nikodym2_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), v : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & ((('const/measure/measure_space' A) v) & (((('const/measure/m_space' A) v) = (('const/measure/m_space' A) m)) & (((('const/measure/measurable_sets' A) v) = (('const/measure/measurable_sets' A) m)) & (('const/lebesgue/measure_absolutely_continuous' A) v m))))) => (?[f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) 'const/measure/Borel')) & ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))) & ((![x : A]: (~ ((f x) = 'const/extreal/PosInf'))) & (![A0 : (A > $o)]: ((('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m)) => ((('const/lebesgue/pos_fn_integral' A) m (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) A0 x)))) = ('const/extreal/Normal' (('const/measure/measure' A) v A0)))))))))))).
