SSL fubini_tonelli.prf
Interaktion und
(fubini_tonellinil 3453187626"" (skosimp)"" (lemma "fubini_tonelli_scaf1" ("h" "h!1" ))"" (replace 1 -1) (("" (propax) nil nil )) nil )) nil ))nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil fubini_tonelli nil )nil fubini_tonelli nil )nil measure_space nil )"bool" measure_space nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil fubini_tonelli_scaf nil ))nil 3459562328"" (skosimp)"" (lemma "fubini_tonelli_scaf2" ("h" "h!1" ))"" (replace 1 -1) (("" (propax) nil nil )) nil )) nil ))nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil fubini_tonelli nil )nil fubini_tonelli nil )nil measure_space nil )"bool" measure_space nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil fubini_tonelli_scaf nil ))nil 3431151472"" (skosimp)"" (typepred "g!1" )"" (lemma "fubini_tonelli_1" ("h" "g!1" ))"1" (assert )"1" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"1" (inst - "g!1" ) nil nil )) nil ))nil )"2" (expand "nn_measurable?" )"2" (split)"1" "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )nil nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil fubini_tonelli nil )nil fubini_tonelli nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil nn_integral nil )nil integral nil )nil fubini_tonelli nil )"bool" measure_space nil )nil measure_space nil ))nil ))nil 3459216640"" (skosimp)"" (typepred "g!1" )"" "nn_integrable_is_measurable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]" )"" (inst - "g!1" )"" (lemma "fubini_tonelli_scaf1" ("h" "g!1" ))"1" (flatten)"1" (split -3)"1" (propax) nil nil )"2" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"2" (inst - "g!1" ) nil nil )) nil ))nil ))nil )"2" (expand "nn_measurable?" )"2" (assert )"2" (skosimp)"2" (typepred "g!1(x!1)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil fubini_tonelli nil )nil fubini_tonelli nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil integral nil )nil fubini_tonelli_scaf nil )"bool" measure_space nil )nil measure_space nil )nil nn_integral nil ))nil 3431151472"" (skosimp)"" (typepred "g!1" )"" (lemma "fubini_tonelli_2" ("h" "g!1" ))"1" (assert )"1" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"1" (inst - "g!1" ) nil nil )) nil ))nil )"2" (expand "nn_measurable?" )"2" "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"2" (assert )"2" (skosimp) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil fubini_tonelli nil )nil fubini_tonelli nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil nn_integral nil )nil integral nil )nil fubini_tonelli nil )"bool" measure_space nil )nil measure_space nil ))nil ))nil 3459746299"" (skosimp)"" (typepred "g!1" )"" "nn_integrable_is_measurable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"" (inst - "g!1" )"" (lemma "fubini_tonelli_scaf2" ("h" "g!1" ))"1" (flatten)"1" (split -3)"1" (propax) nil nil )"2" "nn_integrable_is_integrable[[T1, T2], sigma_times(S1, S2), m_times(mu, nu)]" )"2" (inst - "g!1" ) nil nil )) nil ))nil ))nil )"2" (expand "nn_measurable?" )"2" (assert )"2" (skosimp) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"sigma_finite_measure[T2, S2]" fubini_tonellinil )"sigma_finite_measure[T1, S1]" fubini_tonellinil )"sigma_finite_measure[[T1, T2], sigma_times(S1, S2)]" nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra[T2]" fubini_tonelli nil )"sigma_algebra[T1]" fubini_tonelli nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil fubini_tonelli nil )nil fubini_tonelli nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil integral nil )nil fubini_tonelli_scaf nil )"bool" measure_space nil )nil measure_space nil )nil nn_integral nil ))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
