Quelle rs_integral_cont.prf
Sprache: Lisp
(rs_integral_contnil 3494863474"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil rs_integral_cont nil )) nil ))nil 3494863474"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil rs_integral_cont nil )) nil ))nil 3494864317"" (skeep)"" (skeep) (("" (hide -) (("" (grind) nil nil )) nil )) nil )) nil )"real" reals nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"bool" metric_spaces_def nil )"nnreal" real_metric_space nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"odd_int" integers 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 )"[real -> boolean]" rs_integral_cont nil )nil rs_integral_cont nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))nil 3494864317"" (skeep)"" (skeep)"" (hide -)"" (lemma "real_metric_space" ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil )nil real_metric_space 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 )set type-eq-decl nil sets nil )"set" sets nil ))nil ))nil 3492526014"" (skolem 1 ("a" "b" "f" "gg" ))"" (flatten)"" (assert )"" (label "altb" -1)"" (flatten)"" (label "fcont" -2)"" (label "ginc" -3)"" (name "CI" "closed_intv[T](a,b)" )"" (replace -1)"" (label "CIname" -1)"" case "NOT uniformly_continuous?[T,real_dist,real,real_dist](f,CI)" )"1" "ff" "(LAMBDA (x:real): IF T_pred(x) THEN f(x) ELSE 0 ENDIF)" )"1" "Heine[real,real_dist,real,real_dist]" )"1" "LAMBDA (x:real): a<=x AND x<=b" "ff" )"1" assert )"1" "1" "1" expand "uniformly_continuous?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "x!1" "p!1" )"1" assert )"1" expand "ff" )"1" nil nil ))nil ))nil )"2" assert )"2" "p!1" )"2" expand "CI" )"2" nil nil ))nil ))nil ))nil )"3" "x!1" )"3" expand "CI" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fcont" 1))"2" expand "continuous?" )"2" "2" "x!1" )"1" expand "continuous_at?" )"1" "1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" assert )"1" expand "ball" )"1" case "T_pred(x!1) AND T_pred(y!1)" )"1" "1" expand "ff" )"1" assert )nil nil ))nil ))nil )"2" "2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "x!1" )"2" "a" "b" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "CI" )"2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "CI" )"2" "connected_domain" )"2" expand "connected?" )"2" "a" "b" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "closed_intervals_compact" )"3" (inst - "a" "b" ) nil nil ))nil )"4" assert )"4" "4" expand "empty?" )"4" "a" )"4" expand "member" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "funif" -1)"2" (lemma "integrable_lem2" )"2" (inst - "a" "b" "f" "gg" )"2" assert )"2" "1" "1" "eps" )"1" expand "uniformly_continuous?" )"1" "newep" "eps/(2*(abs(gg(b)-gg(a)) + 1))" )"1" "newepname" -1)"1" "funif" "newep" )"1" "funif" "deltaf" )"1" "deltaf/2" )"1" "1" "Pwidth" "1" "RSS1" "RSS2" ))"1" "RSS1" )"1" "RSS1name" "1" "RSS2" )"1" "RSS2name" "1" expand "Riemann_sum?" )"1" "RSS2name" "xis2" )"1" "RSS1name" "xis1" )"1" replace "RSS1name" "1" replace "RSS2name" "1" expand "Rie_sum" "1" rewrite "sigma_minus" )"1" "sigma_abs[below(P`length-1)]" )"1" "1" case "sigma(0, P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" "sigma_le[below(P`length-1)]" )"2" "LAMBDA (n: below(P`length - 1)): " "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" )"2" assert )"2" case "sigma(0, P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )"1" "1" "nn" )"1" case "abs(f(xis1`seq(nn))-f(xis2`seq(nn)))< newep" )"1" "abs(gg(P`seq(1+nn))-gg(P`seq(nn)))" )"1" case "abs(gg(P`seq(1 + nn)) - gg(P`seq(nn))) = gg(P`seq(1 + nn)) - gg(P`seq(nn))" )"1" rewrite "abs_mult" "1" assert )nil nil ))nil )"2" "2" "ginc" )"2" expand "increasing?" "2" expand "restrict" )"2" "P`seq(nn)" "P`seq(1+nn)" )"1" assert )"1" expand "abs" "1" "1" "1" "P" )"1" expand "increasing?" )"1" "nn" "1+nn" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "P" )"2" "1+nn" )nil nil ))nil ))nil )"3" "P" )"3" "nn" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "funif" "xis1`seq(nn)" "xis2`seq(nn)" )"1" assert )"1" expand "real_dist" )"1" "funif" "Pwidth" ))"1" "xis1" )"1" "nn" )"1" "xis2" )"1" "nn" )"1" assert )"1" "1" "width_lem" )"1" "a" "b" "P" "nn" )"1" "width" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xis2" )"2" "nn" )"2" "2" "P" )"2" "nn" )"2" "nn+1" )"2" "2" expand "CI" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "xis1" )"3" "nn" )"3" "3" "P" )"3" "nn" )"3" "nn+1" )"3" "3" expand "CI" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (nn:below(P`length-1)): sigma(0, nn, LAMBDA (n: below(P`length - 1)):") "1" "P`length-2" )"1" assert )"1" replace "1" "P" )"1" replace "1" replace "1" case "(gg(b)-gg(a))*newep < eps" )"1" assert )nil nil )"2" "CC1" "gg(b)-gg(a)" )"2" replace "2" expand "newep" "2" "2" replace "2" assert )"2" quality 98%
¤ 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.0.30Bemerkung:
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Bot Zugriff
2026-03-28
