(real_fun_on_compact_setsnil 3460717941"" (lemma "fullset_metric_space" ) (("" (propax) nil nil )) nil )nil real_fun_on_compact_setsnil ))nil ))nil 3460717941"" (lemma "real_metric_space" )"" (inst - "fullset[real]" ) nil nil )) 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 ) (fullset const-decl "set" sets nil )nil real_metric_space nil ))nil ))nil 3460718129"" (skosimp*)"" (label "cont" -1)"" (label "compact" -2)"" (label "empty" 1)"" (label "maxexists" 2)"" (lemma "compact_sequence_limit[T,d]" )"" (label "csl" -1)"" (inst "csl" "S!1" )"" (expand "nonempty?" )"" (prop)"" case "bounded_real_defs.bounded?(image(f!1,S!1))" )"1" (label "bounded" -1)"1" (expand "bounded?" )"1" (prop)"1" "bbel" -2)"1" "bbel" )"1" "real_complete" )"1" "lub" -1)"1" "lub" "image(f!1,S!1)" )"1" expand "bounded_above?" )"1" "1" "1" "1" expand "least_upper_bound?" )"1" "1" "lub2" -2)"1" "seq" "(LAMBDA (n: nat): choose({s: T | S!1(s) AND y!1-f!1(s) < 1/(n+1)}))" )"1" "seq_def" "1" "csl" "seq" )"1" "1" "maxexists" "p!1" )"1" "maxexists2" "1" "lub" )"1" "lub3" "1" expand "upper_bound?" "lub" )"1" "1" "lub" "f!1(t!1)" )"1" case "y!1 = f!1(t!1)" )"1" replace "1" expand "upper_bound?" "lub3" )"1" "maxexists2" "t!1" )"1" "1" "lub3" "f!1(t!2)" )"1" expand "image" )"1" "t!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "A" "y!1 - f!1(t!1)" )"2" expand "continuous?" )"2" "cont" "p!1" )"2" expand "continuous_at?" )"2" expand "member" )"2" expand "ball" )"2" "cont" "A/2" )"1" "1" "archimedean" )"1" "A/4" )"1" "1" "both_sides_div_pos_lt2" )"1" "n!1+1" "n!1" "1" )"1" assert )"1" "1" "-" "1/n!1" "1" assert )"1" "csl" "delta!1/2" "n!1" )"1" "1" "n!2" )"1" "+" "1" "1" "n1n2" "1" "arch1" "1" "Adef" "1" "cont" "seq(n!2)" )"1" "1" "cont" )"1" "compact" )"1" "seq(n!2)" )"1" "ge2" "1" "both_sides_div_pos_ge2" )"1" "recip" "1" "recip" "n!1 + 1" "n!2 + 1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "compact" )"2" "seq(n!2)" )"2" "n!2le" "2" "seqn!2tp" "2" "both_sides_div_pos_ge2" )"2" "bsxyz" "2" "bsxyz" "n!1 + 1" "n!2+1" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "compact" )"3" "seq(n!2)" )"3" "n!2le" "3" "seqn!2tp" "3" "both_sides_div_pos_ge2" )"3" "bsxyz" "3" "bsxyz" "n!1 + 1" "n!2 + 1" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "compact" )"4" "seq(n!2)" )"4" "n!2le" "4" "seqn!2tp" "4" "both_sides_div_pos_ge2" )"4" "bsxyz" "4" "bsxyz" "n!1 + 1" "n!2 + 1" "1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fullset_metric_space" )"2" expand "metric_space?" )"2" expand "space_symmetric?" )"2" "2" "p!1" "seq(n!2)" )"1" replace "1" assert )nil nil ))nil )"2" expand "fullset" )"2" nil nil ))nil )"3" expand "fullset" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "n!1*n!1" )"1" nil nil ))nil )"2" "n!1*n!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" "t!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "lub2" "y!1-1/(1+n!1)" )"2" "1" assert )nil nil )"2" expand "upper_bound?" "2" expand "image" )"2" "2" "s!1" )"2" expand "image" )"2" "2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "seq" "(LAMBDA (n: nat): choose({s: T | S!1(s) AND f!1(s) > n}))" )"1" "csl" "seq" )"1" "1" "axiom_of_archimedes" )"1" "f!1(p!1)" )"1" "1" expand "continuous?" )"1" "cont" "p!1" )"1" expand "continuous_at?" )"1" "cont" "1" )"1" "1" "csl" "delta!1" "max(i!1,0) + 2" )"1" "1" "n!1" )"1" "cont" "seq(n!1)" )"1" expand "member" )"1" expand "ball" )"1" "1" assert )"1" nil nil ))nil )"2" "fullset_metric_space" )"2" expand "metric_space?" )"2" expand "space_symmetric?" )"2" "2" "p!1" "seq(n!1)" )"1" replace "1" nil nil ))nil )"2" expand "fullset" )"2" nil nil ))nil )"3" expand "fullset" )"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 )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "lub" "n!1" )"2" expand "upper_bound?" "2" "2" "s!1" )"2" expand "image" )"2" "2" "x!3" )"2" expand "member" )"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" (expand "bounded?" )"2" (expand "bounded_above?" )"2" (expand "bounded_below?" )"2" "1" "seq" "(LAMBDA (n: nat): choose({s: T | S!1(s) AND f!1(s) > n}))" )"1" "csl" "seq" )"1" "1" expand "continuous?" )"1" "cont" "p!1" )"1" expand "continuous_at?" )"1" "cont" 1)"1" "1" expand "member" )"1" expand "ball" )"1" "axiom_of_archimedes" )"1" "f!1(p!1)" )"1" "1" "csl" "delta!1" "max(i!1,0) + 3" )"1" "1" "n!1" )"1" "n!1" )"1" expand "upper_bound?" )"1" "cont" "seq(n!1)" )"1" "1" "1" "s!1" )"1" expand "image" )"1" "1" "cont" )nil nil ))nil ))nil ))nil ))nil )"2" "fullset_metric_space" )"2" expand "metric_space?" )"2" expand "space_symmetric?" )"2" "2" "p!1" "seq(n!1)" )"1" replace "1" nil nil ))nil )"2" expand "fullset" )"2" nil nil ))nil )"3" expand "fullset" )"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 )"2" "2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "n!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" expand "image" )"2" "2" "x!2" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "seq" "(LAMBDA (n: nat): choose({s: T | S!1(s) AND f!1(s) < -n}))" )"1" "csl" "seq" )"1" "1" expand "continuous?" )"1" expand "continuous_at?" )"1" "cont" "p!1" )"1" "cont" "1" )"1" "1" "axiom_of_archimedes" )"1" "-f!1(p!1)" )"1" "1" "csl" "delta!1" "max(i!1,0) + 5" )"1" "1" "n!1" )"1" expand "member" )"1" expand "ball" )"1" "cont" "seq(n!1)" )"1" "1" "cont" )nil nil )"2" "fullset_metric_space" )"2" expand "metric_space?" )"2" "2" expand "space_symmetric?" )"2" "p!1" "seq(n!1)" )"1" replace "1" nil nil ))nil )"2" expand "fullset" )"2" nil nil ))nil )"3" expand "fullset" )"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 )"2" expand "nonempty?" )"2" expand "empty?" )"2" "2" expand "member" )"2" "-n!1 - 1" )"2" expand "lower_bound?" )"2" "2" "s!1" )"2" expand "image" )"2" "2" "x!2" )"2" replace -2)"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 )"3" (expand "nonempty?" )"3" (expand "empty?" )"3" (expand "member" )"3" "3" "f!1(x!1)" )"3" expand "image" )"3" (inst + "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> nnreal]" real_fun_on_compact_setsnil )nil real_types nil )"bool" reals 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_fun_on_compact_sets nil )nil compactness nil )set type-eq-decl nil sets nil )"T" real_fun_on_compact_sets nil )"bool" bounded_real_defs nil )"[numfield -> numfield]" number_fields nil )"int" integers nil )"(S!1)" real_fun_on_compact_sets nil )"[n: nat -> ({s: T | S!1(s) AND f!1(s) < -n})]" nil )"int" real_fun_on_compact_sets nil )"above(5 + max(i!1, 0))" nil )"bool" bounded_real_defs nil )"(S!1)" real_fun_on_compact_sets nil )"[n: nat -> ({s: T | S!1(s) AND f!1(s) > n})]" nil )"int" real_fun_on_compact_sets nil )"above(3 + max(i!1, 0))" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"(S!1)" real_fun_on_compact_sets nil )"odd_int" integers nil )"bool" continuity_ms_def nil )"bool" continuity_ms_def nil )"set[T]" metric_spaces nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"real" reals nil )"even_int" integersnil )"odd_int" integers nil )"posrat" nil )"rat" rationals nil )"int" integers nil )"posreal" nil )nil integers nil )nil integers nil )nil real_props nil )"real" real_fun_on_compact_sets nil )"nnreal" real_metric_space nil )"set" sets nil )"bool" sets nil )"bool" metric_spaces nil )"bool" compactness nil )"bool" functions nil )"bool" finite_sets nil )"bool" compactness nil )"bool" compactness nil )"bool" sets nil )"bool" metric_spaces_def nil )"above(n!1)" real_fun_on_compact_sets nil )"posnat" real_fun_on_compact_sets nil )"[n: nat -> ({s: T | S!1(s) AND y!1 - f!1(s) < 1 / (n + 1)})]" nil )"(S!1)" real_fun_on_compact_sets nil )"set" sets nil )"bool" metric_spaces_def nil )nil real_fun_on_compact_setsnil )nil real_props nil )"bool" integers nil )nil real_props nil )nil real_props nil )"odd_int" integers nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil extra_real_propsnil )"even_int" integersnil )nil real_props nil )nil real_props nil )nil real_props nil )"real" reals nil )"posrat" nil )nil integers nil )nil integers nil )nil real_props nil )nil real_types nil )nil real_types nil )"bool" reals nil )"real" real_fun_on_compact_sets nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"(S!1)" real_fun_on_compact_sets nil )"set[T]" real_fun_on_compact_sets nil )"[T -> real]" real_fun_on_compact_sets nil )"bool" bounded_real_defs nil )"posint" nil )"real" reals nil )"posint" nil )"posrat" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"(p)" sets nil )nil real_props nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"above(2 + max(i!1, 0))" nil )"int" real_fun_on_compact_sets nil )"[n: nat -> ({s: T | S!1(s) AND f!1(s) > n})]" nil )"(S!1)" real_fun_on_compact_sets nil )nil bounded_real_defs nil )"set[R]" function_image nil )"bool" bounded_real_defs nil )"bool" sets nil ))nil ))nil 3460718233"" (skosimp*)"" (lemma "cont_on_compact_max" )"" (inst - "S!1" "(Lambda (x: T): -f!1(x))" )"" (assert )"" (prop)"1" (skosimp*)"1" (inst + "s!1" )"1" (skosimp*)"1" (inst - "t!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "continuous?" )"2" (skosimp*)"2" (inst - "x!1" )"2" (expand "continuous_at?" )"2" (skosimp*)"2" (inst - "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "y!1" )"2" expand "member" )"2" expand "ball" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_fun_on_compact_sets nil )"bool" continuity_ms_def nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" real_metric_space nil )"set" sets nil )"bool" sets nil )"bool" metric_spaces nil )"[T, T -> nnreal]" real_fun_on_compact_setsnil )nil real_types nil )"bool" compactness nil )"bool" functions nil )"bool" finite_sets nil )"bool" compactness nil )"bool" compactness nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"set[T]" metric_spaces nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil real_fun_on_compact_sets nil )"real" reals nil ))nil )))
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.0.69Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01)
¤ *Bot Zugriff
