tt('const/measure/Borel', ty, ('type/pair/prod' ('type/extreal/extreal' > $o) (('type/extreal/extreal' > $o) > $o))).
tt('const/measure/additive', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/algebra', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > $o)).
tt('const/measure/closed_cdi', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > $o)).
tt('const/measure/countably_additive', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/countably_subadditive', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/fn_abs', ty, ![A : $t]: ((A > 'type/extreal/extreal') > (A > 'type/extreal/extreal'))).
tt('const/measure/fn_minus', ty, ![A : $t]: ((A > 'type/extreal/extreal') > (A > 'type/extreal/extreal'))).
tt('const/measure/fn_plus', ty, ![A : $t]: ((A > 'type/extreal/extreal') > (A > 'type/extreal/extreal'))).
tt('const/measure/increasing', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/indicator_fn', ty, ![A : $t]: ((A > $o) > (A > 'type/extreal/extreal'))).
tt('const/measure/inf_measure', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > $o) > 'type/realax/real'))).
tt('const/measure/lambda_system', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > (((A > $o) > 'type/realax/real') > ((A > $o) > $o)))).
tt('const/measure/m_space', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > (A > $o))).
tt('const/measure/measurable', ty, ![A : $t, B : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > (('type/pair/prod' (B > $o) ((B > $o) > $o)) > ((A > B) > $o)))).
tt('const/measure/measurable_sets', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > $o) > $o))).
tt('const/measure/measure', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > ((A > $o) > 'type/realax/real'))).
tt('const/measure/measure_preserving', 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'))) > ((A > B) > $o)))).
tt('const/measure/measure_space', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/null_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/measure/outer_measure_space', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/pos_simple_fn', 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' > $o) > (('type/num/num' > (A > $o)) > (('type/num/num' > 'type/realax/real') > $o)))))).
tt('const/measure/positive', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/sigma', ty, ![A : $t]: ((A > $o) > (((A > $o) > $o) > ('type/pair/prod' (A > $o) ((A > $o) > $o))))).
tt('const/measure/sigma_algebra', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > $o)).
tt('const/measure/smallest_closed_cdi', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > ('type/pair/prod' (A > $o) ((A > $o) > $o)))).
tt('const/measure/space', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > (A > $o))).
tt('const/measure/subadditive', ty, ![A : $t]: (('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) > $o)).
tt('const/measure/subset_class', ty, ![A : $t]: ((A > $o) > (((A > $o) > $o) > $o))).
tt('const/measure/subsets', ty, ![A : $t]: (('type/pair/prod' (A > $o) ((A > $o) > $o)) > ((A > $o) > $o))).
tt('thm/measure/space_def_', def, ![A : $t]: (![x : (A > $o), y : ((A > $o) > $o)]: ((('const/measure/space' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) x y)) = x))).
tt('thm/measure/subsets_def_', def, ![A : $t]: (![x : (A > $o), y : ((A > $o) > $o)]: ((('const/measure/subsets' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) x y)) = y))).
tt('thm/measure/subset_class_def_', def, ![A : $t]: (![sp : (A > $o), sts : ((A > $o) > $o)]: ((('const/measure/subset_class' A) sp sts) = (![x : (A > $o)]: ((('const/bool/IN' (A > $o)) x sts) => (('const/pred_set/SUBSET' A) x sp)))))).
tt('thm/measure/algebra_def_', def, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) = ((('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a)))) & (![s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/UNION' A) s t) (('const/measure/subsets' A) a)))))))))).
tt('thm/measure/sigma_algebra_def_', def, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/algebra' A) a) & (![c : ((A > $o) > $o)]: (((('const/util_prob/countable' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/sigma_def_', def, ![A : $t]: (![sp : (A > $o), st : ((A > $o) > $o)]: ((('const/measure/sigma' A) sp st) = (('const/pair/,' (A > $o) ((A > $o) > $o)) sp (('const/pred_set/BIGINTER' (A > $o)) (('const/pred_set/GSPEC' ((A > $o) > $o) ((A > $o) > $o)) (^[s : ((A > $o) > $o)]: (('const/pair/,' ((A > $o) > $o) $o) s ((('const/pred_set/SUBSET' (A > $o)) st s) & (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp s))))))))))).
tt('thm/measure/m_space_def_', def, ![A : $t]: (![sp : (A > $o), sts : ((A > $o) > $o), mu : ((A > $o) > 'type/realax/real')]: ((('const/measure/m_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) sp (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) sts mu))) = sp))).
tt('thm/measure/measurable_sets_def_', def, ![A : $t]: (![sp : (A > $o), sts : ((A > $o) > $o), mu : ((A > $o) > 'type/realax/real')]: ((('const/measure/measurable_sets' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) sp (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) sts mu))) = sts))).
tt('thm/measure/measure_def_', def, ![A : $t]: (![sp : (A > $o), sts : ((A > $o) > $o), mu : ((A > $o) > 'type/realax/real')]: ((('const/measure/measure' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) sp (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) sts mu))) = mu))).
tt('thm/measure/positive_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/positive' A) m) = (((('const/measure/measure' A) m ('const/pred_set/EMPTY' A)) = ('const/real/real_of_num' 'const/num/0')) & (![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (('const/measure/measure' A) m s)))))))).
tt('thm/measure/additive_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/additive' A) m) = (![s : (A > $o), t : (A > $o)]: (((('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/pred_set/DISJOINT' A) s t))) => ((('const/measure/measure' A) m (('const/pred_set/UNION' A) s t)) = ('const/realax/real_add' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))))).
tt('thm/measure/countably_additive_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/countably_additive' A) m) = (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/measurable_sets' A) m)))) => ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))))))))).
tt('thm/measure/subadditive_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/subadditive' A) m) = (![s : (A > $o), t : (A > $o)]: (((('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/real/real_lte' (('const/measure/measure' A) m (('const/pred_set/UNION' A) s t)) ('const/realax/real_add' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))))).
tt('thm/measure/countably_subadditive_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/countably_subadditive' A) m) = (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/measurable_sets' A) m)) & ('const/seq/summable' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f)))) => ('const/real/real_lte' (('const/measure/measure' A) m (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) ('const/seq/suminf' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f)))))))).
tt('thm/measure/increasing_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/increasing' A) m) = (![s : (A > $o), t : (A > $o)]: (((('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/pred_set/SUBSET' A) s t))) => ('const/real/real_lte' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t))))))).
tt('thm/measure/measure_space_def_', def, ![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/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/positive' A) m) & (('const/measure/countably_additive' A) m)))))).
tt('thm/measure/lambda_system_def_', def, ![A : $t]: (![gen : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: ((('const/measure/lambda_system' A) gen lam) = (('const/pred_set/GSPEC' (A > $o) (A > $o)) (^[l : (A > $o)]: (('const/pair/,' (A > $o) $o) l ((('const/bool/IN' (A > $o)) l (('const/measure/subsets' A) gen)) & (![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) gen)) => (('const/realax/real_add' (lam (('const/pred_set/INTER' A) l s)) (lam (('const/pred_set/INTER' A) (('const/pred_set/DIFF' A) (('const/measure/space' A) gen) l) s))) = (lam s))))))))))).
tt('thm/measure/outer_measure_space_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/outer_measure_space' A) m) = ((('const/measure/positive' A) m) & ((('const/measure/increasing' A) m) & (('const/measure/countably_subadditive' A) m)))))).
tt('thm/measure/inf_measure_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: ((('const/measure/inf_measure' A) m s) = ('const/real/inf' (('const/pred_set/GSPEC' 'type/realax/real' 'type/realax/real') (^[r : 'type/realax/real']: (('const/pair/,' 'type/realax/real' $o) r (?[f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & ((('const/pred_set/SUBSET' A) s (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) r)))))))))))).
tt('thm/measure/closed_cdi_def_', def, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/closed_cdi' A) p) = ((('const/measure/subset_class' A) (('const/measure/space' A) p) (('const/measure/subsets' A) p)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) p)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) p) s) (('const/measure/subsets' A) p)))) & ((![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) p))) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) p)))) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) p))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) p)))))))))).
tt('thm/measure/smallest_closed_cdi_def_', def, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/smallest_closed_cdi' A) a) = (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/space' A) a) (('const/pred_set/BIGINTER' (A > $o)) (('const/pred_set/GSPEC' ((A > $o) > $o) ((A > $o) > $o)) (^[b : ((A > $o) > $o)]: (('const/pair/,' ((A > $o) > $o) $o) b ((('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) a) b) & (('const/measure/closed_cdi' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/space' A) a) b))))))))))).
tt('thm/measure/measurable_def_', def, ![A : $t, B : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o))]: ((('const/measure/measurable' A B) a b) = (('const/pred_set/GSPEC' (A > B) (A > B)) (^[f : (A > B)]: (('const/pair/,' (A > B) $o) f ((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))))))))))).
tt('thm/measure/measure_preserving_def_', def, ![B : $t, A : $t]: (![m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: ((('const/measure/measure_preserving' A B) m1 m2) = (('const/pred_set/GSPEC' (A > B) (A > B)) (^[f : (A > B)]: (('const/pair/,' (A > B) $o) f ((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m1) (('const/measure/measurable_sets' A) m1)) (('const/pair/,' (B > $o) ((B > $o) > $o)) (('const/measure/m_space' B) m2) (('const/measure/measurable_sets' B) m2)))) & ((('const/measure/measure_space' A) m1) & ((('const/measure/measure_space' B) m2) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/measurable_sets' B) m2)) => ((('const/measure/measure' A) m1 (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/m_space' A) m1))) = (('const/measure/measure' B) m2 s))))))))))))).
tt('thm/measure/indicator_fn_def_', def, ![A : $t]: (![s : (A > $o)]: ((('const/measure/indicator_fn' A) s) = (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (('const/bool/IN' A) x s) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/measure/pos_simple_fn_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'), 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) = ((![t : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f t))) & ((![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' (x i)) (('const/measure/indicator_fn' A) (a i) t))) s)))) & ((![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/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', j : 'type/num/num']: (((('const/bool/IN' 'type/num/num') i s) & ((('const/bool/IN' 'type/num/num') j s) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (a i) (a j)))) & ((('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) a s)) = (('const/measure/m_space' A) m))))))))))).
tt('thm/measure/null_set_def_', def, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o)]: ((('const/measure/null_set' A) m s) = ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & ((('const/measure/measure' A) m s) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/measure/SPACE_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) = a))).
tt('thm/measure/ALGEBRA_ALT_INTER_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) = ((('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a)))) & (![s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) s t) (('const/measure/subsets' A) a)))))))))).
tt('thm/measure/ALGEBRA_EMPTY_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) => (('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_SPACE_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) => (('const/bool/IN' (A > $o)) (('const/measure/space' A) a) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_COMPL_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o)]: (((('const/measure/algebra' A) a) & (('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_UNION_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o), t : (A > $o)]: (((('const/measure/algebra' A) a) & ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/UNION' A) s t) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_INTER_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o), t : (A > $o)]: (((('const/measure/algebra' A) a) & ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) s t) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_DIFF_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o), t : (A > $o)]: (((('const/measure/algebra' A) a) & ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) s t) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_FINITE_UNION_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), c : ((A > $o) > $o)]: (((('const/measure/algebra' A) a) & ((('const/pred_set/FINITE' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) (('const/measure/subsets' A) a))))).
tt('thm/measure/ALGEBRA_INTER_SPACE_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o)]: (((('const/measure/algebra' A) a) & (('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a))) => (((('const/pred_set/INTER' A) (('const/measure/space' A) a) s) = s) & ((('const/pred_set/INTER' A) s (('const/measure/space' A) a)) = s))))).
tt('thm/measure/LAMBDA_SYSTEM_EMPTY_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: (((('const/measure/algebra' A) g0) & (('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam)))) => (('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/lambda_system' A) g0 lam))))).
tt('thm/measure/LAMBDA_SYSTEM_COMPL_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real'), l : (A > $o)]: (((('const/measure/algebra' A) g0) & ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) & (('const/bool/IN' (A > $o)) l (('const/measure/lambda_system' A) g0 lam)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) g0) l) (('const/measure/lambda_system' A) g0 lam))))).
tt('thm/measure/LAMBDA_SYSTEM_INTER_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real'), l1 : (A > $o), l2 : (A > $o)]: (((('const/measure/algebra' A) g0) & ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) & ((('const/bool/IN' (A > $o)) l1 (('const/measure/lambda_system' A) g0 lam)) & (('const/bool/IN' (A > $o)) l2 (('const/measure/lambda_system' A) g0 lam))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) l1 l2) (('const/measure/lambda_system' A) g0 lam))))).
tt('thm/measure/LAMBDA_SYSTEM_ALGEBRA_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: (((('const/measure/algebra' A) g0) & (('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam)))) => (('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/space' A) g0) (('const/measure/lambda_system' A) g0 lam)))))).
tt('thm/measure/LAMBDA_SYSTEM_STRONG_ADDITIVE_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real'), g : (A > $o), l1 : (A > $o), l2 : (A > $o)]: (((('const/measure/algebra' A) g0) & ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) & ((('const/bool/IN' (A > $o)) g (('const/measure/subsets' A) g0)) & ((('const/pred_set/DISJOINT' A) l1 l2) & ((('const/bool/IN' (A > $o)) l1 (('const/measure/lambda_system' A) g0 lam)) & (('const/bool/IN' (A > $o)) l2 (('const/measure/lambda_system' A) g0 lam))))))) => ((lam (('const/pred_set/INTER' A) (('const/pred_set/UNION' A) l1 l2) g)) = ('const/realax/real_add' (lam (('const/pred_set/INTER' A) l1 g)) (lam (('const/pred_set/INTER' A) l2 g))))))).
tt('thm/measure/LAMBDA_SYSTEM_ADDITIVE_', ax, ![A : $t, C : $t, B : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real'), l1 : B, l2 : C]: (((('const/measure/algebra' A) g0) & (('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam)))) => (('const/measure/additive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/lambda_system' A) g0 lam) lam)))))).
tt('thm/measure/COUNTABLY_SUBADDITIVE_SUBADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/measure/countably_subadditive' A) m))) => (('const/measure/subadditive' A) m)))).
tt('thm/measure/SIGMA_ALGEBRA_ALT_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/algebra' A) a) & (![f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/SIGMA_ALGEBRA_ALT_MONO_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/algebra' A) a) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/SIGMA_ALGEBRA_ALT_DISJOINT_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/algebra' A) a) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/SUBADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/measure/subadditive' A) m) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & ((('const/bool/IN' (A > $o)) t (('const/measure/measurable_sets' A) m)) & (u = (('const/pred_set/UNION' A) s t))))) => ('const/real/real_lte' (('const/measure/measure' A) m u) ('const/realax/real_add' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))).
tt('thm/measure/ADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/measure/additive' A) m) & ((('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/pred_set/DISJOINT' A) s t) & (u = (('const/pred_set/UNION' A) s t)))))) => ((('const/measure/measure' A) m u) = ('const/realax/real_add' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))).
tt('thm/measure/COUNTABLY_SUBADDITIVE_', 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 > $o)), s : (A > $o)]: (((('const/measure/countably_subadditive' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (('const/seq/summable' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f)) & ((s = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)))))) => ('const/real/real_lte' (('const/measure/measure' A) m s) ('const/seq/suminf' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f)))))).
tt('thm/measure/ADDITIVE_SUM_', 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 > $o)), n : 'type/num/num']: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/measure/additive' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (![m0 : 'type/num/num', n0 : 'type/num/num']: ((~ (m0 = n0)) => (('const/pred_set/DISJOINT' A) (f m0) (f n0)))))))) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f)) = (('const/measure/measure' A) m (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/count' n)))))))).
tt('thm/measure/INCREASING_ADDITIVE_SUMMABLE_', 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 > $o))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/measure/increasing' A) m) & ((('const/measure/additive' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n))))))))) => ('const/seq/summable' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f))))).
tt('thm/measure/LAMBDA_SYSTEM_POSITIVE_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) => (('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/lambda_system' A) g0 lam) lam)))))).
tt('thm/measure/LAMBDA_SYSTEM_INCREASING_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: ((('const/measure/increasing' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) => (('const/measure/increasing' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/lambda_system' A) g0 lam) lam)))))).
tt('thm/measure/LAMBDA_SYSTEM_STRONG_SUM_', ax, ![A : $t]: (![g0 : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real'), g : (A > $o), f : ('type/num/num' > (A > $o)), n : 'type/num/num']: (((('const/measure/algebra' A) g0) & ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) g0) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) g0) lam))) & ((('const/bool/IN' (A > $o)) g (('const/measure/subsets' A) g0)) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/lambda_system' A) g0 lam))) & (![m : 'type/num/num', n0 : 'type/num/num']: ((~ (m = n0)) => (('const/pred_set/DISJOINT' A) (f m) (f n0)))))))) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) lam (('const/combin/o' 'type/num/num' (A > $o) (A > $o)) (^[s : (A > $o)]: (('const/pred_set/INTER' A) s g)) f))) = (lam (('const/pred_set/INTER' A) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/count' n))) g)))))).
tt('thm/measure/SIGMA_ALGEBRA_ALGEBRA_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) => (('const/measure/algebra' A) a)))).
tt('thm/measure/OUTER_MEASURE_SPACE_POSITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/measure/outer_measure_space' A) m) => (('const/measure/positive' A) m)))).
tt('thm/measure/LAMBDA_SYSTEM_CARATHEODORY_', ax, ![A : $t]: (![gsig : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: (((('const/measure/sigma_algebra' A) gsig) & (('const/measure/outer_measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) gsig) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) gsig) lam)))) => (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/lambda_system' A) gsig lam))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => ((('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/lambda_system' A) gsig lam)) & ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) lam f) (lam (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))))))))))).
tt('thm/measure/CARATHEODORY_LEMMA_', ax, ![A : $t]: (![gsig : ('type/pair/prod' (A > $o) ((A > $o) > $o)), lam : ((A > $o) > 'type/realax/real')]: (((('const/measure/sigma_algebra' A) gsig) & (('const/measure/outer_measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) gsig) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) gsig) lam)))) => (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) gsig) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/lambda_system' A) gsig lam) lam)))))).
tt('thm/measure/INF_MEASURE_NONEMPTY_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), g : (A > $o), s : (A > $o)]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)) & (('const/pred_set/SUBSET' A) g s)))) => (('const/bool/IN' 'type/realax/real') (('const/measure/measure' A) m s) (('const/pred_set/GSPEC' 'type/realax/real' 'type/realax/real') (^[r : 'type/realax/real']: (('const/pair/,' 'type/realax/real' $o) r (?[f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & ((('const/pred_set/SUBSET' A) g (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) r)))))))))))).
tt('thm/measure/INF_MEASURE_POS0_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), g : (A > $o), x : 'type/realax/real']: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/bool/IN' 'type/realax/real') x (('const/pred_set/GSPEC' 'type/realax/real' 'type/realax/real') (^[r : 'type/realax/real']: (('const/pair/,' 'type/realax/real' $o) r (?[f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & ((('const/pred_set/SUBSET' A) g (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) r))))))))))) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/measure/INF_MEASURE_POS_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), g : (A > $o)]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/pred_set/SUBSET' A) g (('const/measure/m_space' A) m)))) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (('const/measure/inf_measure' A) m g))))).
tt('thm/measure/INCREASING_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o)]: (((('const/measure/increasing' A) m) & ((('const/pred_set/SUBSET' 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/real/real_lte' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t))))).
tt('thm/measure/ADDITIVE_INCREASING_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/measure/additive' A) m))) => (('const/measure/increasing' A) m)))).
tt('thm/measure/COUNTABLY_ADDITIVE_ADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/measure/countably_additive' A) m))) => (('const/measure/additive' A) m)))).
tt('thm/measure/COUNTABLY_ADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), f : ('type/num/num' > (A > $o))]: (((('const/measure/countably_additive' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & ((s = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m)))))) => ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m s))))).
tt('thm/measure/INF_MEASURE_AGREES_', 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/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/measure/countably_additive' A) m) & (('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m))))) => ((('const/measure/inf_measure' A) m s) = (('const/measure/measure' A) m s))))).
tt('thm/measure/MEASURE_DOWN_', ax, ![A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m0) (('const/measure/measurable_sets' A) m0))) & ((('const/pred_set/SUBSET' (A > $o)) (('const/measure/measurable_sets' A) m0) (('const/measure/measurable_sets' A) m1)) & (((('const/measure/measure' A) m0) = (('const/measure/measure' A) m1)) & (('const/measure/measure_space' A) m1)))) => (('const/measure/measure_space' A) m0)))).
tt('thm/measure/SIGMA_ALGEBRA_SIGMA_', ax, ![A : $t]: (![sp : (A > $o), sts : ((A > $o) > $o)]: ((('const/measure/subset_class' A) sp sts) => (('const/measure/sigma_algebra' A) (('const/measure/sigma' A) sp sts))))).
tt('thm/measure/POW_ALGEBRA_', ax, ![A : $t]: (![sp : (A > $o)]: (('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp (('const/pred_set/POW' A) sp))))).
tt('thm/measure/POW_SIGMA_ALGEBRA_', ax, ![A : $t]: (![sp : (A > $o)]: (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp (('const/pred_set/POW' A) sp))))).
tt('thm/measure/UNIV_SIGMA_ALGEBRA_', ax, ![A : $t]: (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) ('const/pred_set/UNIV' A) ('const/pred_set/UNIV' (A > $o))))).
tt('thm/measure/INF_MEASURE_EMPTY_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & (('const/measure/positive' A) m)) => ((('const/measure/inf_measure' A) m ('const/pred_set/EMPTY' A)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/measure/INF_MEASURE_POSITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & (('const/measure/positive' A) m)) => (('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) (('const/measure/m_space' A) m)) (('const/measure/inf_measure' A) m))))))).
tt('thm/measure/INF_MEASURE_INCREASING_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & (('const/measure/positive' A) m)) => (('const/measure/increasing' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) (('const/measure/m_space' A) m)) (('const/measure/inf_measure' A) m))))))).
tt('thm/measure/INF_MEASURE_LE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), x : 'type/realax/real']: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/measure/increasing' A) m) & (('const/bool/IN' 'type/realax/real') x (('const/pred_set/GSPEC' 'type/realax/real' 'type/realax/real') (^[r : 'type/realax/real']: (('const/pair/,' 'type/realax/real' $o) r (?[f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((('const/pred_set/SUBSET' A) s (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) r))))))))))) => ('const/real/real_lte' (('const/measure/inf_measure' A) m s) x)))).
tt('thm/measure/INF_MEASURE_CLOSE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), e : 'type/realax/real']: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) & (('const/pred_set/SUBSET' A) s (('const/measure/m_space' A) m))))) => (?[f : ('type/num/num' > (A > $o)), l : 'type/realax/real']: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((('const/pred_set/SUBSET' A) s (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & (('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) l) & ('const/real/real_lte' l ('const/realax/real_add' (('const/measure/inf_measure' A) m s) e)))))))))).
tt('thm/measure/INF_MEASURE_COUNTABLY_SUBADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/measure/increasing' A) m))) => (('const/measure/countably_subadditive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) (('const/measure/m_space' A) m)) (('const/measure/inf_measure' A) m))))))).
tt('thm/measure/INF_MEASURE_OUTER_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & (('const/measure/increasing' A) m))) => (('const/measure/outer_measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) (('const/measure/m_space' A) m)) (('const/measure/inf_measure' A) m))))))).
tt('thm/measure/SIGMA_SUBSET_', ax, ![A : $t]: (![a : ((A > $o) > $o), b : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: (((('const/measure/sigma_algebra' A) b) & (('const/pred_set/SUBSET' (A > $o)) a (('const/measure/subsets' A) b))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) (('const/measure/space' A) b) a)) (('const/measure/subsets' A) b))))).
tt('thm/measure/ALGEBRA_SUBSET_LAMBDA_SYSTEM_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))) & ((('const/measure/positive' A) m) & ((('const/measure/increasing' A) m) & (('const/measure/additive' A) m)))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/measurable_sets' A) m) (('const/measure/lambda_system' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/pred_set/POW' A) (('const/measure/m_space' A) m))) (('const/measure/inf_measure' A) m)))))).
tt('thm/measure/CARATHEODORY_', ax, ![A : $t]: (![m0 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m0) (('const/measure/measurable_sets' A) m0))) & ((('const/measure/positive' A) m0) & (('const/measure/countably_additive' A) m0))) => (?[m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/measurable_sets' A) m0)) => ((('const/measure/measure' A) m s) = (('const/measure/measure' A) m0 s)))) & (((('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) = (('const/measure/sigma' A) (('const/measure/m_space' A) m0) (('const/measure/measurable_sets' A) m0))) & (('const/measure/measure_space' A) m))))))).
tt('thm/measure/SIGMA_SUBSET_SUBSETS_', ax, ![A : $t]: (![sp : (A > $o), a : ((A > $o) > $o)]: (('const/pred_set/SUBSET' (A > $o)) a (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))))).
tt('thm/measure/IN_SIGMA_', ax, ![A : $t]: (![sp : (A > $o), a : ((A > $o) > $o), x : (A > $o)]: ((('const/bool/IN' (A > $o)) x a) => (('const/bool/IN' (A > $o)) x (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)))))).
tt('thm/measure/SIGMA_ALGEBRA_', ax, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) p) = ((('const/measure/subset_class' A) (('const/measure/space' A) p) (('const/measure/subsets' A) p)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) p)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) p)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) p) s) (('const/measure/subsets' A) p)))) & (![c : ((A > $o) > $o)]: (((('const/util_prob/countable' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/measure/subsets' A) p))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) (('const/measure/subsets' A) p)))))))))).
tt('thm/measure/SIGMA_ALGEBRA_COUNTABLE_UNION_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), c : ((A > $o) > $o)]: (((('const/measure/sigma_algebra' A) a) & ((('const/util_prob/countable' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) (('const/measure/subsets' A) a))))).
tt('thm/measure/SIGMA_ALGEBRA_ENUM_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : ('type/num/num' > (A > $o))]: (((('const/measure/sigma_algebra' A) a) & (('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a))))).
tt('thm/measure/MEASURE_COMPL_', 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/measure' A) m (('const/pred_set/DIFF' A) (('const/measure/m_space' A) m) s)) = ('const/real/real_sub' (('const/measure/measure' A) m (('const/measure/m_space' A) m)) (('const/measure/measure' A) m s)))))).
tt('thm/measure/SIGMA_PROPERTY_', ax, ![A : $t]: (![sp : (A > $o), p : ((A > $o) > $o), a : ((A > $o) > $o)]: (((('const/measure/subset_class' A) sp p) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) p) & ((('const/pred_set/SUBSET' (A > $o)) a p) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) sp s) p))) & (![c : ((A > $o) > $o)]: (((('const/util_prob/countable' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) p))))))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)) p)))).
tt('thm/measure/MEASURE_EMPTY_', 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/measure/measure' A) m ('const/pred_set/EMPTY' A)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/measure/SIGMA_SUBSET_MEASURABLE_SETS_', ax, ![A : $t]: (![a : ((A > $o) > $o), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & (('const/pred_set/SUBSET' (A > $o)) a (('const/measure/measurable_sets' A) m))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) (('const/measure/m_space' A) m) a)) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/SIGMA_ALGEBRA_FN_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a)))) & (![f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a)))))))))).
tt('thm/measure/SIGMA_ALGEBRA_FN_DISJOINT_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) = ((('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a)))) & ((![s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/UNION' A) s t) (('const/measure/subsets' A) a)))) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a))))))))))).
tt('thm/measure/SIGMA_PROPERTY_ALT_', ax, ![A : $t]: (![sp : (A > $o), p : ((A > $o) > $o), a : ((A > $o) > $o)]: (((('const/measure/subset_class' A) sp p) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) p) & ((('const/pred_set/SUBSET' (A > $o)) a p) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) sp s) p))) & (![f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) p))))))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)) p)))).
tt('thm/measure/SPACE_SMALLEST_CLOSED_CDI_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/space' A) (('const/measure/smallest_closed_cdi' A) a)) = (('const/measure/space' A) a)))).
tt('thm/measure/SMALLEST_CLOSED_CDI_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) => ((('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) a) (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a))) & ((('const/measure/closed_cdi' A) (('const/measure/smallest_closed_cdi' A) a)) & (('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a)))))))).
tt('thm/measure/CLOSED_CDI_DUNION_', ax, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) p)) & ((('const/measure/closed_cdi' A) p) & ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) p)) & ((('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) p)) & (('const/pred_set/DISJOINT' A) s t))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/UNION' A) s t) (('const/measure/subsets' A) p))))).
tt('thm/measure/CLOSED_CDI_COMPL_', ax, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o)), s : (A > $o)]: (((('const/measure/closed_cdi' A) p) & (('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) p))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) p) s) (('const/measure/subsets' A) p))))).
tt('thm/measure/CLOSED_CDI_DISJOINT_', ax, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : ('type/num/num' > (A > $o))]: (((('const/measure/closed_cdi' A) p) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) p))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n)))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) p))))).
tt('thm/measure/CLOSED_CDI_INCREASING_', ax, ![A : $t]: (![p : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : ('type/num/num' > (A > $o))]: (((('const/measure/closed_cdi' A) p) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) p))) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n))))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) p))))).
tt('thm/measure/SIGMA_PROPERTY_DISJOINT_LEMMA1_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) => (![s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) s t) (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a)))))))).
tt('thm/measure/SIGMA_PROPERTY_DISJOINT_LEMMA2_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/algebra' A) a) => (![s : (A > $o), t : (A > $o)]: (((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a))) & (('const/bool/IN' (A > $o)) t (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) s t) (('const/measure/subsets' A) (('const/measure/smallest_closed_cdi' A) a)))))))).
tt('thm/measure/SIGMA_PROPERTY_DISJOINT_LEMMA_', ax, ![A : $t]: (![sp : (A > $o), a : ((A > $o) > $o), p : ((A > $o) > $o)]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp a)) & ((('const/pred_set/SUBSET' (A > $o)) a p) & (('const/measure/closed_cdi' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp p)))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)) p)))).
tt('thm/measure/SIGMA_PROPERTY_DISJOINT_WEAK_', ax, ![A : $t]: (![sp : (A > $o), p : ((A > $o) > $o), a : ((A > $o) > $o)]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp a)) & ((('const/pred_set/SUBSET' (A > $o)) a p) & ((('const/measure/subset_class' A) sp p) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s p) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) sp s) p))) & ((![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') p)) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) p))) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') p)) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) p)))))))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)) p)))).
tt('thm/measure/SIGMA_PROPERTY_DISJOINT_', ax, ![A : $t]: (![sp : (A > $o), p : ((A > $o) > $o), a : ((A > $o) > $o)]: (((('const/measure/algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp a)) & ((('const/pred_set/SUBSET' (A > $o)) a p) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) sp s) p))) & ((![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))))) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) p))) & (![f : ('type/num/num' > (A > $o))]: (((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/pred_set/INTER' (A > $o)) p (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))))) & (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (f m) (f n))))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) p))))))) => (('const/pred_set/SUBSET' (A > $o)) (('const/measure/subsets' A) (('const/measure/sigma' A) sp a)) p)))).
tt('thm/measure/MEASURE_COUNTABLY_ADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), f : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![m0 : 'type/num/num', n : 'type/num/num']: ((~ (m0 = n)) => (('const/pred_set/DISJOINT' A) (f m0) (f n)))) & (s = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))))))) => ('const/seq/sums' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m s))))).
tt('thm/measure/MEASURE_SPACE_ADDITIVE_', 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/measure/additive' A) m)))).
tt('thm/measure/MEASURE_ADDITIVE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o), u : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('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/pred_set/DISJOINT' A) s t) & (u = (('const/pred_set/UNION' A) s t)))))) => ((('const/measure/measure' A) m u) = ('const/realax/real_add' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))).
tt('thm/measure/MEASURE_COUNTABLE_INCREASING_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), f : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (((f 'const/num/0') = ('const/pred_set/EMPTY' A)) & ((![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))) & (s = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))))))) => ('const/seq/-->' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m s))))).
tt('thm/measure/MEASURE_SPACE_REDUCE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/measurable_sets' A) m) (('const/measure/measure' A) m))) = m))).
tt('thm/measure/SPACE_SIGMA_', ax, ![A : $t]: (![sp : (A > $o), a : ((A > $o) > $o)]: ((('const/measure/space' A) (('const/measure/sigma' A) sp a)) = sp))).
tt('thm/measure/MONOTONE_CONVERGENCE_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), f : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))) & (s = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))))))) => ('const/seq/-->' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m s))))).
tt('thm/measure/SIGMA_REDUCE_', ax, ![A : $t]: (![sp : (A > $o), a : ((A > $o) > $o)]: ((('const/pair/,' (A > $o) ((A > $o) > $o)) sp (('const/measure/subsets' A) (('const/measure/sigma' A) sp a))) = (('const/measure/sigma' A) sp a)))).
tt('thm/measure/MEASURABLE_SETS_SUBSET_SPACE_', 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/pred_set/SUBSET' A) s (('const/measure/m_space' A) m))))).
tt('thm/measure/MEASURABLE_DIFF_PROPERTY_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: (((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/subsets' A) a))))))) => (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => ((('const/util_prob/PREIMAGE' A B) f (('const/pred_set/DIFF' B) (('const/measure/space' B) b) s)) = (('const/pred_set/DIFF' A) (('const/measure/space' A) a) (('const/util_prob/PREIMAGE' A B) f s)))))))).
tt('thm/measure/MEASURABLE_BIGUNION_PROPERTY_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: (((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/subsets' A) a))))))) => (![c : ((B > $o) > $o)]: ((('const/pred_set/SUBSET' (B > $o)) c (('const/measure/subsets' B) b)) => ((('const/util_prob/PREIMAGE' A B) f (('const/pred_set/BIGUNION' B) c)) = (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' (B > $o) (A > $o)) (('const/util_prob/PREIMAGE' A B) f) c)))))))).
tt('thm/measure/MEASUBABLE_BIGUNION_LEMMA_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: (((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/subsets' A) a))))))) => (![c : ((A > $o) > $o)]: (((('const/util_prob/countable' (A > $o)) c) & (('const/pred_set/SUBSET' (A > $o)) c (('const/pred_set/IMAGE' (B > $o) (A > $o)) (('const/util_prob/PREIMAGE' A B) f) (('const/measure/subsets' B) b)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) c) (('const/pred_set/IMAGE' (B > $o) (A > $o)) (('const/util_prob/PREIMAGE' A B) f) (('const/measure/subsets' B) b)))))))).
tt('thm/measure/MEASURABLE_SIGMA_PREIMAGES_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: (((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/subsets' A) a))))))) => (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/space' A) a) (('const/pred_set/IMAGE' (B > $o) (A > $o)) (('const/util_prob/PREIMAGE' A B) f) (('const/measure/subsets' B) b))))))).
tt('thm/measure/IN_MEASURABLE_', ax, ![A : $t, B : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: ((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a b)) = ((('const/measure/sigma_algebra' A) a) & ((('const/measure/sigma_algebra' B) b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) (('const/measure/space' B) b))) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/subsets' B) b)) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))))).
tt('thm/measure/MEASURABLE_SIGMA_', ax, ![B : $t, A : $t]: (![f : (A > B), a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ((B > $o) > $o), sp : (B > $o)]: (((('const/measure/sigma_algebra' A) a) & ((('const/measure/subset_class' B) sp b) & ((('const/bool/IN' (A > B)) f (('const/util_prob/FUNSET' A B) (('const/measure/space' A) a) sp)) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s b) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))))) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a (('const/measure/sigma' B) sp b)))))).
tt('thm/measure/MEASURABLE_SUBSET_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o))]: (('const/pred_set/SUBSET' (A > B)) (('const/measure/measurable' A B) a b) (('const/measure/measurable' A B) a (('const/measure/sigma' B) (('const/measure/space' B) b) (('const/measure/subsets' B) b)))))).
tt('thm/measure/MEASURABLE_LIFT_', ax, ![B : $t, A : $t]: (![f : (A > B), a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o))]: ((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a b)) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a (('const/measure/sigma' B) (('const/measure/space' B) b) (('const/measure/subsets' B) b))))))).
tt('thm/measure/IN_MEASURE_PRESERVING_', ax, ![B : $t, A : $t]: (![m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), f : (A > B)]: ((('const/bool/IN' (A > B)) f (('const/measure/measure_preserving' A B) m1 m2)) = ((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m1) (('const/measure/measurable_sets' A) m1)) (('const/pair/,' (B > $o) ((B > $o) > $o)) (('const/measure/m_space' B) m2) (('const/measure/measurable_sets' B) m2)))) & ((('const/measure/measure_space' A) m1) & ((('const/measure/measure_space' B) m2) & (![s : (B > $o)]: ((('const/bool/IN' (B > $o)) s (('const/measure/measurable_sets' B) m2)) => ((('const/measure/measure' A) m1 (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A B) f s) (('const/measure/m_space' A) m1))) = (('const/measure/measure' B) m2 s)))))))))).
tt('thm/measure/MEASURE_PRESERVING_LIFT_', ax, ![B : $t, A : $t]: (![m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), a : ((B > $o) > $o), f : (A > B)]: (((('const/measure/measure_space' A) m1) & ((('const/measure/measure_space' B) m2) & (((('const/measure/measurable_sets' B) m2) = (('const/measure/subsets' B) (('const/measure/sigma' B) (('const/measure/m_space' B) m2) a))) & (('const/bool/IN' (A > B)) f (('const/measure/measure_preserving' A B) m1 (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) (('const/measure/m_space' B) m2) (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) a (('const/measure/measure' B) m2)))))))) => (('const/bool/IN' (A > B)) f (('const/measure/measure_preserving' A B) m1 m2))))).
tt('thm/measure/MEASURE_PRESERVING_SUBSET_', ax, ![B : $t, A : $t]: (![m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), a : ((B > $o) > $o)]: (((('const/measure/measure_space' A) m1) & ((('const/measure/measure_space' B) m2) & ((('const/measure/measurable_sets' B) m2) = (('const/measure/subsets' B) (('const/measure/sigma' B) (('const/measure/m_space' B) m2) a))))) => (('const/pred_set/SUBSET' (A > B)) (('const/measure/measure_preserving' A B) m1 (('const/pair/,' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))) (('const/measure/m_space' B) m2) (('const/pair/,' ((B > $o) > $o) ((B > $o) > 'type/realax/real')) a (('const/measure/measure' B) m2)))) (('const/measure/measure_preserving' A B) m1 m2))))).
tt('thm/measure/MEASURABLE_I_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) => (('const/bool/IN' (A > A)) ('const/combin/I' A) (('const/measure/measurable' A A) a a))))).
tt('thm/measure/MEASURABLE_COMP_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), c : ('type/pair/prod' (C > $o) ((C > $o) > $o))]: (((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a b)) & (('const/bool/IN' (B > C)) g (('const/measure/measurable' B C) b c))) => (('const/bool/IN' (A > C)) (('const/combin/o' A C B) g f) (('const/measure/measurable' A C) a c))))).
tt('thm/measure/MEASURABLE_COMP_STRONG_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), c : ('type/pair/prod' (C > $o) ((C > $o) > $o))]: (((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a b)) & ((('const/measure/sigma_algebra' C) c) & ((('const/bool/IN' (B > C)) g (('const/util_prob/FUNSET' B C) (('const/measure/space' B) b) (('const/measure/space' C) c))) & (![x : (C > $o)]: ((('const/bool/IN' (C > $o)) x (('const/measure/subsets' C) c)) => (('const/bool/IN' (B > $o)) (('const/pred_set/INTER' B) (('const/util_prob/PREIMAGE' B C) g x) (('const/pred_set/IMAGE' A B) f (('const/measure/space' A) a))) (('const/measure/subsets' B) b))))))) => (('const/bool/IN' (A > C)) (('const/combin/o' A C B) g f) (('const/measure/measurable' A C) a c))))).
tt('thm/measure/MEASURABLE_COMP_STRONGER_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (B > C), a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o)), c : ('type/pair/prod' (C > $o) ((C > $o) > $o)), t : (B > $o)]: (((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) a b)) & ((('const/measure/sigma_algebra' C) c) & ((('const/bool/IN' (B > C)) g (('const/util_prob/FUNSET' B C) (('const/measure/space' B) b) (('const/measure/space' C) c))) & ((('const/pred_set/SUBSET' B) (('const/pred_set/IMAGE' A B) f (('const/measure/space' A) a)) t) & (![s : (C > $o)]: ((('const/bool/IN' (C > $o)) s (('const/measure/subsets' C) c)) => (('const/bool/IN' (B > $o)) (('const/pred_set/INTER' B) (('const/util_prob/PREIMAGE' B C) g s) t) (('const/measure/subsets' B) b)))))))) => (('const/bool/IN' (A > C)) (('const/combin/o' A C B) g f) (('const/measure/measurable' A C) a c))))).
tt('thm/measure/MEASURABLE_UP_LIFT_', ax, ![B : $t, A : $t]: (![sp : (A > $o), a : ((A > $o) > $o), b : ((A > $o) > $o), c : ('type/pair/prod' (B > $o) ((B > $o) > $o)), f : (A > B)]: (((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp a) c)) & ((('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp b)) & (('const/pred_set/SUBSET' (A > $o)) a b))) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp b) c))))).
tt('thm/measure/MEASURABLE_UP_SUBSET_', ax, ![B : $t, A : $t]: (![sp : (A > $o), a : ((A > $o) > $o), b : ((A > $o) > $o), c : ('type/pair/prod' (B > $o) ((B > $o) > $o))]: (((('const/pred_set/SUBSET' (A > $o)) a b) & (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp b))) => (('const/pred_set/SUBSET' (A > B)) (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp a) c) (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) sp b) c))))).
tt('thm/measure/MEASURABLE_UP_SIGMA_', ax, ![B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), b : ('type/pair/prod' (B > $o) ((B > $o) > $o))]: (('const/pred_set/SUBSET' (A > B)) (('const/measure/measurable' A B) a b) (('const/measure/measurable' A B) (('const/measure/sigma' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) b)))).
tt('thm/measure/MEASURE_PRESERVING_UP_LIFT_', ax, ![B : $t, A : $t]: (![a : ((A > $o) > $o), m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), f : (A > B)]: (((('const/measure/measure_space' A) m1) & ((('const/bool/IN' (A > B)) f (('const/measure/measure_preserving' A B) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m1) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) a (('const/measure/measure' A) m1))) m2)) & ((('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m1) (('const/measure/measurable_sets' A) m1))) & (('const/pred_set/SUBSET' (A > $o)) a (('const/measure/measurable_sets' A) m1))))) => (('const/bool/IN' (A > B)) f (('const/measure/measure_preserving' A B) m1 m2))))).
tt('thm/measure/MEASURE_PRESERVING_UP_SUBSET_', ax, ![B : $t, A : $t]: (![a : ((A > $o) > $o), m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m1) & ((('const/pred_set/SUBSET' (A > $o)) a (('const/measure/measurable_sets' A) m1)) & (('const/measure/sigma_algebra' A) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m1) (('const/measure/measurable_sets' A) m1))))) => (('const/pred_set/SUBSET' (A > B)) (('const/measure/measure_preserving' A B) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m1) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) a (('const/measure/measure' A) m1))) m2) (('const/measure/measure_preserving' A B) m1 m2))))).
tt('thm/measure/MEASURE_PRESERVING_UP_SIGMA_', ax, ![B : $t, A : $t]: (![m1 : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), m2 : ('type/pair/prod' (B > $o) ('type/pair/prod' ((B > $o) > $o) ((B > $o) > 'type/realax/real'))), a : ((A > $o) > $o)]: (((('const/measure/measure_space' A) m1) & ((('const/measure/measurable_sets' A) m1) = (('const/measure/subsets' A) (('const/measure/sigma' A) (('const/measure/m_space' A) m1) a)))) => (('const/pred_set/SUBSET' (A > B)) (('const/measure/measure_preserving' A B) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m1) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) a (('const/measure/measure' A) m1))) m2) (('const/measure/measure_preserving' A B) m1 m2))))).
tt('thm/measure/MEASURABLE_PROD_SIGMA_', ax, ![C : $t, B : $t, A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), a1 : ('type/pair/prod' (B > $o) ((B > $o) > $o)), a2 : ('type/pair/prod' (C > $o) ((C > $o) > $o)), f : (A > ('type/pair/prod' B C))]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > B)) (('const/combin/o' A B ('type/pair/prod' B C)) ('const/pair/FST' B C) f) (('const/measure/measurable' A B) a a1)) & (('const/bool/IN' (A > C)) (('const/combin/o' A C ('type/pair/prod' B C)) ('const/pair/SND' B C) f) (('const/measure/measurable' A C) a a2)))) => (('const/bool/IN' (A > ('type/pair/prod' B C))) f (('const/measure/measurable' A ('type/pair/prod' B C)) a (('const/measure/sigma' ('type/pair/prod' B C)) (('const/pred_set/CROSS' B C) (('const/measure/space' B) a1) (('const/measure/space' C) a2)) (('const/util_prob/prod_sets' B C) (('const/measure/subsets' B) a1) (('const/measure/subsets' C) a2)))))))).
tt('thm/measure/MEASURABLE_RANGE_REDUCE_', ax, ![A : $t, B : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > B), s : (B > $o)]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) (('const/pair/,' (B > $o) ((B > $o) > $o)) s (('const/pred_set/POW' B) s)))) & (~ (s = ('const/pred_set/EMPTY' B))))) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) (('const/pair/,' (B > $o) ((B > $o) > $o)) (('const/pred_set/INTER' B) s (('const/pred_set/IMAGE' A B) f (('const/measure/m_space' A) m))) (('const/pred_set/POW' B) (('const/pred_set/INTER' B) s (('const/pred_set/IMAGE' A B) f (('const/measure/m_space' A) m)))))))))).
tt('thm/measure/MEASURABLE_POW_TO_POW_', ax, ![B : $t, A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > B)]: (((('const/measure/measure_space' A) m) & ((('const/measure/measurable_sets' A) m) = (('const/pred_set/POW' A) (('const/measure/m_space' A) m)))) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) (('const/pair/,' (B > $o) ((B > $o) > $o)) ('const/pred_set/UNIV' B) (('const/pred_set/POW' B) ('const/pred_set/UNIV' B)))))))).
tt('thm/measure/MEASURABLE_POW_TO_POW_IMAGE_', ax, ![A : $t, B : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), f : (A > B)]: (((('const/measure/measure_space' A) m) & ((('const/measure/measurable_sets' A) m) = (('const/pred_set/POW' A) (('const/measure/m_space' A) m)))) => (('const/bool/IN' (A > B)) f (('const/measure/measurable' A B) (('const/pair/,' (A > $o) ((A > $o) > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m)) (('const/pair/,' (B > $o) ((B > $o) > $o)) (('const/pred_set/IMAGE' A B) f (('const/measure/m_space' A) m)) (('const/pred_set/POW' B) (('const/pred_set/IMAGE' A B) f (('const/measure/m_space' A) m))))))))).
tt('thm/measure/MEASURE_SPACE_SUBSET_', ax, ![A : $t]: (![s : (A > $o), 's\'' : (A > $o), m : ((A > $o) > 'type/realax/real')]: (((('const/pred_set/SUBSET' A) 's\'' s) & (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) s) m)))) => (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) 's\'' (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) 's\'') m)))))).
tt('thm/measure/STRONG_MEASURE_SPACE_SUBSET_', ax, ![A : $t]: (![s : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), 's\'' : (A > $o)]: (((('const/pred_set/SUBSET' A) 's\'' (('const/measure/m_space' A) s)) & ((('const/measure/measure_space' A) s) & (('const/pred_set/SUBSET' (A > $o)) (('const/pred_set/POW' A) 's\'') (('const/measure/measurable_sets' A) s)))) => (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) 's\'' (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/POW' A) 's\'') (('const/measure/measure' A) s))))))).
tt('thm/measure/MEASURE_REAL_SUM_IMAGE_', 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)) & ((![x : A]: ((('const/bool/IN' A) x s) => (('const/bool/IN' (A > $o)) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)) (('const/measure/measurable_sets' A) m)))) & (('const/pred_set/FINITE' A) s)))) => ((('const/measure/measure' A) m s) = (('const/real_sigma/REAL_SUM_IMAGE' A) (^[x : A]: (('const/measure/measure' A) m (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))) s))))).
tt('thm/measure/SIGMA_POW_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/measure/sigma' A) s (('const/pred_set/POW' A) s)) = (('const/pair/,' (A > $o) ((A > $o) > $o)) s (('const/pred_set/POW' A) s))))).
tt('thm/measure/finite_additivity_sufficient_for_finite_spaces_', ax, ![A : $t]: (![s : ('type/pair/prod' (A > $o) ((A > $o) > $o)), m : ((A > $o) > 'type/realax/real')]: (((('const/measure/sigma_algebra' A) s) & ((('const/pred_set/FINITE' A) (('const/measure/space' A) s)) & ((('const/measure/positive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) s) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) s) m))) & (('const/measure/additive' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) s) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) s) m)))))) => (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/space' A) s) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/subsets' A) s) m)))))).
tt('thm/measure/finite_additivity_sufficient_for_finite_spaces2_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('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/pred_set/FINITE' A) (('const/measure/m_space' A) m)) & ((('const/measure/positive' A) m) & (('const/measure/additive' A) m)))) => (('const/measure/measure_space' A) m)))).
tt('thm/measure/IMAGE_SING_', ax, ![B : $t, A : $t]: (![f : (A > B), x : A]: ((('const/pred_set/IMAGE' A B) f (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) = (('const/pred_set/INSERT' B) (f x) ('const/pred_set/EMPTY' B))))).
tt('thm/measure/SUBSET_BIGINTER_', ax, ![A : $t]: (![X : (A > $o), P : ((A > $o) > $o)]: ((('const/pred_set/SUBSET' A) X (('const/pred_set/BIGINTER' A) P)) = (![Y : (A > $o)]: ((('const/bool/IN' (A > $o)) Y P) => (('const/pred_set/SUBSET' A) X Y)))))).
tt('thm/measure/MEASURE_SPACE_INCREASING_', 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/measure/increasing' A) m)))).
tt('thm/measure/MEASURE_SPACE_POSITIVE_', 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/measure/positive' A) m)))).
tt('thm/measure/MEASURE_SPACE_INTER_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('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 > $o)) (('const/pred_set/INTER' A) s t) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MEASURE_SPACE_UNION_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('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 > $o)) (('const/pred_set/UNION' A) s t) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MEASURE_SPACE_DIFF_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), t : (A > $o)]: (((('const/measure/measure_space' A) m) & ((('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 > $o)) (('const/pred_set/DIFF' A) s t) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MEASURE_COMPL_SUBSET_', ax, ![A : $t]: (![t : (A > $o), 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/bool/IN' (A > $o)) t (('const/measure/measurable_sets' A) m)) & (('const/pred_set/SUBSET' A) t s)))) => ((('const/measure/measure' A) m (('const/pred_set/DIFF' A) s t)) = ('const/real/real_sub' (('const/measure/measure' A) m s) (('const/measure/measure' A) m t)))))).
tt('thm/measure/MEASURE_SPACE_BIGUNION_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & (![n : 'type/num/num']: (('const/bool/IN' (A > $o)) (s n) (('const/measure/measurable_sets' A) m)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) s ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MEASURE_SPACE_IN_MSPACE_', 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))) => (![x : A]: ((('const/bool/IN' A) x A0) => (('const/bool/IN' A) x (('const/measure/m_space' A) m))))))).
tt('thm/measure/MEASURE_SPACE_SUBSET_MSPACE_', ax, ![A : $t]: (![A0 : (A > $o), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: (((('const/measure/measure_space' A) m) & (('const/bool/IN' (A > $o)) A0 (('const/measure/measurable_sets' A) m))) => (('const/pred_set/SUBSET' A) A0 (('const/measure/m_space' A) m))))).
tt('thm/measure/MEASURE_SPACE_EMPTY_MEASURABLE_', 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/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MEASURE_SPACE_MSPACE_MEASURABLE_', 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/bool/IN' (A > $o)) (('const/measure/m_space' A) m) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/SIGMA_ALGEBRA_FN_BIGINTER_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/measure/sigma_algebra' A) a) => ((('const/measure/subset_class' A) (('const/measure/space' A) a) (('const/measure/subsets' A) a)) & ((('const/bool/IN' (A > $o)) ('const/pred_set/EMPTY' A) (('const/measure/subsets' A) a)) & ((![s : (A > $o)]: ((('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)) => (('const/bool/IN' (A > $o)) (('const/pred_set/DIFF' A) (('const/measure/space' A) a) s) (('const/measure/subsets' A) a)))) & (![f : ('type/num/num' > (A > $o))]: ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGINTER' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/subsets' A) a)))))))))).
tt('thm/measure/MEASURE_SPACE_BIGINTER_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & (![n : 'type/num/num']: (('const/bool/IN' (A > $o)) (s n) (('const/measure/measurable_sets' A) m)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGINTER' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) s ('const/pred_set/UNIV' 'type/num/num'))) (('const/measure/measurable_sets' A) m))))).
tt('thm/measure/MONOTONE_CONVERGENCE2_', 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 > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f n) (f ('const/num/SUC' n)))))) => ('const/seq/-->' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))))))).
tt('thm/measure/MONOTONE_CONVERGENCE_BIGINTER_', ax, ![A : $t]: (![m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))), s : (A > $o), f : ('type/num/num' > (A > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & ((![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f ('const/num/SUC' n)) (f n))) & (s = (('const/pred_set/BIGINTER' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num'))))))) => ('const/seq/-->' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m s))))).
tt('thm/measure/MONOTONE_CONVERGENCE_BIGINTER2_', 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 > $o))]: (((('const/measure/measure_space' A) m) & ((('const/bool/IN' ('type/num/num' > (A > $o))) f (('const/util_prob/FUNSET' 'type/num/num' (A > $o)) ('const/pred_set/UNIV' 'type/num/num') (('const/measure/measurable_sets' A) m))) & (![n : 'type/num/num']: (('const/pred_set/SUBSET' A) (f ('const/num/SUC' n)) (f n))))) => ('const/seq/-->' (('const/combin/o' 'type/num/num' 'type/realax/real' (A > $o)) (('const/measure/measure' A) m) f) (('const/measure/measure' A) m (('const/pred_set/BIGINTER' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) f ('const/pred_set/UNIV' 'type/num/num')))))))).
tt('thm/measure/MEASURE_SPACE_RESTRICTED_', 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/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) s (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/pred_set/IMAGE' (A > $o) (A > $o)) (^[t : (A > $o)]: (('const/pred_set/INTER' A) s t)) (('const/measure/measurable_sets' A) m)) (('const/measure/measure' A) m))))))).
tt('thm/measure/MEASURE_SPACE_CMUL_', 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/real/real_lte' ('const/real/real_of_num' 'const/num/0') c)) => (('const/measure/measure_space' A) (('const/pair/,' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real'))) (('const/measure/m_space' A) m) (('const/pair/,' ((A > $o) > $o) ((A > $o) > 'type/realax/real')) (('const/measure/measurable_sets' A) m) (^[a : (A > $o)]: ('const/realax/real_mul' c (('const/measure/measure' A) m a))))))))).
tt('thm/measure/BIGUNION_IMAGE_Q_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : ('type/extreal/extreal' > (A > $o))]: (((('const/measure/sigma_algebra' A) a) & (('const/bool/IN' ('type/extreal/extreal' > (A > $o))) f (('const/util_prob/FUNSET' 'type/extreal/extreal' (A > $o)) 'const/extreal/Q_set' (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > $o)) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/extreal/extreal' (A > $o)) f 'const/extreal/Q_set')) (('const/measure/subsets' A) a))))).
tt('thm/measure/Borel_def_', def, ('const/measure/Borel' = (('const/measure/sigma' 'type/extreal/extreal') ('const/pred_set/UNIV' 'type/extreal/extreal') (('const/pred_set/IMAGE' 'type/extreal/extreal' ('type/extreal/extreal' > $o)) (^[a : 'type/extreal/extreal']: (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' x a))))) ('const/pred_set/UNIV' 'type/extreal/extreal'))))).
tt('thm/measure/SIGMA_ALGEBRA_BOREL_', ax, (('const/measure/sigma_algebra' 'type/extreal/extreal') 'const/measure/Borel')).
tt('thm/measure/MEASURABLE_BOREL_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/util_prob/PREIMAGE' A 'type/extreal/extreal') f (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' x c))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' (f x) c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_NEGINF_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((f x) = 'const/extreal/NegInf')))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT1_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' c (f x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT2_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' (f x) c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT3_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' c (f x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT4_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT5_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT6_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT7_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT8_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((f x) = c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALT9_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => ((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/util_prob/FUNSET' A 'type/extreal/extreal') (('const/measure/space' A) a) ('const/pred_set/UNIV' 'type/extreal/extreal'))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (~ ((f x) = c))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a)))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALL_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' (f x) c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' c (f x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' (f x) c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' c (f x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (~ ((f x) = c))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((f x) = c)))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))))))))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ALL_MEASURE_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), m : ('type/pair/prod' (A > $o) ('type/pair/prod' ((A > $o) > $o) ((A > $o) > 'type/realax/real')))]: ((('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')) => ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' (f x) c)))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' c (f x))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' (f x) c)))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' c (f x))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_lt' (f x) d))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_lt' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/extreal/extreal_le' c (f x)) & ('const/extreal/extreal_le' (f x) d))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & ((![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((f x) = c)))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))) & (![c : 'type/extreal/extreal']: (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (~ ((f x) = c))))) (('const/measure/m_space' A) m)) (('const/measure/measurable_sets' A) m))))))))))))))).
tt('thm/measure/IN_MEASURABLE_BOREL_LT_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: (((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_lt' (f x) (g x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))).
tt('thm/measure/IN_MEASURABLE_BOREL_LE_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: (((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))) => (('const/bool/IN' (A > $o)) (('const/pred_set/INTER' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ('const/extreal/extreal_le' (f x) (g x))))) (('const/measure/space' A) a)) (('const/measure/subsets' A) a))))).
tt('thm/measure/SPACE_BOREL_', ax, ((('const/measure/space' 'type/extreal/extreal') 'const/measure/Borel') = ('const/pred_set/UNIV' 'type/extreal/extreal'))).
tt('thm/measure/BOREL_MEASURABLE_SETS1_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' x c)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS2_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_le' c x)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS3_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_le' x c)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS4_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' c x)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS5_', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_le' c x) & ('const/extreal/extreal_lt' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS6_', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_lt' c x) & ('const/extreal/extreal_le' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS7_', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_le' c x) & ('const/extreal/extreal_le' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS8_', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_lt' c x) & ('const/extreal/extreal_lt' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS9_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/INSERT' 'type/extreal/extreal') c ('const/pred_set/EMPTY' 'type/extreal/extreal')) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS10_', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (~ (x = c))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_0', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' x c)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_1', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_le' c x)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_2', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_lt' c x)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_3', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x ('const/extreal/extreal_le' x c)))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_4', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_lt' c x) & ('const/extreal/extreal_lt' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_5', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_le' c x) & ('const/extreal/extreal_lt' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_6', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_lt' c x) & ('const/extreal/extreal_le' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_7', ax, (![c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (('const/extreal/extreal_le' c x) & ('const/extreal/extreal_le' x d))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_8', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/INSERT' 'type/extreal/extreal') c ('const/pred_set/EMPTY' 'type/extreal/extreal')) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/BOREL_MEASURABLE_SETS_e9', ax, (![c : 'type/extreal/extreal']: (('const/bool/IN' ('type/extreal/extreal' > $o)) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (~ (x = c))))) (('const/measure/subsets' 'type/extreal/extreal') 'const/measure/Borel')))).
tt('thm/measure/IN_MEASURABLE_BOREL_CONST_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), k : 'type/extreal/extreal', f : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((f x) = k)))) => (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_INDICATOR_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), A0 : (A > $o), f : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > $o)) A0 (('const/measure/subsets' A) a)) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((f x) = (('const/measure/indicator_fn' A) A0 x)))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_CMUL_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), z : 'type/realax/real']: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((g x) = ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (f x))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ABS_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((g x) = ('const/extreal/extreal_abs' (f x))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_SQR_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((g x) = ('const/extreal/extreal_pow' (f x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_ADD_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), h : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & ((('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((h x) = ('const/extreal/extreal_add' (f x) (g x)))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) h (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_SUB_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), h : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & ((('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((h x) = ('const/extreal/extreal_sub' (f x) (g x)))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) h (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_MUL_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), h : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & ((![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((~ ((f x) = 'const/extreal/NegInf')) & ((~ ((f x) = 'const/extreal/PosInf')) & ((~ ((g x) = 'const/extreal/NegInf')) & (~ ((g x) = 'const/extreal/PosInf'))))))) & ((('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((h x) = ('const/extreal/extreal_mul' (f x) (g x))))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) h (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_SUM_', ax, ![A : $t, B : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (B > (A > 'type/extreal/extreal')), g : (A > 'type/extreal/extreal'), s : (B > $o)]: (((('const/pred_set/FINITE' B) s) & ((('const/measure/sigma_algebra' A) a) & ((![i : B]: ((('const/bool/IN' B) i s) => (('const/bool/IN' (A > 'type/extreal/extreal')) (f i) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')))) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((g x) = (('const/extreal/EXTREAL_SUM_IMAGE' B) (^[i : B]: (f i x)) s))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_CMUL_INDICATOR_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), z : 'type/realax/real', s : (A > $o)]: (((('const/measure/sigma_algebra' A) a) & (('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a))) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' z) (('const/measure/indicator_fn' A) s x))) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_MUL_INDICATOR_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (('const/bool/IN' (A > $o)) s (('const/measure/subsets' A) a)))) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) s x))) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal')]: ((('const/measure/sigma_algebra' A) a) => ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_mul' (f x) (('const/measure/indicator_fn' A) (('const/measure/space' A) a) x))) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')))))).
tt('thm/measure/IN_MEASURABLE_BOREL_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')]: (((('const/measure/measure_space' 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 f s a 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'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_POW_', ax, ![A : $t]: (![n : 'type/num/num', a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((~ ((f x) = 'const/extreal/NegInf')) & (~ ((f x) = 'const/extreal/PosInf'))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_pow' (f x) n)) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_MAX_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal')]: (((('const/measure/sigma_algebra' A) a) & ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (('const/bool/IN' (A > 'type/extreal/extreal')) g (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')))) => (('const/bool/IN' (A > 'type/extreal/extreal')) (^[x : A]: ('const/extreal/extreal_max' (f x) (g x))) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_MONO_SUP_', ax, ![A : $t]: (![fn : ('type/num/num' > (A > 'type/extreal/extreal')), f : (A > 'type/extreal/extreal'), a : ('type/pair/prod' (A > $o) ((A > $o) > $o))]: (((('const/measure/sigma_algebra' A) a) & ((![n : 'type/num/num']: (('const/bool/IN' (A > 'type/extreal/extreal')) (fn n) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))) & ((![n : 'type/num/num', x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ('const/extreal/extreal_le' (fn n x) (fn ('const/num/SUC' n) x)))) & (![x : A]: ((('const/bool/IN' A) x (('const/measure/space' A) a)) => ((f x) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (fn n x)) ('const/pred_set/UNIV' 'type/num/num'))))))))) => (('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/fn_plus_def_', def, ![A : $t]: (![f : (A > 'type/extreal/extreal')]: ((('const/measure/fn_plus' A) f) = (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') (f x)) (f x) ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/measure/fn_minus_def_', def, ![A : $t]: (![f : (A > 'type/extreal/extreal')]: ((('const/measure/fn_minus' A) f) = (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') ('const/extreal/extreal_lt' (f x) ('const/extreal/extreal_of_num' 'const/num/0')) ('const/extreal/extreal_ainv' (f x)) ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/measure/fn_abs_def_', def, ![A : $t]: (![f : (A > 'type/extreal/extreal')]: ((('const/measure/fn_abs' A) f) = (^[x : A]: ('const/extreal/extreal_abs' (f x)))))).
tt('thm/measure/FN_PLUS_POS_', ax, ![A : $t]: (![g : (A > 'type/extreal/extreal'), x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (('const/measure/fn_plus' A) g x)))).
tt('thm/measure/FN_MINUS_POS_', ax, ![A : $t]: (![g : (A > 'type/extreal/extreal'), x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (('const/measure/fn_minus' A) g x)))).
tt('thm/measure/FN_PLUS_POS_ID_', ax, ![A : $t]: (![g : (A > 'type/extreal/extreal')]: ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x))) => ((('const/measure/fn_plus' A) g) = g)))).
tt('thm/measure/FN_MINUS_POS_ZERO_', ax, ![A : $t]: (![g : (A > 'type/extreal/extreal')]: ((![x : A]: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g x))) => ((('const/measure/fn_minus' A) g) = (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/measure/FN_PLUS_CMUL_0', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) => ((('const/measure/fn_plus' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/measure/fn_plus' A) f x))))))).
tt('thm/measure/FN_PLUS_CMUL_e1', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (('const/real/real_lte' c ('const/real/real_of_num' 'const/num/0')) => ((('const/measure/fn_plus' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' ('const/extreal/Normal' c)) (('const/measure/fn_minus' A) f x))))))).
tt('thm/measure/FN_MINUS_CMUL_0', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) => ((('const/measure/fn_minus' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/measure/fn_minus' A) f x))))))).
tt('thm/measure/FN_MINUS_CMUL_e1', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (('const/real/real_lte' c ('const/real/real_of_num' 'const/num/0')) => ((('const/measure/fn_minus' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x)))) = (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' ('const/extreal/Normal' c)) (('const/measure/fn_plus' A) f x))))))).
tt('thm/measure/FN_PLUS_ADD_LE_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), x : A]: ('const/extreal/extreal_le' (('const/measure/fn_plus' A) (^[x0 : A]: ('const/extreal/extreal_add' (f x0) (g x0))) x) ('const/extreal/extreal_add' (('const/measure/fn_plus' A) f x) (('const/measure/fn_plus' A) g x))))).
tt('thm/measure/FN_MINUS_ADD_LE_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), g : (A > 'type/extreal/extreal'), x : A]: ('const/extreal/extreal_le' (('const/measure/fn_minus' A) (^[x0 : A]: ('const/extreal/extreal_add' (f x0) (g x0))) x) ('const/extreal/extreal_add' (('const/measure/fn_minus' A) f x) (('const/measure/fn_minus' A) g x))))).
tt('thm/measure/IN_MEASURABLE_BOREL_FN_PLUS_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => (('const/bool/IN' (A > 'type/extreal/extreal')) (('const/measure/fn_plus' A) f) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_FN_MINUS_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) => (('const/bool/IN' (A > 'type/extreal/extreal')) (('const/measure/fn_minus' A) f) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel'))))).
tt('thm/measure/IN_MEASURABLE_BOREL_PLUS_MINUS_', ax, ![A : $t]: (![a : ('type/pair/prod' (A > $o) ((A > $o) > $o)), f : (A > 'type/extreal/extreal')]: ((('const/bool/IN' (A > 'type/extreal/extreal')) f (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) = ((('const/bool/IN' (A > 'type/extreal/extreal')) (('const/measure/fn_plus' A) f) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')) & (('const/bool/IN' (A > 'type/extreal/extreal')) (('const/measure/fn_minus' A) f) (('const/measure/measurable' A 'type/extreal/extreal') a 'const/measure/Borel')))))).
tt('thm/measure/INDICATOR_FN_MUL_INTER_', ax, ![A : $t]: (![A0 : (A > $o), B : (A > $o)]: ((^[t : A]: ('const/extreal/extreal_mul' (('const/measure/indicator_fn' A) A0 t) (('const/measure/indicator_fn' A) B t))) = (^[t : A]: (('const/measure/indicator_fn' A) (('const/pred_set/INTER' A) A0 B) t))))).
tt('thm/measure/indicator_fn_split_', ax, ![A : $t]: (![r : ('type/num/num' > $o), s : (A > $o), b : ('type/num/num' > (A > $o))]: (((('const/pred_set/FINITE' 'type/num/num') r) & (((('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) b r)) = s) & (![i : 'type/num/num', j : 'type/num/num']: (((('const/bool/IN' 'type/num/num') i r) & ((('const/bool/IN' 'type/num/num') j r) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (b i) (b j)))))) => (![a : (A > $o)]: ((('const/pred_set/SUBSET' A) a s) => ((('const/measure/indicator_fn' A) a) = (^[x : A]: (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: (('const/measure/indicator_fn' A) (('const/pred_set/INTER' A) a (b i)) x)) r)))))))).
tt('thm/measure/indicator_fn_suminf_', ax, ![A : $t]: (![a : ('type/num/num' > (A > $o)), x : A]: ((![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) => (('const/pred_set/DISJOINT' A) (a m) (a n)))) => (('const/extreal/ext_suminf' (^[i : 'type/num/num']: (('const/measure/indicator_fn' A) (a i) x))) = (('const/measure/indicator_fn' A) (('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) a ('const/pred_set/UNIV' 'type/num/num'))) x))))).
tt('thm/measure/measure_split_', ax, ![A : $t]: (![r : ('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')))]: (((('const/measure/measure_space' A) m) & ((('const/pred_set/FINITE' 'type/num/num') r) & (((('const/pred_set/BIGUNION' A) (('const/pred_set/IMAGE' 'type/num/num' (A > $o)) b r)) = (('const/measure/m_space' A) m)) & ((![i : 'type/num/num', j : 'type/num/num']: (((('const/bool/IN' 'type/num/num') i r) & ((('const/bool/IN' 'type/num/num') j r) & (~ (i = j)))) => (('const/pred_set/DISJOINT' A) (b i) (b j)))) & (![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i r) => (('const/bool/IN' (A > $o)) (b i) (('const/measure/measurable_sets' A) m)))))))) => (![a : (A > $o)]: ((('const/bool/IN' (A > $o)) a (('const/measure/measurable_sets' A) m)) => ((('const/measure/measure' A) m a) = (('const/real_sigma/REAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: (('const/measure/measure' A) m (('const/pred_set/INTER' A) a (b i)))) r))))))).
