(outer_measure_def
(outer_measure_TCC1 0
(outer_measure_TCC1-1 nil 3396582266
("" (expand "zero_outer_measure" )
(("" (expand "outer_measure?" )
(("" (split)
(("1" (expand "om_empty?" ) (("1" (propax) nil nil )) nil )
("2" (expand "om_increasing?" )
(("2" (skosimp)
(("2" (expand "x_le" ) (("2" (assert ) nil nil )) nil )) nil ))
nil )
("3" (expand "om_countably_subadditive?" )
(("3" (skosimp)
(("3" (expand "o " )
(("3" (expand "x_sum" )
(("3" (expand "x_le" )
(("3" (rewrite "zero_series_conv" )
(("3" (rewrite "zero_series_limit" )
(("3" (assert ) nil nil )) nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil )
((outer_measure? const-decl "bool" outer_measure_def nil )
(om_countably_subadditive? const-decl "bool" outer_measure_def nil )
(O const-decl "T3" function_props nil )
(zero_series_limit formula-decl nil series "series/" )
(zero_series_conv formula-decl nil series "series/" )
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/" )
(om_increasing? const-decl "bool" outer_measure_def nil )
(x_le const-decl "bool" extended_nnreal "extended_nnreal/" )
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil )
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil )
(om_empty? const-decl "bool" outer_measure_def nil )
(zero_outer_measure const-decl "extended_nnreal" outer_measure_def
nil ))
nil )))
quality 84%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland