tt('type/extreal/extreal', ty, $t).
tt('const/extreal/EXTREAL_SUM_IMAGE', ty, ![A : $t]: ((A > 'type/extreal/extreal') > ((A > $o) > 'type/extreal/extreal'))).
tt('const/extreal/NegInf', ty, 'type/extreal/extreal').
tt('const/extreal/Normal', ty, ('type/realax/real' > 'type/extreal/extreal')).
tt('const/extreal/PosInf', ty, 'type/extreal/extreal').
tt('const/extreal/Q_set', ty, ('type/extreal/extreal' > $o)).
tt('const/extreal/ceiling', ty, ('type/extreal/extreal' > 'type/num/num')).
tt('const/extreal/ext_mono_decreasing', ty, (('type/num/num' > 'type/extreal/extreal') > $o)).
tt('const/extreal/ext_mono_increasing', ty, (('type/num/num' > 'type/extreal/extreal') > $o)).
tt('const/extreal/ext_suminf', ty, (('type/num/num' > 'type/extreal/extreal') > 'type/extreal/extreal')).
tt('const/extreal/extreal_CASE', ty, ![A : $t]: ('type/extreal/extreal' > (A > (A > (('type/realax/real' > A) > A))))).
tt('const/extreal/extreal_abs', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_add', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_add_tupled', ty, (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal')).
tt('const/extreal/extreal_ainv', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_div', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_exp', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_inf', ty, (('type/extreal/extreal' > $o) > 'type/extreal/extreal')).
tt('const/extreal/extreal_inv', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_le', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > $o))).
tt('const/extreal/extreal_le_tupled', ty, (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o)).
tt('const/extreal/extreal_lg', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_logr', ty, ('type/realax/real' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_lt', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > $o))).
tt('const/extreal/extreal_max', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_min', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_mul', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_mul_tupled', ty, (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal')).
tt('const/extreal/extreal_of_num', ty, ('type/num/num' > 'type/extreal/extreal')).
tt('const/extreal/extreal_pow', ty, ('type/extreal/extreal' > ('type/num/num' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_size', ty, ('type/extreal/extreal' > 'type/num/num')).
tt('const/extreal/extreal_sqrt', ty, ('type/extreal/extreal' > 'type/extreal/extreal')).
tt('const/extreal/extreal_sub', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > 'type/extreal/extreal'))).
tt('const/extreal/extreal_sub_tupled', ty, (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal')).
tt('const/extreal/extreal_sup', ty, (('type/extreal/extreal' > $o) > 'type/extreal/extreal')).
tt('const/extreal/mono_decreasing', ty, (('type/num/num' > 'type/realax/real') > $o)).
tt('const/extreal/mono_increasing', ty, (('type/num/num' > 'type/realax/real') > $o)).
tt('const/extreal/open_interval', ty, ('type/extreal/extreal' > ('type/extreal/extreal' > ('type/extreal/extreal' > $o)))).
tt('const/extreal/open_intervals_set', ty, (('type/extreal/extreal' > $o) > $o)).
tt('const/extreal/rational_intervals', ty, (('type/extreal/extreal' > $o) > $o)).
tt('const/extreal/real', ty, ('type/extreal/extreal' > 'type/realax/real')).
tt('thm/extreal/extreal_TY_DEF_', def, (?[rep : ('type/extreal/extreal' > ('type/ind_type/recspace' 'type/realax/real'))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' 'type/realax/real') 'type/extreal/extreal') (^[a0 : ('type/ind_type/recspace' 'type/realax/real')]: (!['\'extreal\'' : (('type/ind_type/recspace' 'type/realax/real') > $o)]: ((![a00 : ('type/ind_type/recspace' 'type/realax/real')]: (((a00 = (('const/ind_type/CONSTR' 'type/realax/real') 'const/num/0' ('const/bool/ARB' 'type/realax/real') (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))) | ((a00 = (('const/ind_type/CONSTR' 'type/realax/real') ('const/num/SUC' 'const/num/0') ('const/bool/ARB' 'type/realax/real') (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))) | (?[a : 'type/realax/real']: (a00 = ((^[a1 : 'type/realax/real']: (('const/ind_type/CONSTR' 'type/realax/real') ('const/num/SUC' ('const/num/SUC' 'const/num/0')) a1 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' 'type/realax/real')))) a))))) => ('\'extreal\'' a00))) => ('\'extreal\'' a0)))) rep))).
tt('thm/extreal/extreal_case_def_0', def, ![A : $t]: (![v : A, v1 : A, f : ('type/realax/real' > A)]: ((('const/extreal/extreal_CASE' A) 'const/extreal/NegInf' v v1 f) = v))).
tt('thm/extreal/extreal_case_def_1', def, ![A : $t]: (![v : A, v1 : A, f : ('type/realax/real' > A)]: ((('const/extreal/extreal_CASE' A) 'const/extreal/PosInf' v v1 f) = v1))).
tt('thm/extreal/extreal_case_def_e2', def, ![A : $t]: (![a : 'type/realax/real', v : A, v1 : A, f : ('type/realax/real' > A)]: ((('const/extreal/extreal_CASE' A) ('const/extreal/Normal' a) v v1 f) = (f a)))).
tt('thm/extreal/extreal_size_def_0', def, (('const/extreal/extreal_size' 'const/extreal/NegInf') = 'const/num/0')).
tt('thm/extreal/extreal_size_def_1', def, (('const/extreal/extreal_size' 'const/extreal/PosInf') = 'const/num/0')).
tt('thm/extreal/extreal_size_def_e2', def, (![a : 'type/realax/real']: (('const/extreal/extreal_size' ('const/extreal/Normal' a)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/datatype_extreal_', ax, (![extreal : ('type/extreal/extreal' > ('type/extreal/extreal' > (('type/realax/real' > 'type/extreal/extreal') > $o)))]: (('const/bool/DATATYPE' $o) (extreal 'const/extreal/NegInf' 'const/extreal/PosInf' 'const/extreal/Normal')))).
tt('thm/extreal/extreal_distinct_0', ax, (~ ('const/extreal/NegInf' = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_distinct_1', ax, (![a : 'type/realax/real']: (~ ('const/extreal/NegInf' = ('const/extreal/Normal' a))))).
tt('thm/extreal/extreal_distinct_e2', ax, (![a : 'type/realax/real']: (~ ('const/extreal/PosInf' = ('const/extreal/Normal' a))))).
tt('thm/extreal/extreal_case_cong_', ax, ![A : $t]: (!['v1\'' : A, 'v\'' : A, 'f\'' : ('type/realax/real' > A), M : 'type/extreal/extreal', 'M\'' : 'type/extreal/extreal', v : A, v1 : A, f : ('type/realax/real' > A)]: (((M = 'M\'') & ((('M\'' = 'const/extreal/NegInf') => (v = 'v\'')) & ((('M\'' = 'const/extreal/PosInf') => (v1 = 'v1\'')) & (![a : 'type/realax/real']: (('M\'' = ('const/extreal/Normal' a)) => ((f a) = ('f\'' a))))))) => ((('const/extreal/extreal_CASE' A) M v v1 f) = (('const/extreal/extreal_CASE' A) 'M\'' 'v\'' 'v1\'' 'f\''))))).
tt('thm/extreal/extreal_nchotomy_', ax, (![ee : 'type/extreal/extreal']: ((ee = 'const/extreal/NegInf') | ((ee = 'const/extreal/PosInf') | (?[r : 'type/realax/real']: (ee = ('const/extreal/Normal' r))))))).
tt('thm/extreal/extreal_Axiom_', ax, ![A : $t]: (![f0 : A, f1 : A, f2 : ('type/realax/real' > A)]: (?[fn : ('type/extreal/extreal' > A)]: (((fn 'const/extreal/NegInf') = f0) & (((fn 'const/extreal/PosInf') = f1) & (![a : 'type/realax/real']: ((fn ('const/extreal/Normal' a)) = (f2 a)))))))).
tt('thm/extreal/extreal_induction_', ax, (![P : ('type/extreal/extreal' > $o)]: (((P 'const/extreal/NegInf') & ((P 'const/extreal/PosInf') & (![r : 'type/realax/real']: (P ('const/extreal/Normal' r))))) => (![e : 'type/extreal/extreal']: (P e))))).
tt('thm/extreal/extreal_of_num_def_', def, (![n : 'type/num/num']: (('const/extreal/extreal_of_num' n) = ('const/extreal/Normal' ('const/real/real_of_num' n))))).
tt('thm/extreal/real_def_', def, (![x : 'type/extreal/extreal']: (('const/extreal/real' x) = (('const/bool/COND' 'type/realax/real') ((x = 'const/extreal/NegInf') | (x = 'const/extreal/PosInf')) ('const/real/real_of_num' 'const/num/0') (('const/min/@' 'type/realax/real') (^[r : 'type/realax/real']: (x = ('const/extreal/Normal' r)))))))).
tt('thm/extreal/real_normal_', ax, (![x : 'type/realax/real']: (('const/extreal/real' ('const/extreal/Normal' x)) = x))).
tt('thm/extreal/normal_real_', ax, (![x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/Normal' ('const/extreal/real' x)) = x)))).
tt('thm/extreal/extreal_add_tupled_primitive_def_', def, ('const/extreal/extreal_add_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') 'type/extreal/extreal') (('const/min/@' (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))) (^[R : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))]: (('const/relation/WF' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) R))) (^[extreal_add_tupled : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal'), 'a\'' : ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')]: (('const/pair/pair_CASE' 'type/extreal/extreal' 'type/extreal/extreal' 'type/extreal/extreal') 'a\'' (^[v : 'type/extreal/extreal', a : 'type/extreal/extreal']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') v (('const/extreal/extreal_CASE' 'type/extreal/extreal') a (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^[v6 : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf'))) (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^[x : 'type/realax/real']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') a (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^[y : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') ('const/extreal/Normal' ('const/realax/real_add' x y))))))))))))).
tt('thm/extreal/extreal_add_curried_def_', def, (![x : 'type/extreal/extreal', x1 : 'type/extreal/extreal']: (('const/extreal/extreal_add' x x1) = ('const/extreal/extreal_add_tupled' (('const/pair/,' 'type/extreal/extreal' 'type/extreal/extreal') x x1))))).
tt('thm/extreal/extreal_add_ind_', ax, (![P : ('type/extreal/extreal' > ('type/extreal/extreal' > $o))]: (((![x : 'type/realax/real', y : 'type/realax/real']: (P ('const/extreal/Normal' x) ('const/extreal/Normal' y))) & ((![a : 'type/extreal/extreal']: (P 'const/extreal/PosInf' a)) & ((P 'const/extreal/NegInf' 'const/extreal/PosInf') & ((![v2 : 'type/realax/real']: (P ('const/extreal/Normal' v2) 'const/extreal/PosInf')) & ((P 'const/extreal/NegInf' 'const/extreal/NegInf') & ((![v5 : 'type/realax/real']: (P 'const/extreal/NegInf' ('const/extreal/Normal' v5))) & (![v3 : 'type/realax/real']: (P ('const/extreal/Normal' v3) 'const/extreal/NegInf')))))))) => (![v : 'type/extreal/extreal', v1 : 'type/extreal/extreal']: (P v v1))))).
tt('thm/extreal/extreal_add_def_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/extreal/extreal_add' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/extreal/Normal' ('const/realax/real_add' x y))))).
tt('thm/extreal/extreal_add_def_1', ax, (![a : 'type/extreal/extreal']: (('const/extreal/extreal_add' 'const/extreal/PosInf' a) = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_add_def_2', ax, (('const/extreal/extreal_add' 'const/extreal/NegInf' 'const/extreal/PosInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_add_def_3', ax, (![v2 : 'type/realax/real']: (('const/extreal/extreal_add' ('const/extreal/Normal' v2) 'const/extreal/PosInf') = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_add_def_4', ax, (('const/extreal/extreal_add' 'const/extreal/NegInf' 'const/extreal/NegInf') = 'const/extreal/NegInf')).
tt('thm/extreal/extreal_add_def_5', ax, (![v5 : 'type/realax/real']: (('const/extreal/extreal_add' 'const/extreal/NegInf' ('const/extreal/Normal' v5)) = 'const/extreal/NegInf'))).
tt('thm/extreal/extreal_add_def_e6', ax, (![v3 : 'type/realax/real']: (('const/extreal/extreal_add' ('const/extreal/Normal' v3) 'const/extreal/NegInf') = 'const/extreal/NegInf'))).
tt('thm/extreal/extreal_sub_tupled_primitive_def_', def, ('const/extreal/extreal_sub_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') 'type/extreal/extreal') (('const/min/@' (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))) (^[R : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))]: (('const/relation/WF' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) R))) (^[extreal_sub_tupled : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal'), 'a\'' : ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')]: (('const/pair/pair_CASE' 'type/extreal/extreal' 'type/extreal/extreal' 'type/extreal/extreal') 'a\'' (^[v : 'type/extreal/extreal', a : 'type/extreal/extreal']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') v (('const/extreal/extreal_CASE' 'type/extreal/extreal') a (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (^[v6 : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf'))) (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^[x : 'type/realax/real']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') a (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (^[y : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') ('const/extreal/Normal' ('const/real/real_sub' x y))))))))))))).
tt('thm/extreal/extreal_sub_curried_def_', def, (![x : 'type/extreal/extreal', x1 : 'type/extreal/extreal']: (('const/extreal/extreal_sub' x x1) = ('const/extreal/extreal_sub_tupled' (('const/pair/,' 'type/extreal/extreal' 'type/extreal/extreal') x x1))))).
tt('thm/extreal/extreal_sub_ind_', ax, (![P : ('type/extreal/extreal' > ('type/extreal/extreal' > $o))]: (((![x : 'type/realax/real', y : 'type/realax/real']: (P ('const/extreal/Normal' x) ('const/extreal/Normal' y))) & ((![a : 'type/extreal/extreal']: (P 'const/extreal/PosInf' a)) & ((P 'const/extreal/NegInf' 'const/extreal/PosInf') & ((![v2 : 'type/realax/real']: (P ('const/extreal/Normal' v2) 'const/extreal/PosInf')) & ((P 'const/extreal/NegInf' 'const/extreal/NegInf') & ((![v5 : 'type/realax/real']: (P 'const/extreal/NegInf' ('const/extreal/Normal' v5))) & (![v3 : 'type/realax/real']: (P ('const/extreal/Normal' v3) 'const/extreal/NegInf')))))))) => (![v : 'type/extreal/extreal', v1 : 'type/extreal/extreal']: (P v v1))))).
tt('thm/extreal/extreal_sub_def_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/extreal/extreal_sub' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/extreal/Normal' ('const/real/real_sub' x y))))).
tt('thm/extreal/extreal_sub_def_1', ax, (![a : 'type/extreal/extreal']: (('const/extreal/extreal_sub' 'const/extreal/PosInf' a) = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_sub_def_2', ax, (('const/extreal/extreal_sub' 'const/extreal/NegInf' 'const/extreal/PosInf') = 'const/extreal/NegInf')).
tt('thm/extreal/extreal_sub_def_3', ax, (![v2 : 'type/realax/real']: (('const/extreal/extreal_sub' ('const/extreal/Normal' v2) 'const/extreal/PosInf') = 'const/extreal/NegInf'))).
tt('thm/extreal/extreal_sub_def_4', ax, (('const/extreal/extreal_sub' 'const/extreal/NegInf' 'const/extreal/NegInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_sub_def_5', ax, (![v5 : 'type/realax/real']: (('const/extreal/extreal_sub' 'const/extreal/NegInf' ('const/extreal/Normal' v5)) = 'const/extreal/NegInf'))).
tt('thm/extreal/extreal_sub_def_e6', ax, (![v3 : 'type/realax/real']: (('const/extreal/extreal_sub' ('const/extreal/Normal' v3) 'const/extreal/NegInf') = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_le_tupled_primitive_def_', def, ('const/extreal/extreal_le_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') $o) (('const/min/@' (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))) (^[R : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))]: (('const/relation/WF' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) R))) (^[extreal_le_tupled : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o), 'a\'' : ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')]: (('const/pair/pair_CASE' $o 'type/extreal/extreal' 'type/extreal/extreal') 'a\'' (^[v : 'type/extreal/extreal', a : 'type/extreal/extreal']: (('const/extreal/extreal_CASE' $o) v (('const/combin/I' $o) $true) (('const/extreal/extreal_CASE' $o) a (('const/combin/I' $o) $false) (('const/combin/I' $o) $true) (^[v6 : 'type/realax/real']: (('const/combin/I' $o) $false))) (^[x : 'type/realax/real']: (('const/extreal/extreal_CASE' $o) a (('const/combin/I' $o) $false) (('const/combin/I' $o) $true) (^[y : 'type/realax/real']: (('const/combin/I' $o) ('const/real/real_lte' x y)))))))))))).
tt('thm/extreal/extreal_le_curried_def_', def, (![x : 'type/extreal/extreal', x1 : 'type/extreal/extreal']: (('const/extreal/extreal_le' x x1) = ('const/extreal/extreal_le_tupled' (('const/pair/,' 'type/extreal/extreal' 'type/extreal/extreal') x x1))))).
tt('thm/extreal/extreal_le_ind_', ax, (![P : ('type/extreal/extreal' > ('type/extreal/extreal' > $o))]: (((![x : 'type/realax/real', y : 'type/realax/real']: (P ('const/extreal/Normal' x) ('const/extreal/Normal' y))) & ((![a : 'type/extreal/extreal']: (P 'const/extreal/NegInf' a)) & ((P 'const/extreal/PosInf' 'const/extreal/PosInf') & ((![v2 : 'type/realax/real']: (P ('const/extreal/Normal' v2) 'const/extreal/PosInf')) & ((P 'const/extreal/PosInf' 'const/extreal/NegInf') & ((![v3 : 'type/realax/real']: (P ('const/extreal/Normal' v3) 'const/extreal/NegInf')) & (![v5 : 'type/realax/real']: (P 'const/extreal/PosInf' ('const/extreal/Normal' v5))))))))) => (![v : 'type/extreal/extreal', v1 : 'type/extreal/extreal']: (P v v1))))).
tt('thm/extreal/extreal_le_def_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/extreal/extreal_le' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/real/real_lte' x y)))).
tt('thm/extreal/extreal_le_def_1', ax, (![a : 'type/extreal/extreal']: (('const/extreal/extreal_le' 'const/extreal/NegInf' a) = $true))).
tt('thm/extreal/extreal_le_def_2', ax, (('const/extreal/extreal_le' 'const/extreal/PosInf' 'const/extreal/PosInf') = $true)).
tt('thm/extreal/extreal_le_def_3', ax, (![v2 : 'type/realax/real']: (('const/extreal/extreal_le' ('const/extreal/Normal' v2) 'const/extreal/PosInf') = $true))).
tt('thm/extreal/extreal_le_def_4', ax, (('const/extreal/extreal_le' 'const/extreal/PosInf' 'const/extreal/NegInf') = $false)).
tt('thm/extreal/extreal_le_def_5', ax, (![v3 : 'type/realax/real']: (('const/extreal/extreal_le' ('const/extreal/Normal' v3) 'const/extreal/NegInf') = $false))).
tt('thm/extreal/extreal_le_def_e6', ax, (![v5 : 'type/realax/real']: (('const/extreal/extreal_le' 'const/extreal/PosInf' ('const/extreal/Normal' v5)) = $false))).
tt('thm/extreal/extreal_lt_def_', def, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) = (~ ('const/extreal/extreal_le' y x))))).
tt('thm/extreal/extreal_mul_tupled_primitive_def_', def, ('const/extreal/extreal_mul_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') 'type/extreal/extreal') (('const/min/@' (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))) (^[R : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > $o))]: (('const/relation/WF' ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) R))) (^[extreal_mul_tupled : (('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal') > 'type/extreal/extreal'), a : ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')]: (('const/pair/pair_CASE' 'type/extreal/extreal' 'type/extreal/extreal' 'type/extreal/extreal') a (^[v : 'type/extreal/extreal', v1 : 'type/extreal/extreal']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') v (('const/extreal/extreal_CASE' 'type/extreal/extreal') v1 (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (^[y : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') (('const/bool/COND' 'type/extreal/extreal') (y = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) 'const/extreal/NegInf' 'const/extreal/PosInf'))))) (('const/extreal/extreal_CASE' 'type/extreal/extreal') v1 (('const/combin/I' 'type/extreal/extreal') 'const/extreal/NegInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^['y\'' : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') (('const/bool/COND' 'type/extreal/extreal') ('y\'' = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') 'y\'') 'const/extreal/PosInf' 'const/extreal/NegInf'))))) (^[x : 'type/realax/real']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') v1 (('const/combin/I' 'type/extreal/extreal') (('const/bool/COND' 'type/extreal/extreal') (x = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) 'const/extreal/NegInf' 'const/extreal/PosInf'))) (('const/combin/I' 'type/extreal/extreal') (('const/bool/COND' 'type/extreal/extreal') (x = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) 'const/extreal/PosInf' 'const/extreal/NegInf'))) (^['y\'\'' : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') ('const/extreal/Normal' ('const/realax/real_mul' x 'y\'\''))))))))))))).
tt('thm/extreal/extreal_mul_curried_def_', def, (![x : 'type/extreal/extreal', x1 : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x x1) = ('const/extreal/extreal_mul_tupled' (('const/pair/,' 'type/extreal/extreal' 'type/extreal/extreal') x x1))))).
tt('thm/extreal/extreal_mul_ind_', ax, (![P : ('type/extreal/extreal' > ('type/extreal/extreal' > $o))]: (((P 'const/extreal/NegInf' 'const/extreal/NegInf') & ((P 'const/extreal/NegInf' 'const/extreal/PosInf') & ((P 'const/extreal/PosInf' 'const/extreal/NegInf') & ((P 'const/extreal/PosInf' 'const/extreal/PosInf') & ((![x : 'type/realax/real']: (P ('const/extreal/Normal' x) 'const/extreal/NegInf')) & ((![y : 'type/realax/real']: (P 'const/extreal/NegInf' ('const/extreal/Normal' y))) & ((![x : 'type/realax/real']: (P ('const/extreal/Normal' x) 'const/extreal/PosInf')) & ((![y : 'type/realax/real']: (P 'const/extreal/PosInf' ('const/extreal/Normal' y))) & (![x : 'type/realax/real', y : 'type/realax/real']: (P ('const/extreal/Normal' x) ('const/extreal/Normal' y))))))))))) => (![v : 'type/extreal/extreal', v1 : 'type/extreal/extreal']: (P v v1))))).
tt('thm/extreal/extreal_mul_def_0', ax, (('const/extreal/extreal_mul' 'const/extreal/NegInf' 'const/extreal/NegInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_mul_def_1', ax, (('const/extreal/extreal_mul' 'const/extreal/NegInf' 'const/extreal/PosInf') = 'const/extreal/NegInf')).
tt('thm/extreal/extreal_mul_def_2', ax, (('const/extreal/extreal_mul' 'const/extreal/PosInf' 'const/extreal/NegInf') = 'const/extreal/NegInf')).
tt('thm/extreal/extreal_mul_def_3', ax, (('const/extreal/extreal_mul' 'const/extreal/PosInf' 'const/extreal/PosInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_mul_def_4', ax, (![x : 'type/realax/real']: (('const/extreal/extreal_mul' ('const/extreal/Normal' x) 'const/extreal/NegInf') = (('const/bool/COND' 'type/extreal/extreal') (x = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) 'const/extreal/NegInf' 'const/extreal/PosInf'))))).
tt('thm/extreal/extreal_mul_def_5', ax, (![y : 'type/realax/real']: (('const/extreal/extreal_mul' 'const/extreal/NegInf' ('const/extreal/Normal' y)) = (('const/bool/COND' 'type/extreal/extreal') (y = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) 'const/extreal/NegInf' 'const/extreal/PosInf'))))).
tt('thm/extreal/extreal_mul_def_6', ax, (![x : 'type/realax/real']: (('const/extreal/extreal_mul' ('const/extreal/Normal' x) 'const/extreal/PosInf') = (('const/bool/COND' 'type/extreal/extreal') (x = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) 'const/extreal/PosInf' 'const/extreal/NegInf'))))).
tt('thm/extreal/extreal_mul_def_7', ax, (![y : 'type/realax/real']: (('const/extreal/extreal_mul' 'const/extreal/PosInf' ('const/extreal/Normal' y)) = (('const/bool/COND' 'type/extreal/extreal') (y = ('const/real/real_of_num' 'const/num/0')) ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')) (('const/bool/COND' 'type/extreal/extreal') ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) 'const/extreal/PosInf' 'const/extreal/NegInf'))))).
tt('thm/extreal/extreal_mul_def_e8', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/extreal/extreal_mul' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/extreal/Normal' ('const/realax/real_mul' x y))))).
tt('thm/extreal/extreal_inv_def_0', def, (('const/extreal/extreal_inv' 'const/extreal/NegInf') = ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/extreal/extreal_inv_def_1', def, (('const/extreal/extreal_inv' 'const/extreal/PosInf') = ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/extreal/extreal_inv_def_e2', def, (![x : 'type/realax/real']: (('const/extreal/extreal_inv' ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/realax/inv' x))))).
tt('thm/extreal/extreal_ainv_def_0', def, (('const/extreal/extreal_ainv' 'const/extreal/NegInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_ainv_def_1', def, (('const/extreal/extreal_ainv' 'const/extreal/PosInf') = 'const/extreal/NegInf')).
tt('thm/extreal/extreal_ainv_def_e2', def, (![x : 'type/realax/real']: (('const/extreal/extreal_ainv' ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/realax/real_neg' x))))).
tt('thm/extreal/extreal_div_def_', def, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_div' x y) = ('const/extreal/extreal_mul' x ('const/extreal/extreal_inv' y))))).
tt('thm/extreal/extreal_abs_primitive_def_', def, ('const/extreal/extreal_abs' = (('const/relation/WFREC' 'type/extreal/extreal' 'type/extreal/extreal') (('const/min/@' ('type/extreal/extreal' > ('type/extreal/extreal' > $o))) (^[R : ('type/extreal/extreal' > ('type/extreal/extreal' > $o))]: (('const/relation/WF' 'type/extreal/extreal') R))) (^[extreal_abs : ('type/extreal/extreal' > 'type/extreal/extreal'), a : 'type/extreal/extreal']: (('const/extreal/extreal_CASE' 'type/extreal/extreal') a (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (('const/combin/I' 'type/extreal/extreal') 'const/extreal/PosInf') (^[x : 'type/realax/real']: (('const/combin/I' 'type/extreal/extreal') ('const/extreal/Normal' ('const/real/abs' x))))))))).
tt('thm/extreal/extreal_abs_ind_', ax, (![P : ('type/extreal/extreal' > $o)]: (((![x : 'type/realax/real']: (P ('const/extreal/Normal' x))) & ((P 'const/extreal/NegInf') & (P 'const/extreal/PosInf'))) => (![v : 'type/extreal/extreal']: (P v))))).
tt('thm/extreal/extreal_abs_def_0', ax, (![x : 'type/realax/real']: (('const/extreal/extreal_abs' ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/real/abs' x))))).
tt('thm/extreal/extreal_abs_def_1', ax, (('const/extreal/extreal_abs' 'const/extreal/NegInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_abs_def_e2', ax, (('const/extreal/extreal_abs' 'const/extreal/PosInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_logr_def_0', def, (![b : 'type/realax/real', x : 'type/realax/real']: (('const/extreal/extreal_logr' b ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/util_prob/logr' b x))))).
tt('thm/extreal/extreal_logr_def_1', def, (![b : 'type/realax/real']: (('const/extreal/extreal_logr' b 'const/extreal/PosInf') = 'const/extreal/PosInf'))).
tt('thm/extreal/extreal_logr_def_e2', def, (![b : 'type/realax/real']: (('const/extreal/extreal_logr' b 'const/extreal/NegInf') = 'const/extreal/NegInf'))).
tt('thm/extreal/extreal_lg_def_', def, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_lg' x) = ('const/extreal/extreal_logr' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/extreal/extreal_exp_def_0', def, (![x : 'type/realax/real']: (('const/extreal/extreal_exp' ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/transc/exp' x))))).
tt('thm/extreal/extreal_exp_def_1', def, (('const/extreal/extreal_exp' 'const/extreal/PosInf') = 'const/extreal/PosInf')).
tt('thm/extreal/extreal_exp_def_e2', def, (('const/extreal/extreal_exp' 'const/extreal/NegInf') = ('const/extreal/Normal' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/extreal/extreal_pow_def_0', def, (![a : 'type/realax/real', n : 'type/num/num']: (('const/extreal/extreal_pow' ('const/extreal/Normal' a) n) = ('const/extreal/Normal' ('const/real/pow' a n))))).
tt('thm/extreal/extreal_pow_def_1', def, (![n : 'type/num/num']: (('const/extreal/extreal_pow' 'const/extreal/PosInf' n) = (('const/bool/COND' 'type/extreal/extreal') (n = 'const/num/0') ('const/extreal/Normal' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/extreal/PosInf')))).
tt('thm/extreal/extreal_pow_def_e2', def, (![n : 'type/num/num']: (('const/extreal/extreal_pow' 'const/extreal/NegInf' n) = (('const/bool/COND' 'type/extreal/extreal') (n = 'const/num/0') ('const/extreal/Normal' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/bool/COND' 'type/extreal/extreal') ('const/arithmetic/EVEN' n) 'const/extreal/PosInf' 'const/extreal/NegInf'))))).
tt('thm/extreal/extreal_sqrt_def_0', def, (![x : 'type/realax/real']: (('const/extreal/extreal_sqrt' ('const/extreal/Normal' x)) = ('const/extreal/Normal' ('const/transc/sqrt' x))))).
tt('thm/extreal/extreal_sqrt_def_e1', def, (('const/extreal/extreal_sqrt' 'const/extreal/PosInf') = 'const/extreal/PosInf')).
tt('thm/extreal/REAL_LT_LMUL_0_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y)) & ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))) => ('const/realax/real_lt' y ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/extreal/REAL_LT_RMUL_0_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y)) & ('const/realax/real_lt' y ('const/real/real_of_num' 'const/num/0'))) => ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/extreal/REAL_LT_LMUL_NEG_0_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/real/real_of_num' 'const/num/0')) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)) => ('const/realax/real_lt' y ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/extreal/REAL_LT_RMUL_NEG_0_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/real/real_of_num' 'const/num/0')) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/extreal/REAL_LT_LMUL_NEG_0_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/real/real_of_num' 'const/num/0')) & ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)))).
tt('thm/extreal/REAL_LT_RMUL_NEG_0_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/real/real_of_num' 'const/num/0')) & ('const/realax/real_lt' y ('const/real/real_of_num' 'const/num/0'))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/extreal/REAL_LT_RDIV_EQ_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' z ('const/real/real_of_num' 'const/num/0')) => (('const/realax/real_lt' ('const/real/#slash#' y z) x) = ('const/realax/real_lt' ('const/realax/real_mul' x z) y))))).
tt('thm/extreal/REAL_LE_RDIV_EQ_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' z ('const/real/real_of_num' 'const/num/0')) => (('const/real/real_lte' ('const/real/#slash#' y z) x) = ('const/real/real_lte' ('const/realax/real_mul' x z) y))))).
tt('thm/extreal/POW_POS_EVEN_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0')) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' x n)) = ('const/arithmetic/EVEN' n))))).
tt('thm/extreal/POW_NEG_ODD_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0')) => (('const/realax/real_lt' ('const/real/pow' x n) ('const/real/real_of_num' 'const/num/0')) = ('const/arithmetic/ODD' n))))).
tt('thm/extreal/LOGR_MONO_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real', b : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) & ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) b))) => (('const/real/real_lte' ('const/util_prob/logr' b x) ('const/util_prob/logr' b y)) = ('const/real/real_lte' x y))))).
tt('thm/extreal/LOGR_MONO_LE_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', b : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x y) & ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) b))) => ('const/real/real_lte' ('const/util_prob/logr' b x) ('const/util_prob/logr' b y))))).
tt('thm/extreal/mono_increasing_def_', def, (![f : ('type/num/num' > 'type/realax/real')]: (('const/extreal/mono_increasing' f) = (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/real/real_lte' (f m) (f n))))))).
tt('thm/extreal/mono_increasing_suc_', ax, (![f : ('type/num/num' > 'type/realax/real')]: (('const/extreal/mono_increasing' f) = (![n : 'type/num/num']: ('const/real/real_lte' (f n) (f ('const/num/SUC' n))))))).
tt('thm/extreal/mono_decreasing_def_', def, (![f : ('type/num/num' > 'type/realax/real')]: (('const/extreal/mono_decreasing' f) = (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/real/real_lte' (f n) (f m))))))).
tt('thm/extreal/mono_decreasing_suc_', ax, (![f : ('type/num/num' > 'type/realax/real')]: (('const/extreal/mono_decreasing' f) = (![n : 'type/num/num']: ('const/real/real_lte' (f ('const/num/SUC' n)) (f n)))))).
tt('thm/extreal/mono_increasing_converges_to_sup_', ax, (![f : ('type/num/num' > 'type/realax/real'), r : 'type/realax/real']: ((('const/extreal/mono_increasing' f) & ('const/seq/-->' f r)) => (r = ('const/real/sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/realax/real') f ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/extreal/extreal_cases_', ax, (![x : 'type/extreal/extreal']: ((x = 'const/extreal/NegInf') | ((x = 'const/extreal/PosInf') | (?[r : 'type/realax/real']: (x = ('const/extreal/Normal' r))))))).
tt('thm/extreal/extreal_eq_zero_', ax, (![x : 'type/realax/real']: ((('const/extreal/Normal' x) = ('const/extreal/extreal_of_num' 'const/num/0')) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/extreal/extreal_not_infty_0', ax, (![x : 'type/realax/real']: (~ (('const/extreal/Normal' x) = 'const/extreal/NegInf')))).
tt('thm/extreal/extreal_not_infty_e1', ax, (![x : 'type/realax/real']: (~ (('const/extreal/Normal' x) = 'const/extreal/PosInf')))).
tt('thm/extreal/num_not_infty_0', ax, (![n : 'type/num/num']: (~ (('const/extreal/extreal_of_num' n) = 'const/extreal/NegInf')))).
tt('thm/extreal/num_not_infty_e1', ax, (![n : 'type/num/num']: (~ (('const/extreal/extreal_of_num' n) = 'const/extreal/PosInf')))).
tt('thm/extreal/extreal_11_', ax, (![a : 'type/realax/real', 'a\'' : 'type/realax/real']: ((('const/extreal/Normal' a) = ('const/extreal/Normal' 'a\'')) = (a = 'a\'')))).
tt('thm/extreal/mul_rzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x ('const/extreal/extreal_of_num' 'const/num/0')) = ('const/extreal/extreal_of_num' 'const/num/0')))).
tt('thm/extreal/mul_lzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' 'const/num/0') x) = ('const/extreal/extreal_of_num' 'const/num/0')))).
tt('thm/extreal/mul_rone_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = x))).
tt('thm/extreal/mul_lone_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) = x))).
tt('thm/extreal/entire_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_mul' x y) = ('const/extreal/extreal_of_num' 'const/num/0')) = ((x = ('const/extreal/extreal_of_num' 'const/num/0')) | (y = ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/extreal/extreal_lt_eq_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/extreal/extreal_lt' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/realax/real_lt' x y)))).
tt('thm/extreal/le_refl_', ax, (![x : 'type/extreal/extreal']: ('const/extreal/extreal_le' x x))).
tt('thm/extreal/lt_refl_', ax, (![x : 'type/extreal/extreal']: (~ ('const/extreal/extreal_lt' x x)))).
tt('thm/extreal/le_infty_tLL', ax, (![x : 'type/extreal/extreal']: ('const/extreal/extreal_le' 'const/extreal/NegInf' x))).
tt('thm/extreal/le_infty_tRL', ax, (![x : 'type/extreal/extreal']: ('const/extreal/extreal_le' x 'const/extreal/PosInf'))).
tt('thm/extreal/le_infty_1', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' x 'const/extreal/NegInf') = (x = 'const/extreal/NegInf')))).
tt('thm/extreal/le_infty_e2', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' 'const/extreal/PosInf' x) = (x = 'const/extreal/PosInf')))).
tt('thm/extreal/lt_infty_0', ax, (![y : 'type/realax/real']: ('const/extreal/extreal_lt' 'const/extreal/NegInf' ('const/extreal/Normal' y)))).
tt('thm/extreal/lt_infty_1', ax, (![y : 'type/realax/real']: ('const/extreal/extreal_lt' ('const/extreal/Normal' y) 'const/extreal/PosInf'))).
tt('thm/extreal/lt_infty_2', ax, ('const/extreal/extreal_lt' 'const/extreal/NegInf' 'const/extreal/PosInf')).
tt('thm/extreal/lt_infty_3', ax, (![x : 'type/extreal/extreal']: (~ ('const/extreal/extreal_lt' x 'const/extreal/NegInf')))).
tt('thm/extreal/lt_infty_4', ax, (![x : 'type/extreal/extreal']: (~ ('const/extreal/extreal_lt' 'const/extreal/PosInf' x)))).
tt('thm/extreal/lt_infty_5', ax, (![x : 'type/extreal/extreal']: ((~ (x = 'const/extreal/PosInf')) = ('const/extreal/extreal_lt' x 'const/extreal/PosInf')))).
tt('thm/extreal/lt_infty_e6', ax, (![x : 'type/extreal/extreal']: ((~ (x = 'const/extreal/NegInf')) = ('const/extreal/extreal_lt' 'const/extreal/NegInf' x)))).
tt('thm/extreal/lt_imp_le_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) => ('const/extreal/extreal_le' x y)))).
tt('thm/extreal/lt_imp_ne_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) => (~ (x = y))))).
tt('thm/extreal/le_trans_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x y) & ('const/extreal/extreal_le' y z)) => ('const/extreal/extreal_le' x z)))).
tt('thm/extreal/lt_trans_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' x y) & ('const/extreal/extreal_lt' y z)) => ('const/extreal/extreal_lt' x z)))).
tt('thm/extreal/let_trans_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x y) & ('const/extreal/extreal_lt' y z)) => ('const/extreal/extreal_lt' x z)))).
tt('thm/extreal/le_antisym_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x y) & ('const/extreal/extreal_le' y x)) = (x = y)))).
tt('thm/extreal/lt_antisym_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (~ (('const/extreal/extreal_lt' x y) & ('const/extreal/extreal_lt' y x))))).
tt('thm/extreal/lte_trans_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' x y) & ('const/extreal/extreal_le' y z)) => ('const/extreal/extreal_lt' x z)))).
tt('thm/extreal/le_total_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' x y) | ('const/extreal/extreal_le' y x)))).
tt('thm/extreal/lt_total_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((x = y) | (('const/extreal/extreal_lt' x y) | ('const/extreal/extreal_lt' y x))))).
tt('thm/extreal/le_01_', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/lt_01_', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/ne_01_', ax, (~ (('const/extreal/extreal_of_num' 'const/num/0') = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/le_02_', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/lt_02_', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/ne_02_', ax, (~ (('const/extreal/extreal_of_num' 'const/num/0') = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/le_num_', ax, (![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' n)))).
tt('thm/extreal/lt_le_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) = (('const/extreal/extreal_le' x y) & (~ (x = y)))))).
tt('thm/extreal/le_lt_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' x y) = (('const/extreal/extreal_lt' x y) | (x = y))))).
tt('thm/extreal/le_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_ainv' x) ('const/extreal/extreal_ainv' y)) = ('const/extreal/extreal_le' y x)))).
tt('thm/extreal/lt_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_ainv' x) ('const/extreal/extreal_ainv' y)) = ('const/extreal/extreal_lt' y x)))).
tt('thm/extreal/le_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/lt_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/let_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/lte_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/le_add2_', ax, (![w : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' w x) & ('const/extreal/extreal_le' y z)) => ('const/extreal/extreal_le' ('const/extreal/extreal_add' w y) ('const/extreal/extreal_add' x z))))).
tt('thm/extreal/lt_add2_', ax, (![w : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' w x) & ('const/extreal/extreal_lt' y z)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_add' w y) ('const/extreal/extreal_add' x z))))).
tt('thm/extreal/let_add2_', ax, (![w : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (w = 'const/extreal/NegInf')) & ((~ (w = 'const/extreal/PosInf')) & (('const/extreal/extreal_le' w x) & ('const/extreal/extreal_lt' y z)))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_add' w y) ('const/extreal/extreal_add' x z))))).
tt('thm/extreal/let_add2_alt_', ax, (![w : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & (('const/extreal/extreal_le' w x) & ('const/extreal/extreal_lt' y z)))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_add' w y) ('const/extreal/extreal_add' x z))))).
tt('thm/extreal/le_addr_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' x ('const/extreal/extreal_add' x y)) = ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y))))).
tt('thm/extreal/le_addr_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y) => ('const/extreal/extreal_le' x ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/le_ladd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' ('const/extreal/extreal_add' x y) ('const/extreal/extreal_add' x z)) = ('const/extreal/extreal_le' y z))))).
tt('thm/extreal/le_radd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' ('const/extreal/extreal_add' y x) ('const/extreal/extreal_add' z x)) = ('const/extreal/extreal_le' y z))))).
tt('thm/extreal/le_radd_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_le' y z) => ('const/extreal/extreal_le' ('const/extreal/extreal_add' y x) ('const/extreal/extreal_add' z x))))).
tt('thm/extreal/le_ladd_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_le' y z) => ('const/extreal/extreal_le' ('const/extreal/extreal_add' x y) ('const/extreal/extreal_add' x z))))).
tt('thm/extreal/lt_ladd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' ('const/extreal/extreal_add' x y) ('const/extreal/extreal_add' x z)) = ('const/extreal/extreal_lt' y z))))).
tt('thm/extreal/lt_radd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' ('const/extreal/extreal_add' y x) ('const/extreal/extreal_add' z x)) = ('const/extreal/extreal_lt' y z))))).
tt('thm/extreal/lt_addl_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' y ('const/extreal/extreal_add' x y)) = ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x))))).
tt('thm/extreal/le_lneg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_ainv' x) y) = ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_add' x y))))).
tt('thm/extreal/le_mul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/let_mul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/lte_mul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/le_mul_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x ('const/extreal/extreal_of_num' 'const/num/0')) & ('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/mul_le_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/lt_mul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') y)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/lt_mul_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' x ('const/extreal/extreal_of_num' 'const/num/0')) & ('const/extreal/extreal_lt' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/mul_lt_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/mul_let_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/mul_lte_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0'))) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/le_rmul_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') z) & ('const/extreal/extreal_le' x y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' x z) ('const/extreal/extreal_mul' y z))))).
tt('thm/extreal/le_lmul_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') z) & ('const/extreal/extreal_le' x y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' z x) ('const/extreal/extreal_mul' z y))))).
tt('thm/extreal/lt_rmul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') z) & (~ (z = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x z) ('const/extreal/extreal_mul' y z)) = ('const/extreal/extreal_lt' x y))))).
tt('thm/extreal/lt_lmul_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_mul' x z)) = ('const/extreal/extreal_lt' y z))))).
tt('thm/extreal/lt_mul2_', ax, (![x1 : 'type/extreal/extreal', x2 : 'type/extreal/extreal', y1 : 'type/extreal/extreal', y2 : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x1) & (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y1) & ((~ (x1 = 'const/extreal/PosInf')) & ((~ (y1 = 'const/extreal/PosInf')) & (('const/extreal/extreal_lt' x1 x2) & ('const/extreal/extreal_lt' y1 y2)))))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x1 y1) ('const/extreal/extreal_mul' x2 y2))))).
tt('thm/extreal/abs_pos_', ax, (![x : 'type/extreal/extreal']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_abs' x)))).
tt('thm/extreal/abs_refl_', ax, (![x : 'type/extreal/extreal']: ((('const/extreal/extreal_abs' x) = x) = ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x)))).
tt('thm/extreal/abs_bounds_', ax, (![x : 'type/extreal/extreal', k : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_abs' x) k) = (('const/extreal/extreal_le' ('const/extreal/extreal_ainv' k) x) & ('const/extreal/extreal_le' x k))))).
tt('thm/extreal/abs_bounds_lt_', ax, (![x : 'type/extreal/extreal', k : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_abs' x) k) = (('const/extreal/extreal_lt' ('const/extreal/extreal_ainv' k) x) & ('const/extreal/extreal_lt' x k))))).
tt('thm/extreal/add_comm_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_add' x y) = ('const/extreal/extreal_add' y x)))).
tt('thm/extreal/add_assoc_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_add' x ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_add' x y) z)))).
tt('thm/extreal/add_not_infty_0', ax, (![y : 'type/extreal/extreal', x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/NegInf'))) => (~ (('const/extreal/extreal_add' x y) = 'const/extreal/NegInf'))))).
tt('thm/extreal/add_not_infty_e1', ax, (![y : 'type/extreal/extreal', x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/PosInf')) & (~ (y = 'const/extreal/PosInf'))) => (~ (('const/extreal/extreal_add' x y) = 'const/extreal/PosInf'))))).
tt('thm/extreal/add_rzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_add' x ('const/extreal/extreal_of_num' 'const/num/0')) = x))).
tt('thm/extreal/add_lzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_add' ('const/extreal/extreal_of_num' 'const/num/0') x) = x))).
tt('thm/extreal/add_infty_tLL', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_add' x 'const/extreal/PosInf') = 'const/extreal/PosInf'))).
tt('thm/extreal/add_infty_tRL', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_add' 'const/extreal/PosInf' x) = 'const/extreal/PosInf'))).
tt('thm/extreal/add_infty_e1', ax, (![x : 'type/extreal/extreal']: ((~ (x = 'const/extreal/PosInf')) => ((('const/extreal/extreal_add' x 'const/extreal/NegInf') = 'const/extreal/NegInf') & (('const/extreal/extreal_add' 'const/extreal/NegInf' x) = 'const/extreal/NegInf'))))).
tt('thm/extreal/EXTREAL_EQ_LADD_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => ((('const/extreal/extreal_add' x y) = ('const/extreal/extreal_add' x z)) = (y = z))))).
tt('thm/extreal/sub_rzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_sub' x ('const/extreal/extreal_of_num' 'const/num/0')) = x))).
tt('thm/extreal/sub_lzero_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_sub' ('const/extreal/extreal_of_num' 'const/num/0') x) = ('const/extreal/extreal_ainv' x)))).
tt('thm/extreal/sub_le_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ('const/extreal/extreal_le' y ('const/extreal/extreal_add' z x)))) => ('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z)))).
tt('thm/extreal/sub_le_imp2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/PosInf')) & ('const/extreal/extreal_le' y ('const/extreal/extreal_add' z x)))) => ('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z)))).
tt('thm/extreal/le_sub_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_add' y x) z) => ('const/extreal/extreal_le' y ('const/extreal/extreal_sub' z x))))).
tt('thm/extreal/lt_sub_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_add' y x) z) => ('const/extreal/extreal_lt' y ('const/extreal/extreal_sub' z x))))).
tt('thm/extreal/sub_lt_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ('const/extreal/extreal_lt' y ('const/extreal/extreal_add' z x)))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_sub' y x) z)))).
tt('thm/extreal/sub_lt_imp2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (z = 'const/extreal/NegInf')) & ((~ (z = 'const/extreal/PosInf')) & ('const/extreal/extreal_lt' y ('const/extreal/extreal_add' z x)))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_sub' y x) z)))).
tt('thm/extreal/sub_zero_lt_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_sub' y x))))).
tt('thm/extreal/sub_zero_lt2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_sub' y x)))) => ('const/extreal/extreal_lt' x y)))).
tt('thm/extreal/sub_lt_zero_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) => ('const/extreal/extreal_lt' ('const/extreal/extreal_sub' x y) ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/sub_lt_zero2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/PosInf')) & ('const/extreal/extreal_lt' ('const/extreal/extreal_sub' x y) ('const/extreal/extreal_of_num' 'const/num/0')))) => ('const/extreal/extreal_lt' x y)))).
tt('thm/extreal/sub_zero_le_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' x y) = ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_sub' y x))))).
tt('thm/extreal/sub_le_zero_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' x y) = ('const/extreal/extreal_le' ('const/extreal/extreal_sub' x y) ('const/extreal/extreal_of_num' 'const/num/0')))))).
tt('thm/extreal/le_sub_eq_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' y ('const/extreal/extreal_sub' z x)) = ('const/extreal/extreal_le' ('const/extreal/extreal_add' y x) z))))).
tt('thm/extreal/le_sub_eq2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (z = 'const/extreal/NegInf')) & ((~ (z = 'const/extreal/PosInf')) & ((~ (x = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/NegInf'))))) => (('const/extreal/extreal_le' y ('const/extreal/extreal_sub' z x)) = ('const/extreal/extreal_le' ('const/extreal/extreal_add' y x) z))))).
tt('thm/extreal/sub_le_eq_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z) = ('const/extreal/extreal_le' y ('const/extreal/extreal_add' z x)))))).
tt('thm/extreal/sub_le_eq2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/PosInf')) & ((~ (x = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/NegInf'))))) => (('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z) = ('const/extreal/extreal_le' y ('const/extreal/extreal_add' z x)))))).
tt('thm/extreal/sub_le_switch_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ((~ (z = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/PosInf'))))) => (('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z) = ('const/extreal/extreal_le' ('const/extreal/extreal_sub' y z) x))))).
tt('thm/extreal/sub_le_switch2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))))) => (('const/extreal/extreal_le' ('const/extreal/extreal_sub' y x) z) = ('const/extreal/extreal_le' ('const/extreal/extreal_sub' y z) x))))).
tt('thm/extreal/lt_sub_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (z = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/PosInf'))) => (('const/extreal/extreal_lt' ('const/extreal/extreal_add' y x) z) = ('const/extreal/extreal_lt' y ('const/extreal/extreal_sub' z x)))))).
tt('thm/extreal/sub_add2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_add' x ('const/extreal/extreal_sub' y x)) = y)))).
tt('thm/extreal/add_sub_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (('const/extreal/extreal_sub' ('const/extreal/extreal_add' x y) y) = x)))).
tt('thm/extreal/add_sub2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (('const/extreal/extreal_sub' ('const/extreal/extreal_add' y x) y) = x)))).
tt('thm/extreal/sub_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (('const/extreal/extreal_add' ('const/extreal/extreal_sub' x y) y) = x)))).
tt('thm/extreal/extreal_sub_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_sub' x y) = ('const/extreal/extreal_add' x ('const/extreal/extreal_ainv' y))))).
tt('thm/extreal/sub_0_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_sub' x y) = ('const/extreal/extreal_of_num' 'const/num/0')) => (x = y)))).
tt('thm/extreal/neg_neg_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_ainv' ('const/extreal/extreal_ainv' x)) = x))).
tt('thm/extreal/neg_0_', ax, (('const/extreal/extreal_ainv' ('const/extreal/extreal_of_num' 'const/num/0')) = ('const/extreal/extreal_of_num' 'const/num/0'))).
tt('thm/extreal/neg_eq0_', ax, (![x : 'type/extreal/extreal']: ((('const/extreal/extreal_ainv' x) = ('const/extreal/extreal_of_num' 'const/num/0')) = (x = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/eq_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_ainv' x) = ('const/extreal/extreal_ainv' y)) = (x = y)))).
tt('thm/extreal/neg_minus1_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_ainv' x) = ('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))).
tt('thm/extreal/sub_rneg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_sub' x ('const/extreal/extreal_ainv' y)) = ('const/extreal/extreal_add' x y)))).
tt('thm/extreal/sub_lneg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((((~ (x = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/NegInf'))) | ((~ (x = 'const/extreal/PosInf')) & (~ (y = 'const/extreal/PosInf')))) => (('const/extreal/extreal_sub' ('const/extreal/extreal_ainv' x) y) = ('const/extreal/extreal_ainv' ('const/extreal/extreal_add' x y)))))).
tt('thm/extreal/neg_sub_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) | ((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf')))) => (('const/extreal/extreal_ainv' ('const/extreal/extreal_sub' x y)) = ('const/extreal/extreal_sub' y x))))).
tt('thm/extreal/sub_not_infty_0', ax, (![y : 'type/extreal/extreal', x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => (~ (('const/extreal/extreal_sub' x y) = 'const/extreal/NegInf'))))).
tt('thm/extreal/sub_not_infty_e1', ax, (![y : 'type/extreal/extreal', x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/PosInf')) & (~ (y = 'const/extreal/NegInf'))) => (~ (('const/extreal/extreal_sub' x y) = 'const/extreal/PosInf'))))).
tt('thm/extreal/le_lsub_imp_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_le' y z) => ('const/extreal/extreal_le' ('const/extreal/extreal_sub' x z) ('const/extreal/extreal_sub' x y))))).
tt('thm/extreal/eq_sub_ladd_normal_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/realax/real']: ((x = ('const/extreal/extreal_sub' y ('const/extreal/Normal' z))) = (('const/extreal/extreal_add' x ('const/extreal/Normal' z)) = y)))).
tt('thm/extreal/eq_sub_radd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))) => ((('const/extreal/extreal_sub' x y) = z) = (x = ('const/extreal/extreal_add' z y)))))).
tt('thm/extreal/eq_sub_ladd_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (z = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/PosInf'))) => ((x = ('const/extreal/extreal_sub' y z)) = (('const/extreal/extreal_add' x z) = y))))).
tt('thm/extreal/eq_sub_switch_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/realax/real']: ((x = ('const/extreal/extreal_sub' ('const/extreal/Normal' z) y)) = (y = ('const/extreal/extreal_sub' ('const/extreal/Normal' z) x))))).
tt('thm/extreal/eq_add_sub_switch_', ax, (![a : 'type/extreal/extreal', b : 'type/extreal/extreal', c : 'type/extreal/extreal', d : 'type/extreal/extreal']: (((~ (b = 'const/extreal/NegInf')) & ((~ (b = 'const/extreal/PosInf')) & ((~ (c = 'const/extreal/NegInf')) & (~ (c = 'const/extreal/PosInf'))))) => ((('const/extreal/extreal_add' a b) = ('const/extreal/extreal_add' c d)) = (('const/extreal/extreal_sub' a c) = ('const/extreal/extreal_sub' d b)))))).
tt('thm/extreal/sub_refl_', ax, (![x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => (('const/extreal/extreal_sub' x x) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/mul_comm_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x y) = ('const/extreal/extreal_mul' y x)))).
tt('thm/extreal/mul_assoc_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x ('const/extreal/extreal_mul' y z)) = ('const/extreal/extreal_mul' ('const/extreal/extreal_mul' x y) z)))).
tt('thm/extreal/mul_not_infty_0', ax, (![c : 'type/realax/real', y : 'type/extreal/extreal']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) & (~ (y = 'const/extreal/NegInf'))) => (~ (('const/extreal/extreal_mul' ('const/extreal/Normal' c) y) = 'const/extreal/NegInf'))))).
tt('thm/extreal/mul_not_infty_1', ax, (![c : 'type/realax/real', y : 'type/extreal/extreal']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) & (~ (y = 'const/extreal/PosInf'))) => (~ (('const/extreal/extreal_mul' ('const/extreal/Normal' c) y) = 'const/extreal/PosInf'))))).
tt('thm/extreal/mul_not_infty_2', ax, (![c : 'type/realax/real', y : 'type/extreal/extreal']: ((('const/real/real_lte' c ('const/real/real_of_num' 'const/num/0')) & (~ (y = 'const/extreal/NegInf'))) => (~ (('const/extreal/extreal_mul' ('const/extreal/Normal' c) y) = 'const/extreal/PosInf'))))).
tt('thm/extreal/mul_not_infty_e3', ax, (![c : 'type/realax/real', y : 'type/extreal/extreal']: ((('const/real/real_lte' c ('const/real/real_of_num' 'const/num/0')) & (~ (y = 'const/extreal/PosInf'))) => (~ (('const/extreal/extreal_mul' ('const/extreal/Normal' c) y) = 'const/extreal/NegInf'))))).
tt('thm/extreal/mul_not_infty2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ((~ (y = 'const/extreal/NegInf')) & (~ (y = 'const/extreal/PosInf'))))) => ((~ (('const/extreal/extreal_mul' x y) = 'const/extreal/NegInf')) & (~ (('const/extreal/extreal_mul' x y) = 'const/extreal/PosInf')))))).
tt('thm/extreal/add_ldistrib_pos_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') z)) => (('const/extreal/extreal_mul' x ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_mul' x z)))))).
tt('thm/extreal/add_ldistrib_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0')) & ('const/extreal/extreal_le' z ('const/extreal/extreal_of_num' 'const/num/0'))) => (('const/extreal/extreal_mul' x ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_mul' x z)))))).
tt('thm/extreal/add_ldistrib_normal_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((((~ (y = 'const/extreal/PosInf')) & (~ (z = 'const/extreal/PosInf'))) | ((~ (y = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/NegInf')))) => (('const/extreal/extreal_mul' ('const/extreal/Normal' x) ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' ('const/extreal/Normal' x) y) ('const/extreal/extreal_mul' ('const/extreal/Normal' x) z)))))).
tt('thm/extreal/add_ldistrib_normal2_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/extreal/extreal_mul' ('const/extreal/Normal' x) ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' ('const/extreal/Normal' x) y) ('const/extreal/extreal_mul' ('const/extreal/Normal' x) z)))))).
tt('thm/extreal/add_rdistrib_normal_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: ((((~ (y = 'const/extreal/PosInf')) & (~ (z = 'const/extreal/PosInf'))) | ((~ (y = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/NegInf')))) => (('const/extreal/extreal_mul' ('const/extreal/extreal_add' y z) ('const/extreal/Normal' x)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' y ('const/extreal/Normal' x)) ('const/extreal/extreal_mul' z ('const/extreal/Normal' x))))))).
tt('thm/extreal/add_rdistrib_normal2_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/extreal/extreal_mul' ('const/extreal/extreal_add' y z) ('const/extreal/Normal' x)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' y ('const/extreal/Normal' x)) ('const/extreal/extreal_mul' z ('const/extreal/Normal' x))))))).
tt('thm/extreal/add_ldistrib_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') z)) | (('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0')) & ('const/extreal/extreal_le' z ('const/extreal/extreal_of_num' 'const/num/0')))) => (('const/extreal/extreal_mul' x ('const/extreal/extreal_add' y z)) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_mul' x z)))))).
tt('thm/extreal/add_rdistrib_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') y) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') z)) | (('const/extreal/extreal_le' y ('const/extreal/extreal_of_num' 'const/num/0')) & ('const/extreal/extreal_le' z ('const/extreal/extreal_of_num' 'const/num/0')))) => (('const/extreal/extreal_mul' ('const/extreal/extreal_add' y z) x) = ('const/extreal/extreal_add' ('const/extreal/extreal_mul' y x) ('const/extreal/extreal_mul' z x)))))).
tt('thm/extreal/mul_lneg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' x) y) = ('const/extreal/extreal_ainv' ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/mul_rneg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_mul' x ('const/extreal/extreal_ainv' y)) = ('const/extreal/extreal_ainv' ('const/extreal/extreal_mul' x y))))).
tt('thm/extreal/neg_mul2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' x) ('const/extreal/extreal_ainv' y)) = ('const/extreal/extreal_mul' x y)))).
tt('thm/extreal/add2_sub2_', ax, (![a : 'type/extreal/extreal', b : 'type/extreal/extreal', c : 'type/extreal/extreal', d : 'type/extreal/extreal']: ((((~ (b = 'const/extreal/PosInf')) & (~ (d = 'const/extreal/PosInf'))) | ((~ (b = 'const/extreal/NegInf')) & (~ (d = 'const/extreal/NegInf')))) => (('const/extreal/extreal_add' ('const/extreal/extreal_sub' a b) ('const/extreal/extreal_sub' c d)) = ('const/extreal/extreal_sub' ('const/extreal/extreal_add' a c) ('const/extreal/extreal_add' b d)))))).
tt('thm/extreal/sub_ldistrib_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ((~ (y = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/PosInf')) & ((~ (z = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/PosInf'))))))) => (('const/extreal/extreal_mul' x ('const/extreal/extreal_sub' y z)) = ('const/extreal/extreal_sub' ('const/extreal/extreal_mul' x y) ('const/extreal/extreal_mul' x z)))))).
tt('thm/extreal/sub_rdistrib_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (x = 'const/extreal/PosInf')) & ((~ (y = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/PosInf')) & ((~ (z = 'const/extreal/NegInf')) & (~ (z = 'const/extreal/PosInf'))))))) => (('const/extreal/extreal_mul' ('const/extreal/extreal_sub' x y) z) = ('const/extreal/extreal_sub' ('const/extreal/extreal_mul' x z) ('const/extreal/extreal_mul' y z)))))).
tt('thm/extreal/extreal_div_eq_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/extreal/extreal_div' ('const/extreal/Normal' x) ('const/extreal/Normal' y)) = ('const/extreal/Normal' ('const/real/#slash#' x y))))).
tt('thm/extreal/inv_one_', ax, (('const/extreal/extreal_inv' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/inv_1over_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_inv' x) = ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x)))).
tt('thm/extreal/div_one_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_div' x ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = x))).
tt('thm/extreal/inv_pos_', ax, (![x : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) & (~ (x = 'const/extreal/PosInf'))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x))))).
tt('thm/extreal/rinv_uniq_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_mul' x y) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (y = ('const/extreal/extreal_inv' x))))).
tt('thm/extreal/linv_uniq_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_mul' x y) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (x = ('const/extreal/extreal_inv' y))))).
tt('thm/extreal/le_rdiv_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/extreal/extreal_le' ('const/extreal/extreal_mul' y ('const/extreal/Normal' x)) z) = ('const/extreal/extreal_le' y ('const/extreal/extreal_div' z ('const/extreal/Normal' x))))))).
tt('thm/extreal/le_ldiv_', ax, (![x : 'type/realax/real', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/extreal/extreal_le' y ('const/extreal/extreal_mul' z ('const/extreal/Normal' x))) = ('const/extreal/extreal_le' ('const/extreal/extreal_div' y ('const/extreal/Normal' x)) z))))).
tt('thm/extreal/lt_rdiv_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/extreal/extreal_lt' x ('const/extreal/extreal_div' y ('const/extreal/Normal' z))) = ('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x ('const/extreal/Normal' z)) y))))).
tt('thm/extreal/lt_ldiv_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/extreal/extreal_lt' ('const/extreal/extreal_div' x ('const/extreal/Normal' z)) y) = ('const/extreal/extreal_lt' x ('const/extreal/extreal_mul' y ('const/extreal/Normal' z))))))).
tt('thm/extreal/lt_rdiv_neg_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/realax/real']: (('const/realax/real_lt' z ('const/real/real_of_num' 'const/num/0')) => (('const/extreal/extreal_lt' ('const/extreal/extreal_div' y ('const/extreal/Normal' z)) x) = ('const/extreal/extreal_lt' ('const/extreal/extreal_mul' x ('const/extreal/Normal' z)) y))))).
tt('thm/extreal/div_add_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal', z : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & ((~ (y = 'const/extreal/NegInf')) & (~ (z = ('const/extreal/extreal_of_num' 'const/num/0'))))) => (('const/extreal/extreal_add' ('const/extreal/extreal_div' x z) ('const/extreal/extreal_div' y z)) = ('const/extreal/extreal_div' ('const/extreal/extreal_add' x y) z))))).
tt('thm/extreal/le_inv_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_inv' x))))).
tt('thm/extreal/pow_0_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_pow' x 'const/num/0') = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/pow_1_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x))).
tt('thm/extreal/pow_2_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/extreal/extreal_mul' x x)))).
tt('thm/extreal/pow_zero_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal']: ((('const/extreal/extreal_pow' x ('const/num/SUC' n)) = ('const/extreal/extreal_of_num' 'const/num/0')) = (x = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/pow_zero_imp_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal']: ((('const/extreal/extreal_pow' x n) = ('const/extreal/extreal_of_num' 'const/num/0')) => (x = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/le_pow2_', ax, (![x : 'type/extreal/extreal']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/pow_pos_le_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) => (![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_pow' x n)))))).
tt('thm/extreal/pow_pos_lt_', ax, (![x : 'type/extreal/extreal', n : 'type/num/num']: (('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_pow' x n))))).
tt('thm/extreal/pow_le_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' x y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_pow' y n))))).
tt('thm/extreal/pow_lt_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' x y)) => ('const/extreal/extreal_lt' ('const/extreal/extreal_pow' x ('const/num/SUC' n)) ('const/extreal/extreal_pow' y ('const/num/SUC' n)))))).
tt('thm/extreal/pow_lt2_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((~ (n = 'const/num/0')) & (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' x y))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_pow' y n))))).
tt('thm/extreal/pow_le_mono_', ax, (![x : 'type/extreal/extreal', n : 'type/num/num', m : 'type/num/num']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) & ('const/arithmetic/<=' n m)) => ('const/extreal/extreal_le' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_pow' x m))))).
tt('thm/extreal/pow_pos_even_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x ('const/extreal/extreal_of_num' 'const/num/0')) => (('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_pow' x n)) = ('const/arithmetic/EVEN' n))))).
tt('thm/extreal/pow_neg_odd_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x ('const/extreal/extreal_of_num' 'const/num/0')) => (('const/extreal/extreal_lt' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_of_num' 'const/num/0')) = ('const/arithmetic/ODD' n))))).
tt('thm/extreal/add_pow2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_pow' ('const/extreal/extreal_add' x y) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/extreal/extreal_add' ('const/extreal/extreal_add' ('const/extreal/extreal_pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_pow' y ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_mul' ('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x) y))))).
tt('thm/extreal/pow_add_', ax, (![x : 'type/extreal/extreal', n : 'type/num/num', m : 'type/num/num']: (('const/extreal/extreal_pow' x ('const/arithmetic/+' n m)) = ('const/extreal/extreal_mul' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_pow' x m))))).
tt('thm/extreal/pow_mul_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_pow' ('const/extreal/extreal_mul' x y) n) = ('const/extreal/extreal_mul' ('const/extreal/extreal_pow' x n) ('const/extreal/extreal_pow' y n))))).
tt('thm/extreal/pow_minus1_', ax, (![n : 'type/num/num']: (('const/extreal/extreal_pow' ('const/extreal/extreal_ainv' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/pow_not_infty_', ax, (![n : 'type/num/num', x : 'type/extreal/extreal']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => ((~ (('const/extreal/extreal_pow' x n) = 'const/extreal/NegInf')) & (~ (('const/extreal/extreal_pow' x n) = 'const/extreal/PosInf')))))).
tt('thm/extreal/sqrt_pos_le_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_sqrt' x))))).
tt('thm/extreal/sqrt_pos_lt_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_sqrt' x))))).
tt('thm/extreal/pow2_sqrt_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) => (('const/extreal/extreal_sqrt' ('const/extreal/extreal_pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = x)))).
tt('thm/extreal/sqrt_pow2_', ax, (![x : 'type/extreal/extreal']: ((('const/extreal/extreal_pow' ('const/extreal/extreal_sqrt' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = x) = ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x)))).
tt('thm/extreal/sqrt_mono_le_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_le' x y)) => ('const/extreal/extreal_le' ('const/extreal/extreal_sqrt' x) ('const/extreal/extreal_sqrt' y))))).
tt('thm/extreal/logr_not_infty_', ax, (![x : 'type/extreal/extreal', b : 'type/realax/real']: (((~ (x = 'const/extreal/NegInf')) & (~ (x = 'const/extreal/PosInf'))) => ((~ (('const/extreal/extreal_logr' b x) = 'const/extreal/NegInf')) & (~ (('const/extreal/extreal_logr' b x) = 'const/extreal/PosInf')))))).
tt('thm/extreal/half_between_tLL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/half_between_tRL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/half_between_1', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/extreal/half_between_e2', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/thirds_between_tLLL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/thirds_between_tRLL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/thirds_between_tLRL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/thirds_between_tRRL', ax, ('const/extreal/extreal_lt' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/thirds_between_tLLR', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/thirds_between_tRLR', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/thirds_between_2', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/thirds_between_e3', ax, ('const/extreal/extreal_le' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/half_cancel_', ax, (('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/third_cancel_', ax, (('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/fourth_cancel_', ax, (('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/extreal/quotient_normal_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/extreal/extreal_div' ('const/extreal/extreal_of_num' n) ('const/extreal/extreal_of_num' m)) = ('const/extreal/Normal' ('const/real/#slash#' ('const/real/real_of_num' n) ('const/real/real_of_num' m)))))).
tt('thm/extreal/ext_mono_increasing_def_', def, (![f : ('type/num/num' > 'type/extreal/extreal')]: (('const/extreal/ext_mono_increasing' f) = (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/extreal/extreal_le' (f m) (f n))))))).
tt('thm/extreal/ext_mono_increasing_suc_', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: (('const/extreal/ext_mono_increasing' f) = (![n : 'type/num/num']: ('const/extreal/extreal_le' (f n) (f ('const/num/SUC' n))))))).
tt('thm/extreal/ext_mono_decreasing_def_', def, (![f : ('type/num/num' > 'type/extreal/extreal')]: (('const/extreal/ext_mono_decreasing' f) = (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/extreal/extreal_le' (f n) (f m))))))).
tt('thm/extreal/ext_mono_decreasing_suc_', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: (('const/extreal/ext_mono_decreasing' f) = (![n : 'type/num/num']: ('const/extreal/extreal_le' (f ('const/num/SUC' n)) (f n)))))).
tt('thm/extreal/EXTREAL_ARCH_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') x) => (![y : 'type/extreal/extreal']: ((~ (y = 'const/extreal/PosInf')) => (?[n : 'type/num/num']: ('const/extreal/extreal_lt' y ('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' n) x)))))))).
tt('thm/extreal/SIMP_REAL_ARCH_', ax, (![x : 'type/realax/real']: (?[n : 'type/num/num']: ('const/real/real_lte' x ('const/real/real_of_num' n))))).
tt('thm/extreal/SIMP_REAL_ARCH_NEG_', ax, (![x : 'type/realax/real']: (?[n : 'type/num/num']: ('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' n)) x)))).
tt('thm/extreal/SIMP_EXTREAL_ARCH_', ax, (![x : 'type/extreal/extreal']: ((~ (x = 'const/extreal/PosInf')) => (?[n : 'type/num/num']: ('const/extreal/extreal_le' x ('const/extreal/extreal_of_num' n)))))).
tt('thm/extreal/REAL_ARCH_POW_', ax, (![x : 'type/realax/real']: (?[n : 'type/num/num']: ('const/realax/real_lt' x ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n))))).
tt('thm/extreal/EXTREAL_ARCH_POW_', ax, (![x : 'type/extreal/extreal']: ((~ (x = 'const/extreal/PosInf')) => (?[n : 'type/num/num']: ('const/extreal/extreal_lt' x ('const/extreal/extreal_pow' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))).
tt('thm/extreal/EXTREAL_ARCH_POW_INV_', ax, (![e : 'type/extreal/extreal']: (('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') e) => (?[n : 'type/num/num']: ('const/extreal/extreal_lt' ('const/extreal/Normal' ('const/real/pow' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) n)) e))))).
tt('thm/extreal/REAL_LE_MUL_EPSILON_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((![z : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) & ('const/realax/real_lt' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/real/real_lte' ('const/realax/real_mul' z x) y))) => ('const/real/real_lte' x y)))).
tt('thm/extreal/le_epsilon_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((![e : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') e) & (~ (e = 'const/extreal/PosInf'))) => ('const/extreal/extreal_le' x ('const/extreal/extreal_add' y e)))) => ('const/extreal/extreal_le' x y)))).
tt('thm/extreal/le_mul_epsilon_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((![z : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') z) & ('const/extreal/extreal_lt' z ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/extreal/extreal_le' ('const/extreal/extreal_mul' z x) y))) => ('const/extreal/extreal_le' x y)))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_DEF_', def, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = (('const/pred_set/ITSET' A 'type/extreal/extreal') (^[e : A, acc : 'type/extreal/extreal']: ('const/extreal/extreal_add' (f e) acc)) s ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_THM_0', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f ('const/pred_set/EMPTY' A)) = ('const/extreal/extreal_of_num' 'const/num/0')))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_THM_e1', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), e : A, s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/INSERT' A) e s)) = ('const/extreal/extreal_add' (f e) (('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/DELETE' A) s e))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_NOT_NEG_INF_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (~ ((f x) = 'const/extreal/NegInf'))))) => (~ ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = 'const/extreal/NegInf'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_NOT_POS_INF_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (~ ((f x) = 'const/extreal/PosInf'))))) => (~ ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = 'const/extreal/PosInf'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_NOT_INFTY_0', ax, ![A : $t]: (![s : (A > $o), f : (A > 'type/extreal/extreal')]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (~ ((f x) = 'const/extreal/NegInf'))))) => (~ ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = 'const/extreal/NegInf'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_NOT_INFTY_e1', ax, ![A : $t]: (![s : (A > $o), f : (A > 'type/extreal/extreal')]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (~ ((f x) = 'const/extreal/PosInf'))))) => (~ ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = 'const/extreal/PosInf'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_SING_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), e : A]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/INSERT' A) e ('const/pred_set/EMPTY' A))) = (f e)))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_POS_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (('const/extreal/EXTREAL_SUM_IMAGE' A) f s))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_SPOS_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & ((~ (s = ('const/pred_set/EMPTY' A))) & (![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') (f x)))))) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') (('const/extreal/EXTREAL_SUM_IMAGE' A) f s))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_IF_ELIM_', ax, ![A : $t]: (![s : (A > $o), P : (A > $o), f : (A > 'type/extreal/extreal')]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (P x)))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (P x) (f x) ('const/extreal/extreal_of_num' 'const/num/0'))) s) = (('const/extreal/EXTREAL_SUM_IMAGE' A) f s))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_FINITE_SAME_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), p : A]: (((('const/bool/IN' A) p s) & (![q : A]: ((('const/bool/IN' A) q s) => ((f p) = (f q))))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = ('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' (('const/pred_set/CARD' A) s)) (f p)))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_FINITE_CONST_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/pred_set/FINITE' A) P) => (![f : (A > 'type/extreal/extreal'), x : 'type/extreal/extreal']: ((![y : A]: ((f y) = x)) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f P) = ('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' (('const/pred_set/CARD' A) P)) x))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_ZERO_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_of_num' 'const/num/0')) s) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_0_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => ((f x) = ('const/extreal/extreal_of_num' 'const/num/0'))))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = ('const/extreal/extreal_of_num' 'const/num/0'))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_IN_IF_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = (('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (('const/bool/IN' A) x s) (f x) ('const/extreal/extreal_of_num' 'const/num/0'))) s)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_CMUL_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) | (![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x))) s) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/extreal/EXTREAL_SUM_IMAGE' A) f s)))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_CMUL2_', ax, ![A : $t]: (![s : (A > $o), f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => (~ ((f x) = 'const/extreal/NegInf'))))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f x))) s) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (('const/extreal/EXTREAL_SUM_IMAGE' A) f s)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_IMAGE_', ax, ![A : $t, B : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (!['f\'' : (A > B)]: ((('const/pred_set/INJ' A B) 'f\'' s (('const/pred_set/IMAGE' A B) 'f\'' s)) => (![f : (B > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' B) f (('const/pred_set/IMAGE' A B) 'f\'' s)) = (('const/extreal/EXTREAL_SUM_IMAGE' A) (('const/combin/o' A 'type/extreal/extreal' B) f 'f\'') s)))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_DISJOINT_UNION_', ax, ![A : $t]: (![s : (A > $o), 's\'' : (A > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/pred_set/FINITE' A) 's\'') & (('const/pred_set/DISJOINT' A) s 's\''))) => (![f : (A > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/UNION' A) s 's\'')) = ('const/extreal/extreal_add' (('const/extreal/EXTREAL_SUM_IMAGE' A) f s) (('const/extreal/EXTREAL_SUM_IMAGE' A) f 's\''))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_EQ_CARD_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[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'))) s) = ('const/extreal/extreal_of_num' (('const/pred_set/CARD' A) s)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_INV_CARD_EQ_1_', ax, ![A : $t]: (![s : (A > $o)]: (((~ (s = ('const/pred_set/EMPTY' A))) & (('const/pred_set/FINITE' A) s)) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (('const/bool/IN' A) x s) ('const/extreal/extreal_inv' ('const/extreal/extreal_of_num' (('const/pred_set/CARD' A) s))) ('const/extreal/extreal_of_num' 'const/num/0'))) s) = ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_INTER_NONZERO_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/INTER' A) s (^[p : A]: (~ ((f p) = ('const/extreal/extreal_of_num' 'const/num/0')))))) = (('const/extreal/EXTREAL_SUM_IMAGE' A) f s)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_INTER_ELIM_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), 's\'' : (A > $o)]: ((![x : A]: ((~ (('const/bool/IN' A) x 's\'')) => ((f x) = ('const/extreal/extreal_of_num' 'const/num/0')))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/INTER' A) s 's\'')) = (('const/extreal/EXTREAL_SUM_IMAGE' A) f s))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_ZERO_DIFF_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), t : (A > $o)]: ((![x : A]: ((('const/bool/IN' A) x t) => ((f x) = ('const/extreal/extreal_of_num' 'const/num/0')))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = (('const/extreal/EXTREAL_SUM_IMAGE' A) f (('const/pred_set/DIFF' A) s t)))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_MONO_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), 'f\'' : (A > 'type/extreal/extreal')]: ((![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_le' (f x) ('f\'' x)))) => ('const/extreal/extreal_le' (('const/extreal/EXTREAL_SUM_IMAGE' A) f s) (('const/extreal/EXTREAL_SUM_IMAGE' A) 'f\'' s))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_MONO_SET_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o), t : (A > $o)]: (((('const/pred_set/FINITE' A) s) & ((('const/pred_set/FINITE' A) t) & ((('const/pred_set/SUBSET' A) s t) & (![x : A]: ((('const/bool/IN' A) x t) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))))) => ('const/extreal/extreal_le' (('const/extreal/EXTREAL_SUM_IMAGE' A) f s) (('const/extreal/EXTREAL_SUM_IMAGE' A) f t))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_EQ_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), 'f\'' : (A > 'type/extreal/extreal')]: ((![x : A]: ((('const/bool/IN' A) x s) => ((f x) = ('f\'' x)))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = (('const/extreal/EXTREAL_SUM_IMAGE' A) 'f\'' s))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_POS_MEM_LE_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), s : (A > $o)]: (((('const/pred_set/FINITE' A) s) & (![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f x))))) => (![x : A]: ((('const/bool/IN' A) x s) => ('const/extreal/extreal_le' (f x) (('const/extreal/EXTREAL_SUM_IMAGE' A) f s))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_ADD_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), 'f\'' : (A > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_add' (f x) ('f\'' x))) s) = ('const/extreal/extreal_add' (('const/extreal/EXTREAL_SUM_IMAGE' A) f s) (('const/extreal/EXTREAL_SUM_IMAGE' A) 'f\'' s))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_SUB_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => (![f : (A > 'type/extreal/extreal'), 'f\'' : (A > 'type/extreal/extreal')]: (((![x : A]: ((('const/bool/IN' A) x s) => (~ (('f\'' x) = 'const/extreal/NegInf')))) | (![x : A]: ((('const/bool/IN' A) x s) => (~ (('f\'' x) = 'const/extreal/PosInf'))))) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/extreal_sub' (f x) ('f\'' x))) s) = ('const/extreal/extreal_sub' (('const/extreal/EXTREAL_SUM_IMAGE' A) f s) (('const/extreal/EXTREAL_SUM_IMAGE' A) 'f\'' s)))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_EXTREAL_SUM_IMAGE_', ax, ![B : $t, A : $t]: (![s : (A > $o), 's\'' : (B > $o), f : (A > (B > 'type/extreal/extreal'))]: (((('const/pred_set/FINITE' A) s) & (('const/pred_set/FINITE' B) 's\'')) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: (('const/extreal/EXTREAL_SUM_IMAGE' B) (f x) 's\'')) s) = (('const/extreal/EXTREAL_SUM_IMAGE' ('type/pair/prod' A B)) (^[x : ('type/pair/prod' A B)]: (f (('const/pair/FST' A B) x) (('const/pair/SND' A B) x))) (('const/pred_set/CROSS' A B) s 's\'')))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_NORMAL_', ax, ![A : $t]: (![f : (A > 'type/realax/real'), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: ('const/extreal/Normal' (f x))) s) = ('const/extreal/Normal' (('const/real_sigma/REAL_SUM_IMAGE' A) f s)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_IN_IF_ALT_', ax, ![A : $t]: (![s : (A > $o), f : (A > 'type/extreal/extreal'), z : 'type/extreal/extreal']: ((('const/pred_set/FINITE' A) s) => ((('const/extreal/EXTREAL_SUM_IMAGE' A) f s) = (('const/extreal/EXTREAL_SUM_IMAGE' A) (^[x : A]: (('const/bool/COND' 'type/extreal/extreal') (('const/bool/IN' A) x s) (f x) z)) s))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_CROSS_SYM_', ax, ![A : $t, B : $t]: (![f : (('type/pair/prod' A B) > 'type/extreal/extreal'), s1 : (A > $o), s2 : (B > $o)]: (((('const/pred_set/FINITE' A) s1) & (('const/pred_set/FINITE' B) s2)) => ((('const/extreal/EXTREAL_SUM_IMAGE' ('type/pair/prod' A B)) (('const/pair/UNCURRY' A B 'type/extreal/extreal') (^[x : A, y : B]: (f (('const/pair/,' A B) x y)))) (('const/pred_set/CROSS' A B) s1 s2)) = (('const/extreal/EXTREAL_SUM_IMAGE' ('type/pair/prod' B A)) (('const/pair/UNCURRY' B A 'type/extreal/extreal') (^[y : B, x : A]: (f (('const/pair/,' A B) x y)))) (('const/pred_set/CROSS' B A) s2 s1)))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_COUNT_0', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/extreal/extreal_add' (f 'const/num/0') (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_COUNT_1', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/extreal/extreal_add' ('const/extreal/extreal_add' (f 'const/num/0') (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_COUNT_2', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/extreal/extreal_add' ('const/extreal/extreal_add' ('const/extreal/extreal_add' (f 'const/num/0') (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/extreal/EXTREAL_SUM_IMAGE_COUNT_e3', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/extreal/extreal_add' ('const/extreal/extreal_add' ('const/extreal/extreal_add' ('const/extreal/extreal_add' (f 'const/num/0') (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/extreal/extreal_sup_def_', def, (![p : ('type/extreal/extreal' > $o)]: (('const/extreal/extreal_sup' p) = (('const/bool/COND' 'type/extreal/extreal') (![x : 'type/extreal/extreal']: ((![y : 'type/extreal/extreal']: ((p y) => ('const/extreal/extreal_le' y x))) => (x = 'const/extreal/PosInf'))) 'const/extreal/PosInf' (('const/bool/COND' 'type/extreal/extreal') (![x : 'type/extreal/extreal']: ((p x) => (x = 'const/extreal/NegInf'))) 'const/extreal/NegInf' ('const/extreal/Normal' ('const/real/sup' (^[r : 'type/realax/real']: (p ('const/extreal/Normal' r)))))))))).
tt('thm/extreal/extreal_inf_def_', def, (![p : ('type/extreal/extreal' > $o)]: (('const/extreal/extreal_inf' p) = ('const/extreal/extreal_ainv' ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/extreal/extreal' 'type/extreal/extreal') 'const/extreal/extreal_ainv' p)))))).
tt('thm/extreal/le_sup_imp_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_le' x ('const/extreal/extreal_sup' p))))).
tt('thm/extreal/sup_le_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_sup' p) x) = (![y : 'type/extreal/extreal']: ((p y) => ('const/extreal/extreal_le' y x)))))).
tt('thm/extreal/le_sup_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: (('const/extreal/extreal_le' x ('const/extreal/extreal_sup' p)) = (![y : 'type/extreal/extreal']: ((![z : 'type/extreal/extreal']: ((p z) => ('const/extreal/extreal_le' z y))) => ('const/extreal/extreal_le' x y)))))).
tt('thm/extreal/sup_eq_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: ((('const/extreal/extreal_sup' p) = x) = ((![y : 'type/extreal/extreal']: ((p y) => ('const/extreal/extreal_le' y x))) & (![y : 'type/extreal/extreal']: ((![z : 'type/extreal/extreal']: ((p z) => ('const/extreal/extreal_le' z y))) => ('const/extreal/extreal_le' x y))))))).
tt('thm/extreal/sup_const_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_sup' (^[y : 'type/extreal/extreal']: (y = x))) = x))).
tt('thm/extreal/sup_const_alt_', ax, (![p : ('type/extreal/extreal' > $o), z : 'type/extreal/extreal']: (((?[x : 'type/extreal/extreal']: (p x)) & (![x : 'type/extreal/extreal']: ((p x) => (x = z)))) => (('const/extreal/extreal_sup' p) = z)))).
tt('thm/extreal/sup_const_over_set_', ax, ![A : $t]: (![s : (A > $o), k : 'type/extreal/extreal']: ((~ (s = ('const/pred_set/EMPTY' A))) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' A 'type/extreal/extreal') (^[x : A]: k) s)) = k)))).
tt('thm/extreal/sup_num_', ax, (('const/extreal/extreal_sup' (^[x : 'type/extreal/extreal']: (?[n : 'type/num/num']: (x = ('const/extreal/extreal_of_num' n))))) = 'const/extreal/PosInf')).
tt('thm/extreal/sup_le_sup_imp_', ax, (![p : ('type/extreal/extreal' > $o), q : ('type/extreal/extreal' > $o)]: ((![x : 'type/extreal/extreal']: ((p x) => (?[y : 'type/extreal/extreal']: ((q y) & ('const/extreal/extreal_le' x y))))) => ('const/extreal/extreal_le' ('const/extreal/extreal_sup' p) ('const/extreal/extreal_sup' q))))).
tt('thm/extreal/sup_mono_', ax, (![p : ('type/num/num' > 'type/extreal/extreal'), q : ('type/num/num' > 'type/extreal/extreal')]: ((![n : 'type/num/num']: ('const/extreal/extreal_le' (p n) (q n))) => ('const/extreal/extreal_le' ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') p ('const/pred_set/UNIV' 'type/num/num'))) ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') q ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/extreal/sup_suc_', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/extreal/extreal_le' (f m) (f n)))) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (f ('const/num/SUC' n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') f ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/extreal/sup_seq_', ax, (![f : ('type/num/num' > 'type/realax/real'), l : 'type/realax/real']: (('const/extreal/mono_increasing' f) => (('const/seq/-->' f l) = (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: ('const/extreal/Normal' (f n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/Normal' l)))))).
tt('thm/extreal/sup_lt_infty_', ax, (![p : ('type/extreal/extreal' > $o)]: (('const/extreal/extreal_lt' ('const/extreal/extreal_sup' p) 'const/extreal/PosInf') => (![x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_lt' x 'const/extreal/PosInf')))))).
tt('thm/extreal/sup_max_', ax, (![p : ('type/extreal/extreal' > $o), z : 'type/extreal/extreal']: (((p z) & (![x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_le' x z)))) => (('const/extreal/extreal_sup' p) = z)))).
tt('thm/extreal/sup_add_mono_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), g : ('type/num/num' > 'type/extreal/extreal')]: (((![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f n))) & ((![n : 'type/num/num']: ('const/extreal/extreal_le' (f n) (f ('const/num/SUC' n)))) & ((![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g n))) & (![n : 'type/num/num']: ('const/extreal/extreal_le' (g n) (g ('const/num/SUC' n))))))) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: ('const/extreal/extreal_add' (f n) (g n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_add' ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') f ('const/pred_set/UNIV' 'type/num/num'))) ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') g ('const/pred_set/UNIV' 'type/num/num')))))))).
tt('thm/extreal/sup_sum_mono_', ax, (![f : ('type/num/num' > ('type/num/num' > 'type/extreal/extreal')), s : ('type/num/num' > $o)]: (((('const/pred_set/FINITE' 'type/num/num') s) & ((![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i s) => (![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f i n))))) & (![i : 'type/num/num']: ((('const/bool/IN' 'type/num/num') i s) => (![n : 'type/num/num']: ('const/extreal/extreal_le' (f i n) (f i ('const/num/SUC' n)))))))) => (('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: (f i n)) s)) ('const/pred_set/UNIV' 'type/num/num'))) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') (^[i : 'type/num/num']: ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (f i) ('const/pred_set/UNIV' 'type/num/num')))) s))))).
tt('thm/extreal/sup_le_mono_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), z : 'type/extreal/extreal']: (((![n : 'type/num/num']: ('const/extreal/extreal_le' (f n) (f ('const/num/SUC' n)))) & ('const/extreal/extreal_lt' z ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') f ('const/pred_set/UNIV' 'type/num/num'))))) => (?[n : 'type/num/num']: ('const/extreal/extreal_le' z (f n)))))).
tt('thm/extreal/sup_cmul_', 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/extreal/extreal_sup' (('const/pred_set/IMAGE' A 'type/extreal/extreal') (^[n : A]: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f n))) ('const/pred_set/UNIV' A))) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' A 'type/extreal/extreal') f ('const/pred_set/UNIV' A)))))))).
tt('thm/extreal/sup_lt_', ax, (![P : ('type/extreal/extreal' > $o), y : 'type/extreal/extreal']: ((?[x : 'type/extreal/extreal']: ((P x) & ('const/extreal/extreal_lt' y x))) = ('const/extreal/extreal_lt' y ('const/extreal/extreal_sup' P))))).
tt('thm/extreal/sup_lt_epsilon_', ax, (![P : ('type/extreal/extreal' > $o), e : 'type/extreal/extreal']: ((('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') e) & ((?[x : 'type/extreal/extreal']: ((P x) & (~ (x = 'const/extreal/NegInf')))) & (~ (('const/extreal/extreal_sup' P) = 'const/extreal/PosInf')))) => (?[x : 'type/extreal/extreal']: ((P x) & ('const/extreal/extreal_lt' ('const/extreal/extreal_sup' P) ('const/extreal/extreal_add' x e))))))).
tt('thm/extreal/inf_le_imp_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_le' ('const/extreal/extreal_inf' p) x)))).
tt('thm/extreal/le_inf_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: (('const/extreal/extreal_le' x ('const/extreal/extreal_inf' p)) = (![y : 'type/extreal/extreal']: ((p y) => ('const/extreal/extreal_le' x y)))))).
tt('thm/extreal/inf_le_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_inf' p) x) = (![y : 'type/extreal/extreal']: ((![z : 'type/extreal/extreal']: ((p z) => ('const/extreal/extreal_le' y z))) => ('const/extreal/extreal_le' y x)))))).
tt('thm/extreal/inf_eq_', ax, (![p : ('type/extreal/extreal' > $o), x : 'type/extreal/extreal']: ((('const/extreal/extreal_inf' p) = x) = ((![y : 'type/extreal/extreal']: ((p y) => ('const/extreal/extreal_le' x y))) & (![y : 'type/extreal/extreal']: ((![z : 'type/extreal/extreal']: ((p z) => ('const/extreal/extreal_le' y z))) => ('const/extreal/extreal_le' y x))))))).
tt('thm/extreal/inf_const_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_inf' (^[y : 'type/extreal/extreal']: (y = x))) = x))).
tt('thm/extreal/inf_const_alt_', ax, (![p : ('type/extreal/extreal' > $o), z : 'type/extreal/extreal']: (((?[x : 'type/extreal/extreal']: (p x)) & (![x : 'type/extreal/extreal']: ((p x) => (x = z)))) => (('const/extreal/extreal_inf' p) = z)))).
tt('thm/extreal/inf_const_over_set_', ax, ![A : $t]: (![s : (A > $o), k : 'type/extreal/extreal']: ((~ (s = ('const/pred_set/EMPTY' A))) => (('const/extreal/extreal_inf' (('const/pred_set/IMAGE' A 'type/extreal/extreal') (^[x : A]: k) s)) = k)))).
tt('thm/extreal/inf_suc_', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: ((![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/extreal/extreal_le' (f n) (f m)))) => (('const/extreal/extreal_inf' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (f ('const/num/SUC' n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/extreal_inf' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') f ('const/pred_set/UNIV' 'type/num/num'))))))).
tt('thm/extreal/inf_seq_', ax, (![f : ('type/num/num' > 'type/realax/real'), l : 'type/realax/real']: (('const/extreal/mono_decreasing' f) => (('const/seq/-->' f l) = (('const/extreal/extreal_inf' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: ('const/extreal/Normal' (f n))) ('const/pred_set/UNIV' 'type/num/num'))) = ('const/extreal/Normal' l)))))).
tt('thm/extreal/inf_lt_infty_', ax, (![p : ('type/extreal/extreal' > $o)]: (('const/extreal/extreal_lt' 'const/extreal/NegInf' ('const/extreal/extreal_inf' p)) => (![x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_lt' 'const/extreal/NegInf' x)))))).
tt('thm/extreal/inf_min_', ax, (![p : ('type/extreal/extreal' > $o), z : 'type/extreal/extreal']: (((p z) & (![x : 'type/extreal/extreal']: ((p x) => ('const/extreal/extreal_le' z x)))) => (('const/extreal/extreal_inf' p) = z)))).
tt('thm/extreal/inf_cminus_', ax, ![A : $t]: (![f : (A > 'type/extreal/extreal'), c : 'type/realax/real']: (('const/extreal/extreal_sub' ('const/extreal/Normal' c) ('const/extreal/extreal_inf' (('const/pred_set/IMAGE' A 'type/extreal/extreal') f ('const/pred_set/UNIV' A)))) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' A 'type/extreal/extreal') (^[n : A]: ('const/extreal/extreal_sub' ('const/extreal/Normal' c) (f n))) ('const/pred_set/UNIV' A)))))).
tt('thm/extreal/ext_suminf_def_', def, (![f : ('type/num/num' > 'type/extreal/extreal')]: (('const/extreal/ext_suminf' f) = ('const/extreal/extreal_sup' (('const/pred_set/IMAGE' 'type/num/num' 'type/extreal/extreal') (^[n : 'type/num/num']: (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' n))) ('const/pred_set/UNIV' 'type/num/num')))))).
tt('thm/extreal/ext_suminf_add_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), g : ('type/num/num' > 'type/extreal/extreal')]: ((![n : 'type/num/num']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f n)) & ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g n)))) => (('const/extreal/ext_suminf' (^[n : 'type/num/num']: ('const/extreal/extreal_add' (f n) (g n)))) = ('const/extreal/extreal_add' ('const/extreal/ext_suminf' f) ('const/extreal/ext_suminf' g)))))).
tt('thm/extreal/ext_suminf_cmul_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), c : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') c) & (![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f n)))) => (('const/extreal/ext_suminf' (^[n : 'type/num/num']: ('const/extreal/extreal_mul' c (f n)))) = ('const/extreal/extreal_mul' c ('const/extreal/ext_suminf' f)))))).
tt('thm/extreal/ext_suminf_cmul_alt_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), c : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') c) & ((![n : 'type/num/num']: (~ ((f n) = 'const/extreal/NegInf'))) | (![n : 'type/num/num']: (~ ((f n) = 'const/extreal/PosInf'))))) => (('const/extreal/ext_suminf' (^[n : 'type/num/num']: ('const/extreal/extreal_mul' ('const/extreal/Normal' c) (f n)))) = ('const/extreal/extreal_mul' ('const/extreal/Normal' c) ('const/extreal/ext_suminf' f)))))).
tt('thm/extreal/ext_suminf_lt_infty_', ax, (![f : ('type/num/num' > 'type/extreal/extreal')]: (((![n : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f n))) & (~ (('const/extreal/ext_suminf' f) = 'const/extreal/PosInf'))) => (![n : 'type/num/num']: ('const/extreal/extreal_lt' (f n) 'const/extreal/PosInf'))))).
tt('thm/extreal/ext_suminf_suminf_', ax, (![r : ('type/num/num' > 'type/realax/real')]: (((![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (r n))) & (~ (('const/extreal/ext_suminf' (^[n : 'type/num/num']: ('const/extreal/Normal' (r n)))) = 'const/extreal/PosInf'))) => (('const/extreal/ext_suminf' (^[n : 'type/num/num']: ('const/extreal/Normal' (r n)))) = ('const/extreal/Normal' ('const/seq/suminf' r)))))).
tt('thm/extreal/ext_suminf_mono_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), g : ('type/num/num' > 'type/extreal/extreal')]: ((![n : 'type/num/num']: ((~ ((g n) = 'const/extreal/NegInf')) & ('const/extreal/extreal_le' (g n) (f n)))) => ('const/extreal/extreal_le' ('const/extreal/ext_suminf' g) ('const/extreal/ext_suminf' f))))).
tt('thm/extreal/ext_suminf_sub_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), g : ('type/num/num' > 'type/extreal/extreal')]: (((![n : 'type/num/num']: (('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (g n)) & ('const/extreal/extreal_le' (g n) (f n)))) & (~ (('const/extreal/ext_suminf' f) = 'const/extreal/PosInf'))) => (('const/extreal/ext_suminf' (^[i : 'type/num/num']: ('const/extreal/extreal_sub' (f i) (g i)))) = ('const/extreal/extreal_sub' ('const/extreal/ext_suminf' f) ('const/extreal/ext_suminf' g)))))).
tt('thm/extreal/ext_suminf_sum_', ax, (![f : ('type/num/num' > 'type/extreal/extreal'), n : 'type/num/num']: (((![n0 : 'type/num/num']: ('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') (f n0))) & (![m : 'type/num/num']: (('const/arithmetic/<=' n m) => ((f m) = ('const/extreal/extreal_of_num' 'const/num/0'))))) => (('const/extreal/ext_suminf' f) = (('const/extreal/EXTREAL_SUM_IMAGE' 'type/num/num') f ('const/pred_set/count' n)))))).
tt('thm/extreal/extreal_min_def_', def, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_min' x y) = (('const/bool/COND' 'type/extreal/extreal') ('const/extreal/extreal_le' x y) x y)))).
tt('thm/extreal/extreal_max_def_', def, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_max' x y) = (('const/bool/COND' 'type/extreal/extreal') ('const/extreal/extreal_le' x y) y x)))).
tt('thm/extreal/min_le_', ax, (![z : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_min' x y) z) = (('const/extreal/extreal_le' x z) | ('const/extreal/extreal_le' y z))))).
tt('thm/extreal/min_le1_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ('const/extreal/extreal_le' ('const/extreal/extreal_min' x y) x))).
tt('thm/extreal/min_le2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ('const/extreal/extreal_le' ('const/extreal/extreal_min' x y) y))).
tt('thm/extreal/le_min_', ax, (![z : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' z ('const/extreal/extreal_min' x y)) = (('const/extreal/extreal_le' z x) & ('const/extreal/extreal_le' z y))))).
tt('thm/extreal/min_le2_imp_', ax, (![x1 : 'type/extreal/extreal', x2 : 'type/extreal/extreal', y1 : 'type/extreal/extreal', y2 : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x1 y1) & ('const/extreal/extreal_le' x2 y2)) => ('const/extreal/extreal_le' ('const/extreal/extreal_min' x1 x2) ('const/extreal/extreal_min' y1 y2))))).
tt('thm/extreal/min_refl_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_min' x x) = x))).
tt('thm/extreal/min_comm_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_min' x y) = ('const/extreal/extreal_min' y x)))).
tt('thm/extreal/min_infty_0', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_min' x 'const/extreal/PosInf') = x))).
tt('thm/extreal/min_infty_1', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_min' 'const/extreal/PosInf' x) = x))).
tt('thm/extreal/min_infty_2', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_min' 'const/extreal/NegInf' x) = 'const/extreal/NegInf'))).
tt('thm/extreal/min_infty_e3', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_min' x 'const/extreal/NegInf') = 'const/extreal/NegInf'))).
tt('thm/extreal/le_max_', ax, (![z : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' z ('const/extreal/extreal_max' x y)) = (('const/extreal/extreal_le' z x) | ('const/extreal/extreal_le' z y))))).
tt('thm/extreal/le_max1_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ('const/extreal/extreal_le' x ('const/extreal/extreal_max' x y)))).
tt('thm/extreal/le_max2_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ('const/extreal/extreal_le' y ('const/extreal/extreal_max' x y)))).
tt('thm/extreal/max_le_', ax, (![z : 'type/extreal/extreal', x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_le' ('const/extreal/extreal_max' x y) z) = (('const/extreal/extreal_le' x z) & ('const/extreal/extreal_le' y z))))).
tt('thm/extreal/max_le2_imp_', ax, (![x1 : 'type/extreal/extreal', x2 : 'type/extreal/extreal', y1 : 'type/extreal/extreal', y2 : 'type/extreal/extreal']: ((('const/extreal/extreal_le' x1 y1) & ('const/extreal/extreal_le' x2 y2)) => ('const/extreal/extreal_le' ('const/extreal/extreal_max' x1 x2) ('const/extreal/extreal_max' y1 y2))))).
tt('thm/extreal/max_refl_', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_max' x x) = x))).
tt('thm/extreal/max_comm_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_max' x y) = ('const/extreal/extreal_max' y x)))).
tt('thm/extreal/max_infty_0', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_max' x 'const/extreal/PosInf') = 'const/extreal/PosInf'))).
tt('thm/extreal/max_infty_1', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_max' 'const/extreal/PosInf' x) = 'const/extreal/PosInf'))).
tt('thm/extreal/max_infty_2', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_max' 'const/extreal/NegInf' x) = x))).
tt('thm/extreal/max_infty_e3', ax, (![x : 'type/extreal/extreal']: (('const/extreal/extreal_max' x 'const/extreal/NegInf') = x))).
tt('thm/extreal/Q_set_def_', def, ('const/extreal/Q_set' = (('const/pred_set/UNION' 'type/extreal/extreal') (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (?[a : 'type/num/num', b : 'type/num/num']: ((x = ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' a) ('const/extreal/extreal_of_num' b))) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' b))))))) (('const/pred_set/GSPEC' 'type/extreal/extreal' 'type/extreal/extreal') (^[x : 'type/extreal/extreal']: (('const/pair/,' 'type/extreal/extreal' $o) x (?[a : 'type/num/num', b : 'type/num/num']: ((x = ('const/extreal/extreal_ainv' ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' a) ('const/extreal/extreal_of_num' b)))) & ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' 'const/num/0') ('const/extreal/extreal_of_num' b)))))))))).
tt('thm/extreal/Q_not_infty_', ax, (![x : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') => (?[y : 'type/realax/real']: (x = ('const/extreal/Normal' y)))))).
tt('thm/extreal/Q_COUNTABLE_', ax, (('const/util_prob/countable' 'type/extreal/extreal') 'const/extreal/Q_set')).
tt('thm/extreal/NUM_IN_Q_0', ax, (![n : 'type/num/num']: (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_of_num' n) 'const/extreal/Q_set'))).
tt('thm/extreal/NUM_IN_Q_e1', ax, (![n : 'type/num/num']: (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_ainv' ('const/extreal/extreal_of_num' n)) 'const/extreal/Q_set'))).
tt('thm/extreal/Q_INFINITE_', ax, (~ (('const/pred_set/FINITE' 'type/extreal/extreal') 'const/extreal/Q_set'))).
tt('thm/extreal/OPP_IN_Q_', ax, (![x : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_ainv' x) 'const/extreal/Q_set')))).
tt('thm/extreal/INV_IN_Q_', ax, (![x : 'type/extreal/extreal']: (((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') & (~ (x = ('const/extreal/extreal_of_num' 'const/num/0')))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_div' ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) 'const/extreal/Q_set')))).
tt('thm/extreal/CMUL_IN_Q_', ax, (![z : 'type/num/num', x : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') => ((('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_mul' ('const/extreal/extreal_of_num' z) x) 'const/extreal/Q_set') & (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_mul' ('const/extreal/extreal_ainv' ('const/extreal/extreal_of_num' z)) x) 'const/extreal/Q_set'))))).
tt('thm/extreal/ADD_IN_Q_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') & (('const/bool/IN' 'type/extreal/extreal') y 'const/extreal/Q_set')) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_add' x y) 'const/extreal/Q_set')))).
tt('thm/extreal/SUB_IN_Q_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') & (('const/bool/IN' 'type/extreal/extreal') y 'const/extreal/Q_set')) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_sub' x y) 'const/extreal/Q_set')))).
tt('thm/extreal/MUL_IN_Q_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') & (('const/bool/IN' 'type/extreal/extreal') y 'const/extreal/Q_set')) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_mul' x y) 'const/extreal/Q_set')))).
tt('thm/extreal/DIV_IN_Q_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (((('const/bool/IN' 'type/extreal/extreal') x 'const/extreal/Q_set') & ((('const/bool/IN' 'type/extreal/extreal') y 'const/extreal/Q_set') & (~ (y = ('const/extreal/extreal_of_num' 'const/num/0'))))) => (('const/bool/IN' 'type/extreal/extreal') ('const/extreal/extreal_div' x y) 'const/extreal/Q_set')))).
tt('thm/extreal/rat_not_infty_', ax, (![r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r 'const/extreal/Q_set') => ((~ (r = 'const/extreal/NegInf')) & (~ (r = 'const/extreal/PosInf')))))).
tt('thm/extreal/ceiling_def_', def, (![x : 'type/realax/real']: (('const/extreal/ceiling' ('const/extreal/Normal' x)) = ('const/while/LEAST' (^[n : 'type/num/num']: ('const/real/real_lte' x ('const/real/real_of_num' n))))))).
tt('thm/extreal/CEILING_LBOUND_', ax, (![x : 'type/realax/real']: ('const/extreal/extreal_le' ('const/extreal/Normal' x) ('const/extreal/extreal_of_num' ('const/extreal/ceiling' ('const/extreal/Normal' x)))))).
tt('thm/extreal/CEILING_UBOUND_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/extreal/extreal_lt' ('const/extreal/extreal_of_num' ('const/extreal/ceiling' ('const/extreal/Normal' x))) ('const/extreal/extreal_add' ('const/extreal/Normal' x) ('const/extreal/extreal_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/extreal/Q_DENSE_IN_R_LEMMA_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: ((('const/extreal/extreal_le' ('const/extreal/extreal_of_num' 'const/num/0') x) & ('const/extreal/extreal_lt' x y)) => (?[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r 'const/extreal/Q_set') & (('const/extreal/extreal_lt' x r) & ('const/extreal/extreal_lt' r y))))))).
tt('thm/extreal/Q_DENSE_IN_R_', ax, (![x : 'type/extreal/extreal', y : 'type/extreal/extreal']: (('const/extreal/extreal_lt' x y) => (?[r : 'type/extreal/extreal']: ((('const/bool/IN' 'type/extreal/extreal') r 'const/extreal/Q_set') & (('const/extreal/extreal_lt' x r) & ('const/extreal/extreal_lt' r y))))))).
tt('thm/extreal/COUNTABLE_ENUM_Q_', ax, ![A : $t]: (![c : (A > $o)]: ((('const/util_prob/countable' A) c) = ((c = ('const/pred_set/EMPTY' A)) | (?[f : ('type/extreal/extreal' > A)]: (c = (('const/pred_set/IMAGE' 'type/extreal/extreal' A) f 'const/extreal/Q_set'))))))).
tt('thm/extreal/CROSS_COUNTABLE_UNIV_', ax, (('const/util_prob/countable' ('type/pair/prod' 'type/num/num' 'type/num/num')) (('const/pred_set/CROSS' 'type/num/num' 'type/num/num') ('const/pred_set/UNIV' 'type/num/num') ('const/pred_set/UNIV' 'type/num/num')))).
tt('thm/extreal/CROSS_COUNTABLE_LEMMA1_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o)]: (((('const/util_prob/countable' A) s) & ((('const/pred_set/FINITE' A) s) & (('const/util_prob/countable' B) t))) => (('const/util_prob/countable' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s t))))).
tt('thm/extreal/CROSS_COUNTABLE_LEMMA2_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o)]: (((('const/util_prob/countable' A) s) & ((('const/util_prob/countable' B) t) & (('const/pred_set/FINITE' B) t))) => (('const/util_prob/countable' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s t))))).
tt('thm/extreal/CROSS_COUNTABLE_', ax, ![B : $t, A : $t]: (![t : (B > $o), s : (A > $o)]: (((('const/util_prob/countable' A) s) & (('const/util_prob/countable' B) t)) => (('const/util_prob/countable' ('type/pair/prod' A B)) (('const/pred_set/CROSS' A B) s t))))).
tt('thm/extreal/open_interval_def_', def, (![a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (('const/extreal/open_interval' a b) = (('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' a x) & ('const/extreal/extreal_lt' x b)))))))).
tt('thm/extreal/open_intervals_set_def_', def, ('const/extreal/open_intervals_set' = (('const/pred_set/GSPEC' ('type/extreal/extreal' > $o) ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) (('const/pair/UNCURRY' 'type/extreal/extreal' 'type/extreal/extreal' ('type/pair/prod' ('type/extreal/extreal' > $o) $o)) (^[a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (('const/pair/,' ('type/extreal/extreal' > $o) $o) ('const/extreal/open_interval' a b) ((('const/bool/IN' 'type/extreal/extreal') a ('const/pred_set/UNIV' 'type/extreal/extreal')) & (('const/bool/IN' 'type/extreal/extreal') b ('const/pred_set/UNIV' 'type/extreal/extreal'))))))))).
tt('thm/extreal/rational_intervals_def_', def, ('const/extreal/rational_intervals' = (('const/pred_set/GSPEC' ('type/extreal/extreal' > $o) ('type/pair/prod' 'type/extreal/extreal' 'type/extreal/extreal')) (('const/pair/UNCURRY' 'type/extreal/extreal' 'type/extreal/extreal' ('type/pair/prod' ('type/extreal/extreal' > $o) $o)) (^[a : 'type/extreal/extreal', b : 'type/extreal/extreal']: (('const/pair/,' ('type/extreal/extreal' > $o) $o) ('const/extreal/open_interval' a b) ((('const/bool/IN' 'type/extreal/extreal') a 'const/extreal/Q_set') & (('const/bool/IN' 'type/extreal/extreal') b 'const/extreal/Q_set')))))))).
tt('thm/extreal/COUNTABLE_RATIONAL_INTERVALS_', ax, (('const/util_prob/countable' ('type/extreal/extreal' > $o)) 'const/extreal/rational_intervals')).
