Impressum product_finite_measure.prf
Sprache: Lisp
(product_finite_measurenil 3450064167"" (skosimp)"" (expand "x_section" )"" "x_section_measurable[T1,T2]" "Z" "M!1" "x" "x1!1" "S1" "S1" "S2" "S2" ))"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"[T1 -> set[T2]]" cross_product "topology/" )"bool" sets nil )nil product_sigma_def nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )set type-eq-decl nil sets nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil product_finite_measure nil )nil product_finite_measure nil ))nil ))nil 3450064365"" (skosimp)"" (expand "o " )"" (split)"1" (assert ) nil nil )"2" (expand "x_section" )"2" "x_section_measurable[T1,T2]" "Z" "M!1" "x" "x!1" "S1" "S1" "S2" "S2" ))"2" (expand "member" )"2" "fm_monotone[T2,S2,nu!1]" "A" "x_section(M!1, x!1)" "B" "fullset[T2]" ))"2" (split)"1" (propax) nil nil )"2" (expand "subset?" )"2" (skosimp)"2" (expand "member" )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )"[T1 -> set[T2]]" cross_product "topology/" )"bool" sets nil )"bool" sets nil )"(S)" product_finite_measurenil )nil finite_measure nil )"set[T2]" cross_product "topology/" )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )nil product_sigma_def nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )set type-eq-decl nil sets nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil product_finite_measure nil )nil product_finite_measure nil )"(total_order?[real])" nil ))nil 3450064167"" (skosimp)"" (expand "y_section" )"" "y_section_measurable[T1,T2]" "Z" "M!1" "y" "x1!1" "S1" "S1" "S2" "S2" ))"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"[T2 -> set[T1]]" cross_product "topology/" )"bool" sets nil )nil product_sigma_def nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )set type-eq-decl nil sets nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil product_finite_measure nil )nil product_finite_measure nil ))nil ))nil 3450064193"" (skosimp)"" (expand "o" )"" (split)"1" (assert ) nil nil )"2" (expand "y_section" )"2" "y_section_measurable[T1,T2]" "Z" "M!1" "y" "y!1" "S1" "S1" "S2" "S2" ))"2" (expand "member" )"2" "m_monotone[T1,S1,to_measure(mu!1)]" "a" "y_section(M!1, y!1)" "b" "fullset[T1]" ))"1" (split)"1" (expand "to_measure" )"1" (expand "x_le" ) (("1" (propax) nil nil ))nil ))nil )"2" (expand "subset?" )"2" (expand "fullset" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil )"3" (expand "measurable_set?" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )"[T2 -> set[T1]]" cross_product "topology/" )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"bool" sets nil )"(S)" product_finite_measurenil )nil measure_props nil )"bool" measure_space_def nil )nil measure_space_def nil )"set[T1]" cross_product "topology/" )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil )nil product_sigma_def nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )set type-eq-decl nil sets nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil product_finite_measure nil )nil product_finite_measure nil )"(total_order?[real])" nil ))nil 3430980741"" (skosimp)"" (name "F" "lambda M: nu!1 o x_section(M)" )"1" (case-replace "nu!1 o x_section(M!1) = F(M!1)" )"1" (hide-all-but 1)"1" case "forall x,M: 0 <= F(M)(x) & F(M)(x) <= nu!1(fullset[T2])" )"1" "U" "{M:set[[T1,T2]] | sigma_times(S1,S2)(M) & measurable_function?[T1,S1](F(M))}" )"1" case "forall (R:measurable_rectangle(S1,S2)): U(R)" )"1" case "FORALL (a, b: (U)): disjoint?(a,b) => U(union(a, b))" )"1" (case "FORALL (a: (U)): U(complement(a))" )"1" (case "monotone?(U)" )"1" (lemma "monotone_class" ("C" "U" ))"1" (typepred "rectangle_algebra" )"1" (typepred "M!1" )"1" (inst -3 "rectangle_algebra" )"1" "1" expand "subset?" )"1" "M!1" )"1" expand "member" )"1" "1" expand "U" )"1" (propax) nil nil ))nil )"2" "2" expand "sigma_times" -1)"2" "generated_sigma_algebra_subset2" "X" "extend " "Y" "generated_sigma_algebra(rectangle_algebra)" ))"2" "SA" "generated_sigma_algebra(extend ") "2" "1" expand "subset?" )"1" "M!1" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "fullset" )"2" expand "extend" )"2" expand "member" )"2" "2" "2" "generated_sigma_algebra_subset1" "X" "rectangle_algebra" ))"2" expand "subset?" )"2" "x!1" )"2" assert )"2" "2" expand "rectangle_algebra" )"2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "lambda (i:nat): if i = 0 then x!1 else emptyset[[T1,T2]] endif" "1" )"2" "1" "1" nil nil ))nil )"2" "2" expand "IUnion" )"2" "x!1(x!2, x!3)" )"1" "0" )nil nil )"2" assert )"2" "2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "i!1=0" )"1" assert )nil nil )"2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" expand "rectangle_algebra" )"2" expand "finite_disjoint_unions" )"2" "2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "2" case "forall (n:nat): U(IUnion(n,E!1))" )"1" "IUnion(E!1)=IUnion(n!1,E!1)" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "EXISTS (i: nat): E!1(i)(x!2, x!3)" )"1" "1" "i!1" )"1" "1" "i!1<n!1" )"1" "E!1(i!1)" )"1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" expand "empty?" )"2" "(x!2,x!3)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "a!1" )"2" "n!2" )"2" "n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" rewrite "IUnion_0_def" )"1" "0" )"1" "1" "E!1(0)" )"1" assert )"1" rewrite "emptyset_is_empty?" )"1" replace "1" "1" expand "measurable_rectangle?" )"1" "emptyset" "emptyset" )"1" "1" "1" nil nil ))nil )"2" "S1" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "S2" )"3" expand "sigma_algebra?" )"3" "3" expand "subset_algebra_empty?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "IUnion_n_def" )"2" "E!1(1 + j!1)" )"1" "IUnion(j!1, E!1)" "E!1(1 + j!1)" )"1" "1" nil nil )"2" "2" expand "disjoint?" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "IUnion" )"2" expand "empty?" )"2" "2" expand "member" )"2" "2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "n!2" )"2" "n!2" "1+j!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace "2" "2" expand "measurable_rectangle?" )"2" "emptyset" "emptyset" )"2" "1" "1" nil nil ))nil )"2" "S1" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "S2" )"3" expand "sigma_algebra?" )"3" "3" expand "subset_algebra_empty?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (hide-all-but 1)"2" (expand "monotone?" )"2" (skosimp)"2" (expand "member" )"2" "1" "1" expand "U" 1)"1" "1" "sigma_algebra_IUnion[[T1,T2],sigma_times(S1, S2)]" "SS" "E!1" ))"1" (assert ) nil nil )"2" "2" "x1!1" )"2" expand "U" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil )"2" "pointwise_measurable[T1, S1]" "f" "F(IUnion(E!1))" "u" "lambda (n:nat): F(E!1(n))" ))"1" assert )"1" "1" expand "pointwise_convergence?" )"1" "1" expand "U" )"1" "fm_IUnion[T2,S2,nu!1]" "X" "lambda (n:nat): x_section(E!1(n),x!1)" ))"1" "1" expand "o " )"1" expand "F" )"1" expand "o " )"1" expand "x_section" "1" "LHS" "LAMBDA (n_1: nat): nu!1(x_section(E!1(n_1), x!1))" )"1" "IUnion(LAMBDA (n: nat): x_section(E!1(n), x!1))=x_section(IUnion(E!1), x!1)" )"1" "RHS" "nu!1(x_section(IUnion(E!1), x!1))" )"1" "1" rewrite "metric_convergence_def" )"1" expand "convergence" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "x_section" )"2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "2" "x!2" "y!1" )"2" assert )"2" expand "subset?" )"2" expand "x_section" )"2" expand "member" )"2" "2" "(x!1,x!3)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" "x_section_measurable" "S1" "S1" "S2" "S2" "Z" "E!1(n!1)" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "U" )"2" (flatten) nil nil ))nil ))nil ))nil )"3" "3" "n!1" )"3" expand "U" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "U" )"2" "1" "sigma_algebra_IIntersection[[T1,T2],sigma_times(S1, S2)]" "SS" "E!1" ))"1" (assert ) nil nil )"2" "2" "x1!1" )"2" (flatten) nil nil ))nil ))nil ))nil )"2" "pointwise_measurable[T1, S1]" "f" "F(IIntersection(E!1))" "u" "lambda (n:nat): F(E!1(n))" ))"1" assert )"1" "1" expand "pointwise_convergence?" )"1" "1" expand "F" )"1" expand "o " )"1" "fm_IIntersection[T2,S2,nu!1]" "X" "lambda (n:nat): x_section(E!1(n),x!1)" ))"1" "1" expand "o " )"1" expand "x_section" "1" "LHS" "LAMBDA (n_1: nat): nu!1(x_section(E!1(n_1), x!1))" )"1" "IIntersection(LAMBDA ") "1" "RHS" "nu!1(x_section(IIntersection(E!1), x!1))" )"1" "1" rewrite "metric_convergence_def" )"1" expand "convergence" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "IIntersection" )"2" expand "x_section" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" "2" "x!2" "y!1" )"2" assert )"2" expand "subset?" )"2" expand "x_section" )"2" "2" expand "member" )"2" "(x!1,x!3)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" "x_section_measurable" "S1" "S1" "S2" "S2" "Z" "E!1(n!1)" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" (flatten) nil nil ))nil ))nil )"3" "3" "n!1" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" (typepred "a!1" )"2" (expand "U" )"2" (flatten)"2" "sigma_algebra_complement[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" ))"2" assert )"2" "const_measurable[T1,S1]" "c" "nu!1(fullset[T2])" ))"2" "diff_measurable[T1,S1]" "g1" "LAMBDA (x: T1): nu!1(fullset[T2])" "g2" "F(a!1)" ))"1" expand "-" )"1" "(LAMBDA (x_1: T1): ") "1" "1" "1" expand "F" )"1" expand "o " )"1" "fm_disjointunion[T2,S2,nu!1]" "A" "x_section(a!1)(x!1)" "B" "x_section(complement(a!1))(x!1)" ))"1" expand "x_section" )"1" "1" "union(x_section(a!1, x!1), x_section(complement(a!1), x!1))=fullset[T2]" )"1" assert )nil nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (hide -3)"2" (typepred "b!1" )"2" (typepred "a!1" )"2" (expand "U" )"2" "2" "sigma_algebra_union[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" "y" "b!1" ))"2" assert )"2" "sum_measurable[T1, S1]" "g1" "F(a!1)" "g2" "F(b!1)" ))"2" expand "+" -1)"2" "(LAMBDA (x: T1): F(a!1)(x) + F(b!1)(x))=F(union(a!1, b!1))" )"2" "2" "2" expand "F" )"2" expand "o " )"2" expand "x_section" )"2" "fm_disjointunion[T2,S2,nu!1]" "A" "x_section(a!1, x!1)" "B" "x_section(b!1, x!1)" ))"2" rewrite "x_section_union" )"2" assert )"2" "2" "x_section_disjoint" "X" "a!1" "Y" "b!1" "a" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "U" )"2" (hide -1)"2" (typepred "R!1" )"2" (expand "measurable_rectangle?" )"2" (skosimp)"2" "1" assert )"1" expand "sigma_times" )"1" "generated_sigma_algebra_subset1" "X" "extend ")) "1" "SA" "generated_sigma_algebra(extend ") "1" expand "subset?" )"1" expand "fullset" )"1" expand "extend" )"1" expand "member" )"1" "R!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "F" )"2" expand "o " )"2" expand "x_section" )"2" "2" "phi_is_simple[T1,S1]" "X" "X!1" ))"1" expand "simple?" )"1" "1" "1" "scal_measurable[T1,S1]" "c" "nu!1(Y!1)" "g" "phi[T1,S1](X!1)" ))"1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "(LAMBDA (x: T1): IF X!1(x) THEN 1 ELSE 0 ENDIF)=(LAMBDA (x: T1): nu!1(x_section(R!1, x)))") "1" "1" replace "1" expand "cross_product" )"1" expand "x_section" )"1" "1" "X!1(x!1)" )"1" "{b: T2 | Y!1(b)}=Y!1" )"1" assert )nil nil )"2" nil nil ))nil )"2" assert )"2" "nu!1" )"2" expand "finite_measure?" )"2" "2" expand "emptyset" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "cross_product" )"2" expand "x_section" )"2" "X!1(x!1)" )"1" "{b: T2 | Y!1(b)}=Y!1" )"1" nil nil ))nil )"2" assert )"2" "S2" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "x_section" )"2" replace "2" expand "cross_product" )"2" "X!1(x!1)" )"1" "{b: T2 | Y!1(b)}=Y!1" )"1" nil nil ))nil )"2" assert )"2" "S2" )"2" expand "sigma_algebra?" )"2" expand "subset_algebra_empty?" )"2" "2" expand "member" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "F" )"2" (skosimp)"2" "x_section_bounded" "nu" "nu!1" "M" "M!2" "x" "x!1" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "F" ) (("2" (propax) nil nil )) nil ))nil )"2" (skosimp)"2" (skosimp)"2" (expand "x_section" )"2" "x_section_measurable" "S1" "S1" "S2" "S2" "Z" "M!2" "x" "x1!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[T1 -> set[T2]]" cross_product "topology/" )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )"T3" function_props nil )"[T, T -> boolean]" equalities 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 )"sigma_algebra[T2]" product_finite_measurenil )"sigma_algebra[T1]" product_finite_measurenil )"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 booleans nil )nil booleans nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )"bool" measure_space_def nil )nil measure_space nil )nil measure_space_def nil )"nat" measure_space nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" nil )"(S)" sigma_algebranil )"set[T2]" product_finite_measure nil )"measurable_rectangle[T1, T2](S1, S2)" nil )"[T -> real]" real_fun_ops "reals/" )"bool" measure_space nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"set" sets nil )nil measure_space_def nil )"nnreal" nil )nil finite_measure nil )"[T -> real]" real_fun_ops "reals/" )nil measure_space nil )nil sigma_algebra nil )"bool" subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"subset_algebra[[T1, T2]]" nil )"set[T]" nat_indexed_sets "sets_aux/" )"set" sets nil )"nat" product_finite_measure nil )"sequence[set[[T1, T2]]]" nil )"nat" product_finite_measure nil )"(total_order?[real])" nil )"bool" reals nil )"set[R]" function_image nil )nil defined_types nil )nil naturalnumbers nil )"bool" subset_algebra_def nil )"set[[T1, T2]]" cross_product"topology/" )"(S)" nil )"(S)" nil )nil nat_indexed_sets "sets_aux/" )nil nat_indexed_sets "sets_aux/" )"int" integers nil )"posint" nil )"nat" product_finite_measure nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"bool" sets nil )"bool" sets nil )nil nil )"bool" booleans nil )"R" extend nil )"sigma_algebra" nil )nil nil )"setofsets[T]" nil )"bool" subset_algebra_def nil )"real" reals nil )"boolean" notequal nil )"set" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"(total_order?[real])" nil )"set[T]" indexed_sets nil )"(strict_total_order?[real])" real_props nil )nil sets_lemmas nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"(S)" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )"(S)" nil )"(S)" sigma_algebranil )"[set[[T1, T2]] -> boolean]" nil )nil subset_algebra_def nil )nil subset_algebra_def nil )nil sigma_algebra nil )nil finite_measure nil )"bool" fun_preds_partial "structures/" )"set[T]" indexed_sets nil )nil sigma_algebra nil )"bool" pointwise_convergencenil )nil product_sigma_def nil )"[(sigma_times(S1, S2)) -> [T1 -> nnreal]]" nil )"bool" convergence_sequences "analysis/" )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"set[T]" metric_space_def "metric_space/" )"bool" reals nil )nil real_types nil )"bool" metric_space_def"metric_space/" )nil metric_space"metric_space/" )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" fun_preds_partial "structures/" )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"set[T2]" cross_product "topology/" )nil finite_measure nil )nil measure_space_defnil )nil measure_space nil )"set" sets nil )nil sigma_algebra nil )nil measure_space_def nil )nil product_sections nil )nil product_sections nil )"[T -> real]" real_fun_ops "reals/" )nil product_sigma_defnil )"bool" product_sigma_def nil )"set" sets nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(S)" product_finite_measurenil ))nil 3455615935"" (skosimp)"" (name "F" "lambda M: mu!1 o y_section(M)" )"1" (case-replace "mu!1 o y_section(M!1) = F(M!1)" )"1" (hide-all-but 1)"1" case "forall y,M: 0 <= F(M)(y) & F(M)(y) <= mu!1(fullset[T1])" )"1" "U" "{M:set[[T1,T2]] | sigma_times(S1,S2)(M) & measurable_function?[T2,S2](F(M))}" )"1" case "forall (R:measurable_rectangle(S1,S2)): U(R)" )"1" case "FORALL (a, b: (U)): disjoint?(a,b) => U(union(a, b))" )"1" (case "FORALL (a: (U)): U(complement(a))" )"1" (case "monotone?(U)" )"1" (lemma "monotone_class" ("C" "U" ))"1" (typepred "rectangle_algebra" )"1" (typepred "M!1" )"1" (inst -3 "rectangle_algebra" )"1" "1" expand "subset?" )"1" "M!1" )"1" expand "member" )"1" "1" expand "U" )"1" (propax) nil nil ))nil )"2" "2" expand "sigma_times" -1)"2" "generated_sigma_algebra_subset2" "X" "extend " "Y" "generated_sigma_algebra(rectangle_algebra)" ))"2" assert )"2" "1" "SA" "generated_sigma_algebra(extend ") "1" expand "subset?" )"1" "M!1" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "fullset" )"2" expand "extend" )"2" expand "member" )"2" "2" "generated_sigma_algebra_subset1" "X" "rectangle_algebra" ))"2" expand "subset?" )"2" expand "member" )"2" "x!1" )"2" assert )"2" "2" expand "rectangle_algebra" )"2" rewrite "finite_disjoint_rectangles" )"2" "singleton[(measurable_rectangle?(S1, S2))](x!1)" )"2" assert )"2" "1" "1" expand "singleton" )"1" expand "extend" )"1" expand "Union" )"1" "x!1(x!2,x!3)" )"1" "x!1" )nil nil )"2" assert )"2" "2" "a!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" "y!1" )"2" expand "singleton" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" "2" expand "rectangle_algebra" )"2" "2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "2" expand "member" )"2" case "forall (n:nat): U(IUnion(n,E!1))" )"1" "IUnion(E!1)=IUnion(n!1, E!1)" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "2" "2" "IUnion(E!1)(x!2, x!3)" )"1" expand "IUnion" )"1" "1" case "i!1>=n!1" )"1" "i!1" )"1" "1" assert )"1" expand "empty?" )"1" "(x!2,x!3)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" assert )"2" expand "image" )"2" expand "Union" )"2" "E!1(i!1)" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "2" "x!4" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" rewrite "IUnion_0_def" )"1" "0" )"1" "1" "n!1>0" )"1" assert )"1" "E!1(0)" )nil nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace "2" "emptyset" )"2" "2" expand "measurable_rectangle?" )"2" "emptyset" "emptyset" )"2" "1" "1" expand "cross_product" )"1" nil nil ))nil ))nil )"2" "S1" )"2" expand "sigma_algebra?" )"2" expand "subset_algebra_empty?" )"2" "2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "S2" )"3" expand "sigma_algebra?" )"3" expand "subset_algebra_empty?" )"3" "3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "IUnion_n_def" )"2" "IUnion(j!1, E!1)" "E!1(1 + j!1)" )"1" "1" nil nil )"2" "2" expand "disjoint?" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "n!2" )"2" "n!2" )"2" "n!2" "1+j!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1+j!1" )"2" "E!1(1+j!1)" )"2" "2" "1 + j!1 < n!1" )"1" nil nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" replace "2" "2" expand "measurable_rectangle?" )"2" "emptyset" "emptyset" )"2" "1" "1" nil nil ))nil )"2" "S1" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "S2" )"3" expand "sigma_algebra?" )"3" "3" expand "subset_algebra_empty?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (hide 2)"2" (expand "monotone?" )"2" (skosimp)"2" (expand "member" )"2" "1" "1" "sigma_algebra_IUnion[[T1,T2],sigma_times(S1,S2)]" "SS" "E!1" ))"1" expand "member" )"1" expand "U" 1)"1" assert )"1" "pointwise_measurable[T2, S2]" "f" "F(IUnion(E!1))" "u" "lambda (n:nat): F(E!1(n))" ))"1" assert )"1" "1" expand "pointwise_convergence?" )"1" "y!1" )"1" expand "F" )"1" expand "o " )"1" expand "y_section" )"1" "1" "mu!1" )"1" expand "finite_measure?" )"1" "1" "disjoint_IUnion" "A" "E!1" ))"1" "1" case "forall (n:nat): sigma_times(S1, S2)(B!1(n))" )"1" "lambda (n:nat): y_section(B!1(n), y!1)" )"1" "(IUnion(LAMBDA (n: nat): y_section(B!1(n), y!1)))=y_section(IUnion(E!1), y!1)" )"1" "1" "RHS" "mu!1(y_section(IUnion(E!1), y!1))" )"1" expand "o " )"1" case "forall (n:nat): IUnion(n, E!1)=E!1(n)" )"1" case "forall (n:nat): series(LAMBDA (x: nat): mu!1(y_section(B!1(x), y!1)))(n)= mu!1(y_section(E!1(n), y!1))" )"1" "extensionality_postulate" "f" "series(LAMBDA (x: nat): mu!1(y_section(B!1(x), y!1)))" "g" "lambda (n:nat): mu!1(y_section(E!1(n), y!1))" ))"1" "1" "1" "1" "1" replace "1" "LHS" "LAMBDA (n: nat): mu!1(y_section(E!1(n), y!1))" )"1" "1" rewrite "metric_convergence_def" )"1" expand "convergence" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" expand "member" )"1" expand "ball" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" expand "sigma" "2" replace "2" "2" "j!1" )"2" replace "2" "j!1" )"2" replace "2" "fm_disjointunion[T1,S1,mu!1]" "A" "y_section(difference(E!1(j!1 + 1), E!1(j!1)), y!1)" "B" "y_section(E!1(j!1), y!1)" ))"2" "1" "union(y_section(difference(E!1(j!1 + 1), E!1(j!1)), y!1), ") "1" assert )nil nil )"2" "2" "2" expand "difference" )"2" expand "y_section" )"2" expand "union" )"2" expand "member" )"2" "E!1(1 + j!1)(x!1, y!1)" )"1" nil nil )"2" assert )"2" expand "increasing?" )"2" "j!1" "1+j!1" )"2" assert )"2" expand "subset?" )"2" "(x!1,y!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "difference" )"2" expand "y_section" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "increasing?" )"2" expand "subset?" )"2" expand "empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!2" )"3" expand "U" )"3" "3" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "E!1(n!2)" "y" "y!1" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "x!1" )"4" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "B!1(x!1)" "y" "y!1" ))"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1" )"3" expand "U" "3" "3" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "E!1(n!1)" "y" "y!1" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "x!1" )"4" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "B!1(x!1)" "y" "y!1" ))"4" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "E!1(n!1)(x!1, x!2)" )"1" "E!1(n!1)" )"1" "n!1" )nil nil ))nil )"2" assert )"2" "2" "a!1" )"2" "n!2" )"2" expand "increasing?" )"2" "n!2" "n!1" )"2" assert )"2" expand "subset?" )"2" "(x!1,x!2)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "IUnion" )"2" expand "y_section" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" "2" expand "disjoint?" )"2" "2" "i!1" "j!1" )"2" assert )"2" "y_section_disjoint" "X" "B!1(i!1)" "Y" "B!1(j!1)" "b" "y!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1" )"3" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "B!1(n!1)" "y" "y!1" ))"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" replace "1" assert )"1" "0" )"1" expand "U" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" replace "2" "IUnion(j!1, E!1)=E!1(j!1)" )"1" "j!1" )"1" "j!1+1" )"1" expand "U" )"1" "1" "sigma_algebra_difference[[T1,T2],sigma_times(S1, S2)]" "x" "E!1(j!1 + 1)" "y" "E!1(j!1)" ))"1" expand "member" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "E!1(j!1)(x!1, x!2)" )"1" expand "IUnion" )"1" expand "image" )"1" expand "Union" )"1" "E!1(j!1)" )"1" "j!1" )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "n!1" )"2" replace "2" "2" expand "increasing?" )"2" "n!1" )"2" "n!1" "j!1" )"2" assert )"2" expand "subset?" )"2" "(x!1,x!2)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "U" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x1!1" )"2" expand "U" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "U" 1)"2" "1" "sigma_algebra_IIntersection[[T1,T2],sigma_times(S1,S2)]" "SS" "E!1" ))"1" (assert ) nil nil )"2" "2" "x1!1" )"2" expand "U" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil )"2" "pointwise_measurable[T2, S2]" "f" "F(IIntersection(E!1))" "u" "lambda (n:nat): F(E!1(n))" ))"1" assert )"1" "1" expand "pointwise_convergence?" )"1" "y!1" )"1" expand "F" )"1" expand "o " )"1" "fm_IIntersection[T1,S1,mu!1]" "X" "lambda (n:nat): y_section(E!1(n),y!1)" ))"1" expand "y_section" "1" expand "o " )"1" "LHS" "LAMBDA (x: nat): mu!1(y_section(E!1(x), y!1))" )"1" "1" "IIntersection(LAMBDA ") "1" "1" "RHS" "mu!1(y_section(IIntersection(E!1), y!1))" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" expand "convergence" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "IIntersection" )"2" expand "y_section" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "decreasing?" )"2" "2" "x!1" "y!2" )"2" assert )"2" expand "subset?" )"2" expand "y_section" )"2" expand "member" )"2" "2" "(x!2,y!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "U" )"2" "2" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "E!1(n!1)" "y" "y!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" expand "U" )"2" (flatten) nil nil ))nil ))nil ))nil )"3" "3" "n!1" )"3" expand "U" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (typepred "a!1" )"2" (expand "U" )"2" (flatten)"2" "1" "sigma_algebra_complement[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" ))"1" (assert ) nil nil ))nil )"2" expand "F" )"2" expand "y_section" )"2" "2" expand "o " )"2" "const_measurable[T2,S2]" "c" "mu!1(fullset[T1])" ))"2" "diff_measurable[T2, S2]" "g1" "(LAMBDA (x: T2): mu!1(fullset[T1]))" "g2" "(LAMBDA (x: T2): mu!1(y_section(a!1, x)))" ))"1" expand "-" )"1" "(LAMBDA (x_1: T2): LAMBDA (x: T2): mu!1(y_section(complement(a!1), x)))") "1" "1" "1" "1" "fm_disjointunion[T1,S1,mu!1]" "A" "y_section(a!1, x!1)" "B" "y_section(complement(a!1), x!1)" ))"1" "1" "union(y_section(a!1, x!1), y_section(complement(a!1), x!1))=fullset[T1]" )"1" assert )nil nil )"2" "2" "2" expand "fullset" )"2" expand "union" )"2" expand "complement" )"2" expand "y_section" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "complement" )"2" expand "intersection" )"2" expand "empty?" )"2" "2" expand "member" )"2" "2" expand "y_section" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "sigma_algebra_complement[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" ))"2" expand "member" )"2" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "complement(a!1)" "y" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "a!1" "y" "x!1" ))"3" assert )nil nil ))nil ))nil ))nil )"2" "2" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "complement(a!1)" "y" "x!1" ))"2" assert )"2" "sigma_algebra_complement[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" "3" "y_section_measurable" "S1" "S1" "S2" "S2" "Z" "a!1" "y" "x!1" ))"3" assert )nil nil ))nil ))nil )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (typepred "a!1" )"2" (typepred "b!1" )"2" (expand "U" )"2" (flatten)"2" "2" "1" "sigma_algebra_union[[T1,T2],sigma_times(S1, S2)]" "x" "a!1" "y" "b!1" ))"1" expand "member" )"1" (propax) nil nil ))nil ))nil )"2" "sum_measurable[T2, S2]" "g1" "F(a!1)" "g2" "F(b!1)" ))"1" "F(union(a!1, b!1))=(reals@real_fun_ops[T2].+)(F(a!1), F(b!1))" )"1" "1" "1" expand "+" )"1" expand "F" )"1" expand "o " )"1" expand "y_section" )"1" rewrite "y_section_union" )"1" "1" "y_section_disjoint" "X" "a!1" "Y" "b!1" "b" "x!1" ))"1" assert )"1" "fm_disjointunion[T1,S1,mu!1]" "A" "y_section(a!1, x!1)" "B" "y_section(b!1, x!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "+" )"2" "x1!1" "a!1" )"2" "x1!1" "b!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (typepred "R!1" )"2" (expand "U" )"2" (hide -2)"2" (assert )"2" (split)"1" expand "sigma_times" )"1" "generated_sigma_algebra_subset1" "X" "(extend ")) "1" "AA" "generated_sigma_algebra(extend ") "1" expand "fullset" )"1" expand "extend" )"1" expand "subset?" )"1" expand "member" )"1" "R!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "F" )"2" expand "measurable_rectangle?" )"2" "2" expand "o " )"2" "phi_is_simple[T2,S2]" "X" "Y!1" ))"1" expand "simple?" )"1" "1" "1" "scal_measurable[T2,S2]" "c" "mu!1(X!1)" "g" "phi[T2,S2](Y!1)" ))"1" expand "*" -1)"1" expand "y_section" )"1" expand "phi" )"1" expand "member" )"1" "(LAMBDA (x: T2): IF Y!1(x) THEN 1 ELSE 0 ENDIF)=(LAMBDA (x: T2): mu!1(y_section(R!1, x)))") "1" "1" replace "1" expand "cross_product" )"1" expand "y_section" )"1" "Y!1(x!1)" )"1" "{a: T1 | X!1(a)}=X!1" )"1" assert )nil nil )"2" nil nil ))nil )"2" assert )"2" "mu!1" )"2" expand "finite_measure?" )"2" "2" expand "emptyset" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "y_section" )"2" replace "2" expand "cross_product" )"2" "Y!1(x!1)" )"1" "{a: T1 | X!1(a)}=X!1" )"1" nil nil ))nil )"2" assert )"2" "S1" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "y_section" )"2" replace "2" expand "cross_product" )"2" "Y!1(x!1)" )"1" "{a: T1 | X!1(a)}=X!1" )"1" nil nil ))nil )"2" assert )"2" "S1" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"2" expand "member" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "F" )"2" "y_section_bounded" "M" "M!2" "mu" "mu!1" "y" "y!1" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "F" ) (("2" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "y_section" )"2" "y_section_measurable[T1,T2]" "Z" "M!2" "S1" "S1" "S2" "S2" "y" "x1!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"[T2 -> set[T1]]" cross_product "topology/" )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )"T3" function_props nil )"[T, T -> boolean]" equalities 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 )"sigma_algebra[T2]" product_finite_measurenil )"sigma_algebra[T1]" product_finite_measurenil )"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 booleans nil )nil booleans nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )"bool" measure_space_def nil )nil measure_space nil )nil measure_space_def nil )"nat" measure_space nil )"measurable_rectangle[T1, T2](S1, S2)" nil )"set[T1]" product_finite_measure nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"bool" measure_space nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"set" sets nil )nil measure_space nil )"[T -> real]" real_fun_ops "reals/" )"(U)" product_finite_measure nil )nil measure_space_def nil )nil sigma_algebra nil )"bool" subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"subset_algebra[[T1, T2]]" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil )"set[T]" nat_indexed_sets "sets_aux/" )"(total_order?[real])" nil )"nat" product_finite_measure nil )"sequence[set[[T1, T2]]]" nil )"nat" product_finite_measure nil )"set[R]" function_image nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )"set[T]" indexed_sets nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil sets_lemmas nil )"(S)" nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"set" sets nil )"real" reals nil )"(S)" nil )"(S)" nil )"set[[T1, T2]]" cross_product"topology/" )"bool" subset_algebra_def nil )nil nat_indexed_sets "sets_aux/" )nil nat_indexed_sets "sets_aux/" )"int" integers nil )"posint" nil )"bool" reals nil )"bool" indexed_sets_aux "sets_aux/" )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" product_finite_measure nil )"posint" nil )"bool" subset_algebra_def nil )"setofsets[T]" nil )"bool" sets nil )"bool" sets nil )nil nil )"bool" booleans nil )"R" extend nil )"sigma_algebra" nil )nil nil )"(singleton?)" sets nil )"bool" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )"(nonempty?[T])" nil )"finite_set[T]" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas_aux nil )"non_empty_finite_set[set[T]]" countable_setofsets "sets_aux/" )"non_empty_finite_set[T]" sigma_countable "sigma_set/" )nil product_sigma nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"(S)" nil )"(S)" sigma_algebranil )"[set[[T1, T2]] -> boolean]" nil )nil subset_algebra_def nil )nil subset_algebra_def nil )nil sigma_algebra nil )nil finite_measure nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )"bool" fun_preds_partial "structures/" )"set[T]" indexed_sets nil )"bool" pointwise_convergencenil )"[(sigma_times(S1, S2)) -> [T2 -> nnreal]]" nil )"nat" product_finite_measure nil )nil sigma_algebra nil )"set[T1]" cross_product "topology/" )"sequence[set[[T1, T2]]]" nil )"T2" product_finite_measure nil )"bool" nil )nil nil )"nat" product_finite_measure nil )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )"set[T]" metric_space_def "metric_space/" )nil real_types nil )"bool" metric_space_def"metric_space/" )nil metric_space"metric_space/" )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil functions nil )"sequence[set[[T1, T2]]]" nil )"real" sigma "reals/" )"nnreal" sigma_nat "reals/" )nil finite_measure nil )"set" sets nil )"nnreal" nil )"bool" fun_preds_partial "structures/" )"odd_int" integersnil )nil product_sigma_def nil )nil product_sections nil )nil nat_indexed_sets "sets_aux/" )"(S)" sigma_algebranil )nil measure_space_defnil )nil measure_space nil )nil sigma_algebra nil )"set" sets nil )nil sigma_algebra nil )"[T -> real]" real_fun_ops "reals/" )"(U)" product_finite_measure nil )"(U)" product_finite_measure nil )nil product_sections nil )nil measure_space_def nil )nil product_sigma_defnil )"bool" product_sigma_def nil )"set" sets nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(S)" product_finite_measurenil ))nil 3449893818"" (skosimp)"" (lemma "x_section_measurable" ("nu" "nu!1" "M" "M!1" ))"" "nn_integrable_le[T1, S1, to_measure(mu!1)]" "g" "nu!1 o x_section(M!1)" ))"1" (inst - "lambda (x:T1): nu!1(fullset[T2])" )"1" (split -1)"1" (flatten)"1" (hide -2 -3)"1" "nn_integrable_is_integrable[T1, S1, to_measure(mu!1)]" )"1" (inst - "nu!1 o x_section(M!1)" ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "o" )"2" (assert )"2" (split)"1" (assert ) nil nil )"2" "m_monotone[T2, S2, to_measure(nu!1)]" "a" "x_section(M!1)(x!1)" "b" "fullset[T2]" ))"1" (split -1)"1" (expand "to_measure" )"1" (expand "x_le" )"1" (propax) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (expand "subset?" )"2" expand "fullset" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -1)"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil )"3" (hide 2)"3" "x_section_measurable[T1,T2]" "Z" "M!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" (expand "member" )"3" expand "measurable_set?" )"3" expand "x_section" 1)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" "nn_isf_is_nn_integrable[T1, S1, to_measure(mu!1)]" )"2" (inst - "LAMBDA (x: T1): nu!1(fullset[T2])" )"1" (flatten) nil nil )"2" (hide 2)"2" (expand "nn_isf?" )"2" (split)"1" (expand "isf?" )"1" (split)"1" "simple_const[T1,S1]" "c" "nu!1(fullset[T2])" ))"1" (propax) nil nil )) nil )"2" (expand "mu_fin?" )"2" (expand "to_measure" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "nu!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )nil generalized_measure_defnil )"bool" generalized_measure_def 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 )"sigma_algebra[T2]" product_finite_measurenil )"sigma_algebra[T1]" product_finite_measurenil )"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 booleans nil )nil booleans nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )"(S)" product_finite_measurenil )"finite_measure[T1, S1]" nil )"bool" nn_integral nil )"finite_measure[T2, S2]" nil )"set" sets nil )nil nn_integral nil )nil product_sigma_def nil )"bool" extended_nnreal "extended_nnreal/" )"bool" sets nil )"bool" sets nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_props nil )"(total_order?[real])" nil )nil integral nil )"(sigma_times(S1, S2))" nil )nil nn_integral nil )nil measure_space nil )"bool" measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"bool" isf nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nn_integral nil )"bool" measure_space_def nil )nil measure_space_defnil )"T3" function_props nil )set type-eq-decl nil sets nil )"[T1 -> set[T2]]" cross_product "topology/" )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil ))nil 3449899886"" (skosimp)"" "nn_integrable_le[T2, S2, to_measure(nu!1)]" "g" "mu!1 o y_section(M!1)" "f" "lambda (x:T2): mu!1(fullset[T1])" ))"1" (split -1)"1" (flatten)"1" "nn_integrable_is_integrable[T2, S2, to_measure(nu!1)]" )"1" (inst - "mu!1 o y_section(M!1)" ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "o" )"2" (split)"1" (assert ) nil nil )"2" (expand "y_section" )"2" "m_monotone[T1,S1,to_measure(mu!1)]" "a" "y_section(M!1, x!1)" "b" "fullset[T1]" ))"1" (split -1)"1" (expand "to_measure" )"1" (expand "x_le" ) (("1" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (expand "subset?" )"2" (expand "fullset" )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil )"3" (hide 2)"3" (expand "measurable_set?" )"3" "y_section_measurable[T1,T2]" "Z" "M!1" "S1" "S1" "S2" "S2" "y" "x!1" ))"3" (expand "member" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (rewrite "y_section_measurable" ) nil nil ))nil )"3" (hide 2)"3" "nn_isf_is_nn_integrable[T2, S2, to_measure(nu!1)]" )"3" (inst - "LAMBDA (x: T2): mu!1(fullset[T1])" )"1" (flatten) nil nil )"2" (hide 2)"2" (expand "nn_isf?" )"2" (split)"1" (expand "isf?" )"1" (expand "mu_fin?" )"1" (expand "to_measure" )"1" "simple_const[T2,S2]" "c" "mu!1(fullset[T1])" ))"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"measure_type" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil generalized_measure_defnil )"bool" generalized_measure_def 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 )"sigma_algebra[T2]" product_finite_measurenil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil product_finite_measure nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"[T2 -> set[T1]]" cross_product "topology/" )"T3" function_props nil )nil measure_space_defnil )"bool" measure_space_def nil )"set" sets nil ) (set type-eq-decl nil sets nil )"sigma_algebra[T1]" product_finite_measurenil )nil product_finite_measure nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"(S)" product_finite_measurenil )nil product_sigma_def nil )"bool" extended_nnreal "extended_nnreal/" )"bool" sets nil )"bool" sets nil )"set[T1]" cross_product "topology/" )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_props nil )"(total_order?[real])" nil )nil integral nil )nil product_finite_measure nil )nil nn_integral nil )"bool" measure_props nil )nil measure_space nil )"(total_order?[real])" nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"finite_measure[T1, S1]" nil )"bool" isf nil )"finite_measure[T2, S2]" nil )AND const-decl "[bool, bool -> bool]" booleans nil ))nil 3450064940"" (skosimp) (("" (rewrite "x_section_integrable" ) nil nil )) nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil ))nil ))nil 3450065087"" (skosimp)"" (expand "o " )"" (expand "x_section" )"" "(LAMBDA (x: T1): nu!1(x_section(M!1, x))) = lambda x: phi[T1,S1](X!1)(x)* nu!1(Y!1)" )"1" (hide -1)"1" "integral_scal[T1, S1, to_measure(mu!1)]" "c" "nu!1(Y!1)" "f" "phi[T1, S1](X!1)" ))"1" "integral_phi[T1, S1, to_measure(mu!1)]" "F" "X!1" ))"1" (expand "mu" -1)"1" (expand "to_measure" )"1" (replace -1)"1" (expand "*" )"1" (expand "phi" )"1" (expand "member" )"1" (hide -1)"1" expand "integral" )"1" "(LAMBDA (x: T1): IF X!1(x) THEN 1 ELSE 0 ENDIF)=(LAMBDA x: IF X!1(x) THEN 1 ELSE 0 ENDIF * nu!1(Y!1))") "1" replace -2 1)"1" (assert ) nil nil ))nil )"2" "2" "X!1(x!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "mu_fin?" )"2" (expand "to_measure" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" "isf_phi[T1, S1, to_measure(mu!1)]" "E" "X!1" ))"1" "isf_is_integrable[T1, S1, to_measure(mu!1)]" )"1" (inst - "phi[T1, S1](X!1)" ) nil nil )) nil )"2" (expand "mu_fin?" )"2" (expand "to_measure" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (expand "x_section" )"1" (replace -1)"1" (expand "cross_product" )"1" (hide -1)"1" (expand "phi" )"1" (expand "member" )"1" (case-replace "X!1(x!1)" )"1" (case-replace "{y: T2 | Y!1(y)}=Y!1" )"1" (assert ) nil nil )"2" nil nil ))nil )"2" (assert )"2" "nu!1" )"2" expand "finite_measure?" )"2" expand "emptyset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "x_section_measurable[T1,T2]" "x" "x!1" "Z" "M!1" "S1" "S1" "S2" "S2" ))"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" "x_section_measurable[T1,T2]" "x" "x!1" "Z" "M!1" "S1" "S1" "S2" "S2" ))"3" (expand "member" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )"nnreal" nil )nil product_finite_measure nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil product_finite_measure nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T2]" product_finite_measurenil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )set type-eq-decl nil sets nil )"set[T2]" cross_product "topology/" )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"sigma_algebra[T1]" product_finite_measurenil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )nil integral nil )"bool" integral nil )nil integral nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil )"nnreal" measure_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" integral nil )"bool" sets nil )"[T -> real]" real_fun_ops "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" measure_props nil )nil measure_space_def nil )"bool" measure_space_def nil )nil integral nil )nil isf nil )nil isf nil )"bool" isf nil )"finite_measure[T1, S1]" nil )"(S1)" product_finite_measure nil )nil integral nil )"(sigma_times(S1, S2))" nil )"(S)" sigma_algebranil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"set[[T1, T2]]" cross_product"topology/" )nil product_sigma_def nil )"[T1 -> set[T2]]" cross_product "topology/" ))nil 3450064940"" (skosimp) (("" (rewrite "y_section_integrable" ) nil nil )) nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil ))nil ))nil 3450066860"" (skosimp)"" (expand "o " )"" (expand "y_section" )"" "(LAMBDA y: mu!1(y_section(M!1, y))) = lambda y: phi[T2,S2](Y!1)(y)* mu!1(X!1)" )"1" (hide -1)"1" (hide -1)"1" "isf_phi[T2, S2, to_measure(nu!1)]" ("E" "Y!1" ))"1" "isf_is_integrable[T2, S2, to_measure(nu!1)]" )"1" (inst - "phi[T2,S2](Y!1)" )"1" (hide -2)"1" "integral_phi[T2, S2, to_measure(nu!1)]" "F" "Y!1" ))"1" "integral_scal[T2, S2, to_measure(nu!1)]" "c" "mu!1(X!1)" "f" "phi[T2, S2](Y!1)" ))"1" (expand "*" )"1" "(LAMBDA (x: T2): mu!1(X!1) * phi[T2, S2](Y!1)(x))=(LAMBDA y: phi[T2, S2](Y!1)(y) * mu!1(X!1))" )"1" replace -2)"1" replace -3)"1" expand "mu" )"1" expand "to_measure" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (expand "mu_fin?" )"2" (expand "to_measure" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality :hide? t)"1" (replace -1)"1" (hide-all-but 1)"1" (expand "cross_product" )"1" (expand "y_section" )"1" (expand "phi" )"1" (expand "member" )"1" (case-replace "Y!1(x!1)" )"1" "{x_1: T1 | X!1(x_1)}=X!1" )"1" (assert ) nil nil )"2" (apply-extensionality :hide? t) nil nil ))nil )"2" (assert )"2" (typepred "mu!1" )"2" expand "finite_measure?" )"2" expand "emptyset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "y_section_measurable[T1,T2]" "Z" "M!1" "y" "y!1" "S1" "S1" "S2" "S2" ))"2" (expand "member" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp)"3" "y_section_measurable[T1,T2]" "Z" "M!1" "y" "y!1" "S1" "S1" "S2" "S2" ))"3" (expand "member" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )"nnreal" nil )nil product_finite_measure nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil product_finite_measure nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )set type-eq-decl nil sets nil )"set[T1]" cross_product "topology/" )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"sigma_algebra[T2]" product_finite_measurenil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space nil )nil integral nil )nil integral nil )"bool" integral nil )nil integral nil )"nnreal" measure_props nil )"[T -> real]" real_fun_ops "reals/" )nil integral nil )nil isf nil )"(S2)" product_finite_measure nil )"bool" isf nil )"finite_measure[T2, S2]" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"measure_type" generalized_measure_def nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_props nil )nil measure_space_def nil )"bool" measure_space_def nil )nil isf nil )nil product_sigma_def nil )"set[[T1, T2]]" cross_product"topology/" )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"(S)" sigma_algebranil )"bool" sets nil )"(sigma_times(S1, S2))" nil )"[T2 -> set[T1]]" cross_product "topology/" ))nil 3431017313"" (skosimp) (("" (rewrite "x_section_integrable" ) nil nil )) nil )nil product_finite_measure nil )nil product_finite_measure nil )nil product_finite_measure nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[[T1, T2]]" product_sigma_defnil )"sigma_algebra[T1]" product_finite_measurenil )"sigma_algebra[T2]" product_finite_measurenil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil ))nil ))nil 3431017313"" (skosimp)"" (expand "o" )"" "integral_nonneg[T1, S1, to_measure[T1, S1](mu!1)]" "f" "LAMBDA (x: T1): nu!1(x_section[T1, T2](M!1)(x))" ))"1" (split -1)"1" (propax) nil nil )"2" (hide -1 2)"2" (skosimp) (("2" (assert ) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" "fm_times_TCC1" ("mu" "mu!1" "nu" "nu!1" "M" "M!1" ))"2" (expand "o" ) (("2" (propax) nil nil )) nil )) nil ))nil )"3" (hide 2)"3" (skosimp)"3" (expand "x_section" )"3" "x_section_measurable[T1,T2]" "Z" "M!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" (expand "member" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T3" function_props nil )"bool" sets nil )nil product_sigma_def nil )nil product_finite_measure nil )"(total_order?[real])" nil )nil integral nil )"bool" integral nil )nil integral nil )nil product_finite_measure nil )"sigma_algebra[T2]" product_finite_measurenil )set type-eq-decl nil sets nil )"[T1 -> set[T2]]" cross_product "topology/" )"sigma_algebra[[T1, T2]]" product_sigma_defnil )nil product_finite_measure nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra[T1]" product_finite_measurenil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" generalized_measure_def nil )nil generalized_measure_defnil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil ))nil ))nil 3431017313"" (skosimp)"" (lemma "fm_times_TCC1" ("mu" "mu!1" "nu" "nu!1" ))"" (lemma "fm_times_TCC2" ("mu" "mu!1" "nu" "nu!1" ))"" (rewrite "finite_measure_def" )"1" (split 1)"1" (inst -2 "emptyset[[T1,T2]]" )"1" (assert )"1" (inst -1 "emptyset[[T1,T2]]" )"1" "x_section[T1, T2](emptyset[[T1, T2]])=lambda (x:T1): emptyset[T2]" )"1" (hide -1)"1" (expand "o" )"1" (rewrite "fm_emptyset[T2,S2,nu!1]" )"1" rewrite "integral_zero[T1, S1, to_measure[T1, S1](mu!1)]" nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (expand "x_section" )"2" expand "x_section" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (expand "o" )"2" (typepred "nu!1" )"2" (rewrite "finite_measure_def" -1)"2" (flatten)"2" (hide -3)"2" "(LAMBDA (x: T1): nu!1(x_section[T1, T2](union(a!1, b!1))(x)))=(reals@real_fun_ops.+)((LAMBDA (x: T1): nu!1(x_section[T1, T2](a!1)(x))),(LAMBDA (x: T1): nu!1(x_section[T1, T2](b!1)(x))))" )"1" (hide -1)"1" (expand "x_section" )"1" rewrite "integral_add[T1, S1, to_measure[T1, S1](mu!1)]" "1" (inst -5 "b!1" ) nil nil )"2" "2" "x_section_measurable[T1,T2]" "Z" "b!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil )"3" (inst -5 "a!1" ) nil nil )"4" "4" "x_section_measurable[T1,T2]" "Z" "a!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"4" expand "member" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -4 -5 2)"2" (apply-extensionality :hide? t)"1" expand "+" )"1" "x_section_disjoint" "X" "a!1" "Y" "b!1" "a" "x!1" ))"1" assert )"1" "x_section(a!1, x!1)" "x_section(b!1, x!1)" )"1" assert )"1" expand "x_section" 1)"1" rewrite "x_section_union" )nil nil ))nil ))nil )"2" "x_section_measurable[T1,T2]" "Z" "b!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"2" expand "member" )"2" (propax) nil nil ))nil ))nil )"3" "x_section_measurable[T1,T2]" "Z" "a!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" expand "member" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "+" )"2" expand "x_section" )"2" "x_section_measurable[T1,T2]" "Z" "a!1" "S1" "S1" "S2" "S2" "x" "x1!1" ))"2" "x_section_measurable[T1,T2]" "Z" "b!1" "S1" "S1" "S2" "S2" "x" "x1!1" ))"2" expand "member" )"2" "nu!1(x_section(a!1, x1!1))" )"2" "nu!1(x_section(b!1, x1!1))" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "x_section" )"3" "x_section_measurable[T1,T2]" "Z" "b!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" expand "member" )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "x_section" )"4" "x_section_measurable[T1,T2]" "Z" "a!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"4" expand "member" )"4" (propax) nil nil ))nil ))nil ))nil ))nil )"5" "5" expand "x_section" )"5" "x_section_measurable[T1,T2]" "Z" "union(a!1,b!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"5" expand "member" )"5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp)"3" expand "x_section" )"3" "x_section_measurable[T1,T2]" "Z" "b!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" expand "member" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (expand "x_section" )"4" "4" "x_section_measurable[T1,T2]" "Z" "a!1" "S1" "S1" "S2" "S2" "x" "x!1" ))"4" expand "member" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp)"5" expand "x_section" )"5" "x_section_measurable[T1,T2]" "Z" "union(a!1,b!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"5" expand "member" )"5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (typepred "X!1" )"3" (expand "o " )"3" (expand "x_section" )"3" "SS" "(LAMBDA (x_1: nat): LAMBDA (x: T1): nu!1(x_section(X!1(x_1), x))))") "1" (replace -1)"1" "FF" "lambda (n:nat): LAMBDA x: nu!1(x_section(IUnion(n,X!1), x))" )"1" case "forall (n:nat): sigma_times(S1,S2)(IUnion(n,X!1))" )"1" case "forall (n: nat): integrable?[T1, S1, to_measure[T1, S1](mu!1)](FF(n))" )"1" case "forall (n:nat,x): 0<=FF(n)(x) & FF(n)(x)<=FF(n+1)(x)" )"1" "ff" "LAMBDA (x: T1): nu!1(x_section(IUnion(X!1), x))" )"1" replace -1)"1" case "forall (n:nat,x): FF(n)(x)<=ff(x)" )"1" "monotone_convergence_scaf[T1, S1, to_measure[T1, S1](mu!1)]" "F" "FF" "f" "ff" ))"1" "series(SS) = integral[T1, S1, to_measure[T1, S1](mu!1)] o FF" )"1" "1" "1" "1" expand "converges_upto?" )"1" "1" "LHS" "integral[T1, S1, to_measure[T1, S1](mu!1)](ff)" )"1" "DRL1" "integral[T1, S1, to_measure[T1, S1](mu!1)] o FF" )"1" "1" "convergence_sequences.limit_lemma" "v" "DRL1" ))"1" "1" rewrite "metric_convergence_def" )"1" expand "convergence" )"1" "RHS" "convergence_sequences.limit(DRL1)" )"1" expand "metric_converges_to" )"1" expand "ball" )"1" expand "member" )"1" case "LHS>RHS" )"1" "1" "DELTA" "(LHS-RHS)/2" )"1" "DELTA" )"1" "DELTA" )"1" "1" "n!1+n!2" )"1" "n!1+n!2" )"1" assert )"1" "triangle" )"1" "LHS - DRL1(n!1 + n!2)" "DRL1(n!1 + n!2) - RHS" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "1" expand "pointwise_convergence?" )"1" "1" "nu!1" )"1" expand "finite_measure?" )"1" "1" "XX" "lambda (n:nat): x_section(X!1(n), x!1)" )"1" case "disjoint?(XX)" )"1" "XX" )"1" "nu!1(IUnion(XX)) = ff(x!1)" )"1" "RHS" "ff(x!1)" )"1" "1" "series(nu!1 o XX)=LAMBDA (n:nat): FF(n)(x!1)" )"1" "LHS" "LAMBDA (n:nat): FF(n)(x!1)" )"1" "1" rewrite "metric_convergence_def" )"1" expand "convergence" )"1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" " n!1" )"1" "1" "i!1" )"1" assert )"1" expand "ball" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (n:nat): series(nu!1 o XX)(n) = FF(n)(x!1)" )"1" nil nil )"2" "2" "n" )"1" expand "FF" )"1" rewrite "IUnion_0_def" )"1" expand "o " )"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "XX" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" expand "sigma" "2" replace "2" expand "o " )"2" expand "FF" )"2" rewrite "IUnion_n_def" )"2" expand "XX" )"2" rewrite "x_section_union" )"2" "fm_disjointunion[T2,S2,nu!1]" "A" "x_section(IUnion(j!1, X!1), x!1)" "B" "x_section(X!1(1 + j!1), x!1)" ))"2" assert )"2" "2" expand "disjoint?" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" expand "x_section" )"2" expand "IUnion" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!1" )"2" "n!2" )"2" "n!2" )"2" "n!2" "1+j!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "ff" )"2" expand "XX" )"2" "IUnion(LAMBDA (n: nat): x_section(X!1(n), x!1))=x_section(IUnion(X!1), x!1)" )"2" "2" "2" expand "IUnion" )"2" expand "x_section" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" assert )"2" "n!1" )"2" expand "XX" )"2" "x_section_measurable[T1,T2]" "Z" "X!1(n!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "XX" )"2" expand "disjoint_indexed_measurable?" )"2" expand "disjoint?" )"2" "2" "i!1" "j!1" )"2" assert )"2" "x_section_disjoint" "X" "X!1(i!1)" "Y" "X!1(j!1)" "a" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "pointwise_increasing?" )"2" "2" case "forall (i,j:nat): FF(i)(x!1)<=FF(i+j)(x!1)" )"1" expand "increasing?" )"1" "1" "x!2" "y!1-x!2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "j" )"1" "1" assert )nil nil ))nil )"2" "2" "i!1" )"2" "i!1+j!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "bounded?" )"3" "1" expand "bounded_above?" )"1" "integral[T1, S1, to_measure(mu!1)](ff)" )"1" expand "o " )"1" "n!1" )"1" "n!1" )"1" "n!1" "_" )"1" "integral_ae_le[T1, S1, to_measure(mu!1)]" "f1" "FF(n!1)" "f2" "ff" ))"1" assert )"1" expand "ae_le?" )"1" expand "pointwise_ae?" )"1" expand "ae?" )"1" expand "fullset" )"1" expand "ae_in?" )"1" "emptyset" )"1" "1" expand "member" )"1" "x!1" )nil nil ))nil ))nil )"2" expand "negligible_set?" )"2" "emptyset[T1]" )"2" assert )"2" "2" "1" expand "null_set?" )"1" expand "measurable_set?" )"1" "mu!1" )"1" expand "mu_fin?" )"1" expand "mu" )"1" expand "to_measure" )"1" expand "finite_measure?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "ff" )"2" "IUnion(X!1)" )nil nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "0" )"2" "2" expand "o " )"2" "integral_nonneg[T1, S1, to_measure(mu!1)]" "f" "FF(x!1)" ))"2" assert )"2" "2" "x!1" "x!2" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (n:nat): series(SS)(n) = integral[T1, S1, to_measure[T1, S1](mu!1)](FF(n))" )"1" "1" "x!1" )"1" assert )"1" expand "o " )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "SS" )"1" expand "FF" )"1" rewrite "IUnion_0_def" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" expand "sigma" "2" replace -1)"2" "2" expand "FF" )"2" rewrite "IUnion_n_def" "2" expand "SS" )"2" "(LAMBDA x: LAMBDA x: nu!1(x_section(IUnion(j!1, X!1), x)),LAMBDA (x: T1): nu!1(x_section(X!1(1 + j!1), x)))") "1" rewrite "integral_add[T1, S1, to_measure[T1, S1](mu!1)]" )"1" "X!1(1 + j!1)" )nil nil )"2" "2" "2" "x_section_measurable[T1,T2]" "Z" "X!1(1+j!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil )"3" "IUnion[[T1, T2]](j!1, X!1)" )"3" "j!1" )nil nil ))nil )"4" "4" "j!1" )"4" "x_section_measurable[T1,T2]" "Z" "IUnion(j!1,X!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"4" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "+" )"1" rewrite "x_section_union" )"1" "fm_disjointunion[T2,S2,nu!1]" "A" "x_section(IUnion(j!1, X!1), x!1)" "B" "x_section(X!1(1 + j!1), x!1)" ))"1" assert )"1" "1" expand "disjoint_indexed_measurable?" )"1" expand "disjoint?" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "x_section" )"1" "1" expand "IUnion" )"1" expand "image" )"1" expand "Union" )"1" "1" "a!1" )"1" "n!2" )"1" "n!2" )"1" "n!2" "1+j!1" )"1" assert )"1" "(x!1, x!2)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "+" )"2" assert )nil nil ))nil ))nil )"3" "3" "x_section_measurable[T1,T2]" "Z" "X!1(1+j!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"3" assert )nil nil ))nil ))nil )"4" "4" "j!1" )"4" "x_section_measurable[T1,T2]" "Z" "IUnion(j!1,X!1)" "S1" "S1" "S2" "S2" "x" "x!1" ))"4" assert )nil nil ))nil ))nil ))nil )"5" "5" "1+j!1" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.1.603Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
