Quelle real_borel.prf
Sprache: Lisp
(real_borelnil 3425663944"" "borel_countable_basis" "B" "fullset[rational_open_interval]" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (lemma "countable_rational_open_interval" )"2" (expand "fullset" )"2" (expand "extend" )"2" (expand "is_countable" )"2" (skosimp)"2" (typepred "f!1" )"2" (inst + "f!1" )"2" (split)"1" (skosimp) (("1" (prop) nil nil )) nil )"2" (expand "injective?" )"2" (skosimp)"2" (inst - "x1!1" "x2!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" )"2" (expand "extend" )"2" (hide 2)"2" (expand "metric_induced_topology" )"2" (expand "base?" )"2" (split)"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp)"1" (prop)"1" (skosimp)"1" (replace -1)"1" "metric_open_ball" "x" "q!1" "r" "pq!1" ))"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "A!1" )"2" "{X:set[real]| EXISTS (q:rat,pq:posrat): X=ball(q,pq) & subset?[real](X,A!1)}" )"2" (split)"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp)"1" "1" "1" (inst + "q!1" "pq!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality :hide? t)"2" (case-replace "A!1(x!1)" )"1" (expand "Union" )"1" expand "metric_open?" )"1" "x!1" )"1" assert )"1" "1" "density" "x" "x!1-r!1" "y" "x!1" ))"1" "density" "x" "x!1" "y" "x!1+r!1" ))"1" assert )"1" "1" "ball((r!3+r!2)/2,abs((r!3-r!2)/2))" )"1" expand "ball" )"1" nil nil ))nil )"2" "(r!2 + r!3) / 2" "abs((r!3 - r!2) / 2)" )"1" expand "subset?" )"1" "1" "x!2" )"1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" expand "Union" )"2" "2" "a!1" )"2" "2" expand "subset?" )"2" "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 )"real" reals nil )"set" sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"odd_int" integers nil )"rat" rationals nil )"({S | metric_open?(S)})" real_borel nil )"rat" real_borel nil )"rat" real_borel nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"rat" rationals nil )"rat" rationals nil )"{r: nonneg_rat | r >= q}" nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"(partial_order?[set[T]])" nil )"(strict_total_order?[real])" real_props nil )nil rational_props nil )"bool" metric_space_def "metric_space/" )"bool" sets nil )nil metric_space "metric_space/" )"bool" sets nil )nil real_topology"metric_space/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"(injective?[({x | TRUE}), nat])" real_borelnil )"bool" functions nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )"bool" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" countability "sets_aux/" )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )nil borel nil )"bool" topology_prelim "topology/" )nil topology_prelim "topology/" )"bool" basis "topology/" )set type-eq-decl nil sets nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )nil rationals nil )"bool" reals nil )nil rationals nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"set[T]" metric_space_def "metric_space/" )nil real_topology"metric_space/" )"bool" booleans nil )"R" extend nil )"set" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" ))nil 3425664555"" (apply-extensionality :hide? t)"1" (expand "fullset" )"1" (rewrite "borel_generated_by_rational_open_interval" )"1" (expand "fullset" )"1" "generated_sigma_algebra(extend ") "1" (expand "extend" )"1" (expand "generated_sigma_algebra" )"1" (expand "Intersection" )"1" (skosimp)"1" (typepred "a!1" )"1" (inst - "a!1" )"1" (expand "subset?" )"1" (expand "member" )"1" (skosimp*)"1" "1" "1" "x!2" )"1" "1" "q!1" "pq!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "extend" )"2" (expand "generated_sigma_algebra" )"2" (expand "Intersection" )"2" (skosimp)"2" (typepred "a!1" )"2" (expand "subset?" -2)"2" (expand "member" )"2" (inst -3 "a!1" )"2" expand "subset?" )"2" expand "member" )"2" "2" "2" "2" replace -1)"2" "2" "VV" "{X:set[real]| EXISTS (q:rat,pq:posrat): X = ball(q,pq) & subset?[real](ball(q,pq),ball(x!3,r!1))}" )"2" "ball(x!3, r!1) = Union(VV)" )"1" expand "sigma_algebra?" )"1" expand "sigma_algebra_union?" )"1" "1" "VV" )"1" expand "member" )"1" "1" nil nil )"2" "2" "countable_rational_open_interval" )"2" expand "is_countable" )"2" "2" "f!1" )"2" "lambda (x:(VV)): f!1(x)" )"1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" "x1!1" "x2!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!4" )"2" expand "VV" )"2" "2" expand "fullset" )"2" "q!1" "pq!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!4" )"3" replace "3" assert )"3" "3" "x!4" )"3" assert )"3" "3" "q!1" "pq!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ball(x!3, r!1)(x!4)" )"1" expand "Union" )"1" "1" expand "ball" )"1" case "x!3-r!1<x!4&x!4<x!3+r!1" )"1" "1" "density" "x" "x!3-r!1" "y" "x!4" ))"1" "density" "x" "x!4" "y" "x!3+r!1" ))"1" assert )"1" "1" "XX" "(r!2+r!3)/2" )"1" "RR" "(r!2-r!3)/2" )"1" "ball(XX,RR)" )"1" expand "ball" )"1" nil nil ))nil )"2" expand "VV" )"2" "XX" "RR" )"1" expand "ball" )"1" nil nil ))nil )"2" assert )nil nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "Union" )"2" "2" "a!2" )"2" expand "VV" )"2" "2" "2" "2" expand "subset?" )"2" expand "member" )"2" "x!4" )"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" "metric_induced_topology[real, (LAMBDA (x, y: real): abs(x - y))]" )"2" (expand "hausdorff_space?" ) (("2" (propax) nil nil )) nil ))nil ))nil )"({Y | AND LAMBDA (t: setof[real]):IF EXISTS q, pq: t = ball(q, pq) THEN TRUE ELSE FALSE ENDIF," real_borel nil) "real" reals nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil rational_props nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"rat" real_borel nil )"rat" real_borel nil )"rat" rationals nil )"rat" rationals nil )"odd_int" integers nil )"real" real_borel nil )"real" reals nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" countability "sets_aux/" )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" functions nil )"(injective?[(fullset[rational_open_interval]), nat])" real_borelnil )"[set[real] -> boolean]" real_borel nil )nil real_topology"metric_space/" )"bool" subset_algebra_def nil )"set" sets nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" sets nil )"({Y | AND LAMBDA (t: setof[real]):IF EXISTS x, r: t = ball(x, r) THEN TRUE ELSE FALSE ENDIF," real_borel nil) "(partial_order?[set[T]])" nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )nil rationals nil )nil rationals nil )nil real_topology"metric_space/" )"bool" booleans nil )nil nil )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"real" reals nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel nil )"sigma_algebra" nil )set type-eq-decl nil sets nil ) (> const-decl "bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"set[T]" metric_space_def "metric_space/" )nil real_topology"metric_space/" )"bool" booleans nil )"R" extend nil )"set" sets nil )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3509858353"" (skosimp)"" (lemma "open_is_borel" ("X" "A!1" ))"1" (expand "real_borel" ) (("1" (propax) nil nil )) nil )"2" (typepred "A!1" )"2" (skosimp)"2" (replace -1)"2" (assert )"2" (hide 2)"2" (expand "open?" )"2" (expand "member" )"2" (expand "metric_induced_topology" )"2" (assert )"2" (rewrite "metric_open_ball" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_topology"metric_space/" )"set[T]" metric_space_def "metric_space/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil topology "topology/" )"bool" topology "topology/" )set type-eq-decl nil sets nil )nil borel nil )"sigma_algebra" real_borel nil )nil metric_space "metric_space/" )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3509858388"" (skosimp)"" (typepred "B!1" )"" (skosimp)"" (typepred "closed_ball(x!1, r!1)" )"" (expand "real_borel" )"" (lemma "closed_is_borel" ("Y" "B!1" ))"1" (propax) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil borel nil )"sigma_algebra" real_borel nil ))nil 3509858573"" (skosimp)"" (typepred "L!1" )"" (skosimp)"" (expand "real_borel" )"" (lemma "closed_is_borel" ("Y" "L!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"sigma_algebra" real_borel nil )nil borel nil ))nil 3509858604"" (skosimp)"" (expand "real_borel" )"" (typepred "R!1" )"" (skosimp)"" (lemma "closed_is_borel" ("Y" "R!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"sigma_algebra" real_borel nil )nil borel nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil sets nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" ))nil 3425663719"" (skolem + "X!1" )"" (lemma "open_interval_borel_rew" ("A" "X!1" ))"" (expand "real_borel" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_topology"metric_space/" )"set[T]" metric_space_def "metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_borel nil )"sigma_algebra" real_borel nil ))nil ))nil 3425710076"" (skolem + "A!1" )"" (lemma "closed_interval_borel_rew" ("B" "A!1" ))"" (expand "real_borel" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_borel nil )"sigma_algebra" real_borel nil ))nil ))nil 3509858281"" (skolem + "X!1" )"" (lemma "left_semiclosed_interval_borel_rew" ("L" "X!1" ))"" (expand "real_borel" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_borelnil )"sigma_algebra" real_borel nil ))nil ))nil 3509858281"" (skolem + "X!1" )"" (lemma "right_semiclosed_interval_borel_rew" ("R" "X!1" ))"" (expand "real_borel" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_borelnil )"sigma_algebra" real_borel nil ))nil ))nil 3509858895"" (apply-extensionality :hide? t)"" "generated_sigma_algebra_subset2" "X" "fullset[left_semiclosed_interval]" "Y" "(borel?)" ))"" (split)"1" (expand "subset?" )"1" (expand "member" )"1" (inst - "x!1" )"1" (case-replace "borel?(x!1)" )"1" (rewrite "borel_generated_by_open_interval" )"1" (expand "fullset" )"1" (expand "extend" )"1" (expand "generated_sigma_algebra" )"1" (expand "Intersection" )"1" (skosimp)"1" (typepred "a!1" )"1" expand "subset?" )"1" expand "member" )"1" "a!1" )"1" expand "subset?" )"1" expand "member" )"1" "1" "1" "1" "1" "AA" "lambda (n:nat): difference[real](closed_inf(x!3-r!1+1/(1+n)),closed_inf(x!3+r!1))" )"1" "x!2=IUnion(AA)" )"1" "1" case "forall (n:nat): a!1(AA(n))" )"1" assert )"1" expand "sigma_algebra?" )"1" "1" "1" expand "sigma_algebra_union?" )"1" "image(AA,fullset[nat])" )"1" "countable_image[nat,set[real]]" )"1" "fullset[nat]" "AA" )"1" "1" expand "image" "1" replace "1" "1" expand "member" )"1" "Union(image(AA, fullset[nat]))=IUnion(AA)" )"1" "1" "1" expand "IUnion" )"1" "(EXISTS (i: nat): AA(i)(x!4))" )"1" "1" expand "fullset" )"1" expand "image" )"1" expand "Union" )"1" "AA(i!1)" )"1" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "fullset" )"2" expand "image" )"2" expand "Union" )"2" "2" "a!2" )"2" "n!1" )"2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!4" )"2" expand "fullset" )"2" expand "image" )"2" expand "member" )"2" "2" "x!5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:nat): n" )"2" expand "injective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "AA" )"2" "closed_inf(r!1 + x!3)" )"2" "closed_inf(1 / (1 + n!1) - r!1 + x!3)" )"2" "1" "1" "X1" "closed_inf(1 / (1 + n!1) - r!1 + x!3)" )"1" "X2" "closed_inf(r!1 + x!3)" )"1" "sigma_union_implies_subset_union[real]" "S" "a!1" ))"1" expand "sigma_algebra?" )"1" "1" assert )"1" rewrite "difference_intersection" )"1" "demorgan1[real]" "a" "complement[real](X1)" "b" "X2" ))"1" rewrite "complement_complement" )"1" replace "1" "1" expand "subset_algebra_union?" )"1" expand "subset_algebra_complement?" )"1" expand "member" )"1" "X1" )"1" "complement[real](X1)" "X2" )"1" "union[real](complement[real](X1), X2)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "r!1+x!3" )nil nil ))nil )"2" nil nil )"3" "1 / (1 + n!1) - r!1 + x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -2)"2" "2" "r!1" )"2" expand "ball" )"2" "2" "IUnion(AA)(x!4)" )"1" expand "IUnion" )"1" "1" expand "AA" )"1" expand "difference" )"1" expand "member" )"1" expand "closed_inf" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" expand "AA" )"2" expand "closed_inf" )"2" expand "difference" )"2" expand "member" )"2" "archimedean" "px" "x!4-x!3+r!1" ))"2" "2" "n!1-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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "fullset" )"2" (expand "extend" )"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp)"2" (prop)"2" (skosimp)"2" (lemma "closed_is_borel" ("Y" "x!2" ))"1" (propax) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )nil nil )nil borel nil )"bool" sets nil )nil real_borel nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"posint" nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"int" integers nil )nil integers nil )nil integers nil )"nzrat" rationalsnil )"int" integers nil )"(total_order?[real])" nil )nil sets_lemmas nil )"set" sets nil )"bool" subset_algebra_def nil )"closed[real, (metric_induced_topology)]" nil )"closed[real, (metric_induced_topology)]" nil )"set" sets nil )"bool" subset_algebra_defnil )nil sets_lemmas nil )"open[T, S]" nil )nil sets_lemmas nil )nil nil )"posrat" nil )"odd_int" integers nil )"bool" subset_algebra_def nil )nil countable_image "sets_aux/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"[nat -> set[real]]" real_borel nil )"nat" real_borel nil )"set" sets nil )"set[R]" function_image nil )"bool" functions nil )"bool" countability "sets_aux/" )"set[R]" function_image nil )"set[T]" indexed_sets nil )"({Y | AND LAMBDA (t: setof[real]):IF EXISTS a: t = closed_inf(a) THEN TRUE ELSE FALSE ENDIF," real_borel nil) "bool" reals nil )nil real_types nil )"set[T]" metric_space_def "metric_space/" )"(partial_order?[set[T]])" nil )"bool" sets nil )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"real" reals nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel nil )"sigma_algebra" nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" booleans nil )"R" extend nil )"set" sets nil )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3509875785"" (apply-extensionality :hide? t)"" "generated_sigma_algebra_subset2" "X" "fullset[right_semiclosed_interval]" "Y" "(borel?)" ))"" (split)"1" (expand "subset?" )"1" (expand "member" )"1" (inst - "x!1" )"1" (case-replace "borel?(x!1)" )"1" (rewrite "borel_generated_by_open_interval" )"1" (expand "fullset" )"1" (expand "extend" )"1" (expand "generated_sigma_algebra" )"1" (expand "Intersection" )"1" (skosimp)"1" (typepred "a!1" )"1" expand "subset?" )"1" expand "member" )"1" "a!1" )"1" expand "subset?" )"1" expand "member" )"1" "1" "1" "1" "1" "AA" "lambda (n:nat): difference[real](inf_closed(x!3+r!1-1/(1+n)),inf_closed(x!3-r!1))" )"1" "x!2=IUnion(AA)" )"1" "1" case "forall (n:nat): a!1(AA(n))" )"1" assert )"1" expand "sigma_algebra?" )"1" expand "sigma_algebra_union?" )"1" "1" "1" "image(AA)(fullset[nat])" )"1" expand "member" )"1" "1" expand "image" )"1" "Union(image(AA, fullset[nat]))=IUnion(AA)" )"1" "1" "1" "IUnion(AA)(x!4)" )"1" "IUnion(AA)(x!4)" )"1" expand "fullset" )"1" expand "image" )"1" expand "Union" )"1" expand "IUnion" )"1" "1" "AA(i!1)" )"1" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "fullset" )"2" expand "image" )"2" expand "Union" )"2" expand "IUnion" )"2" "2" "a!2" )"2" "2" "x!5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "countable_image[nat,set[real]]" )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:nat): n" )"2" expand "injective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "x!4" )"3" expand "fullset" )"3" expand "image" )"3" expand "image" )"3" "3" "x!5" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "AA" )"2" "inf_closed(r!1 - 1 / (1 + n!1) + x!3)" )"2" "inf_closed(x!3-r!1)" )"2" assert )"2" "1" assert )"1" "X1" "inf_closed(r!1 - 1 / (1 + n!1) + x!3)" )"1" "X2" "inf_closed(x!3 - r!1)" )"1" "sigma_union_implies_subset_union[real]" "S" "a!1" ))"1" expand "sigma_algebra?" )"1" "1" assert )"1" rewrite "difference_intersection" )"1" "demorgan1[real]" "a" "complement[real](X1)" "b" "X2" ))"1" rewrite "complement_complement" )"1" replace "1" "1" expand "subset_algebra_complement?" )"1" expand "subset_algebra_union?" )"1" expand "member" )"1" "X1" )"1" "complement[real](X1)" "X2" )"1" "union[real](complement[real](X1),X2)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "r!1 - 1 / (1 + n!1) + x!3" )nil nil )"3" "x!3-r!1" )nil nil )"4" "r!1 - 1 / (1 + n!1) + x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -2)"2" "2" expand "ball" )"2" "abs(x!3 - x!4) < r!1" )"1" expand "AA" )"1" expand "IUnion" )"1" expand "inf_closed" )"1" expand "difference" )"1" expand "member" )"1" assert )"1" "r!1" )"1" "archimedean" "px" "r!1+x!3-x!4" ))"1" "1" "n!1-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "IUnion" )"2" "2" expand "AA" )"2" expand "inf_closed" )"2" expand "difference" )"2" expand "member" )"2" "2" "r!1" )"2" assert )"2" 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" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "fullset" )"2" (expand "extend" )"2" (expand "subset?" )"2" (expand "member" )"2" (skosimp)"2" (prop)"2" (skosimp)"2" "closed_is_borel" "Y" "inf_closed(a!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "real_borel" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil nil )"sigma_algebra" real_borel nil )nil borel nil )"bool" sets nil )nil real_borel nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"posint" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"nzrat" rationalsnil )"int" integers nil )"posrat" nil )"odd_int" integers nil )nil nil )nil sets_lemmas nil )"open[T, S]" nil )nil sets_lemmas nil )"bool" subset_algebra_def nil )"set" sets nil )"closed[real, (metric_induced_topology)]" nil )"closed[real, (metric_induced_topology)]" nil )"bool" subset_algebra_defnil )"set" sets nil )nil sets_lemmas nil )"real" reals nil )"bool" subset_algebra_def nil )"bool" countability "sets_aux/" )"bool" functions nil )nil countable_image "sets_aux/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"nat" real_borel nil )"[nat -> set[real]]" real_borel nil )"set" sets nil )"set[R]" function_image nil )"set[R]" function_image nil )"set[T]" indexed_sets nil )"({Y | AND LAMBDA (t: setof[real]):IF EXISTS a: t = inf_closed(a) THEN TRUE ELSE FALSE ENDIF," real_borel nil) "bool" reals nil )nil real_types nil )"set[T]" metric_space_def "metric_space/" )"(partial_order?[set[T]])" nil )"bool" sets nil )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"real" reals nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel nil )"sigma_algebra" nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" booleans nil )"R" extend nil )"set" sets nil )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.111 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
