(ae_continuous_defnil 3451821924"" (skosimp)"" (expand "*" )"" (expand "phi" )"" (expand "member" )"" (expand "ae_continuous?" )"" "{x_1: real | AND AND NOT continuous_at?(LAMBDA IF closed(a!1, b!1)(x)AND x < b!1 AND NOT continuous_at?(f!1, x)}") "1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (case-replace "a!1)"1" (case-replace "x!1)"1" (assert )"1" (rewrite "metric_continuous_at_def" )"1" (rewrite "metric_continuous_at_def" )"1" (expand "metric_continuous_at?" )"1" expand "member" )"1" "IF closed(a!1, b!1)(x!1) THEN 1 ELSE 0 ENDIF * ") "1" "1" "FORALL (epsilon:posreal): ") "1" assert )"1" "1" "epsilon!1" )"1" "1" "DEL" "min(min(b!1-x!1,x!1-a!1),delta!1)" )"1" case "0)"1" "1" "DEL" )"1" "1" "x!2" )"1" "closed(a!1, b!1)(x!2)" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" "2" "epsilon!1" )"2" "2" "DEL" "min(min(b!1-x!1,x!1-a!1),delta!1)" )"2" case "0)"1" "1" "DEL" )"1" "1" "x!2" )"1" "closed(a!1, b!1)(x!2)" )"1" assert )"1" "1" expand "ball" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"hausdorff[T]" "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )"second_countable" real_topology "metric_space/" )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 )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil sets nil )"bool" reals nil )nil real_types 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" continuity_def "topology/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil real_types nil )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed_interval" real_topology "metric_space/" )"(total_order?[real])" nil )"real" ae_continuous_def nil )"real" ae_continuous_def nil )"(strict_total_order?[real])" real_props nil )nil metric_continuity"metric_space/" )"bool" metric_continuity"metric_space/" )"set[T]" metric_space_def "metric_space/" )nil real_types nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" ae_continuous_def nil )"posreal" ae_continuous_def nil )"{p: real | p <= min(b!1 - x!1, x!1 - a!1) AND p <= delta!1}" nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"measurable_set" nil )"real" reals nil )"real" reals nil )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" ae_continuous_def nil )"{p: real | p <= min(b!1 - x!1, x!1 - a!1) AND p <= delta!1}" nil )"bool" ae_continuous_def nil )"nat" measure_space "measure_integration/" ))nil 3452491324"" (skosimp)"" (expand "ae_continuous?" )"" "{x | a!1 < x AND x < b!1 AND NOT continuous_at?(f!1, x)}=emptyset[real]" )"1" (rewrite "null_emptyset" ) nil nil )"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (hide 1)"2" (flatten)"2" (inst - "x!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" ae_continuous_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )set type-eq-decl nil sets nil )"bool" continuity_def "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 )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities 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 )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[T]" "metric_space/" )"real" reals nil )"finite_set[real]" measure_space"measure_integration/" )"(cal_M)" lebesgue_def nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"(lebesgue_measurable)" nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set" finite_sets nil ))nil 3452491205"" (skosimp)"" (expand "ae_continuous?" )"" "{x | a!1 < x AND x < b!1 AND NOT continuous_at?(f!1, x)}=emptyset[real]" )"1" (rewrite "null_emptyset" ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (flatten)"2" (expand "continuous?" )"2" (inst - "x!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" ae_continuous_def nil )"bool" continuity_def "topology/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil measure_theory"measure_integration/" )"set" sets nil )set type-eq-decl nil sets nil )"bool" continuity_def "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 )nil real_types nil )"bool" reals nil )nil sets nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities 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 )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[T]" "metric_space/" )"real" reals nil )"finite_set[real]" measure_space"measure_integration/" )"(cal_M)" lebesgue_def nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"(lebesgue_measurable)" nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set" finite_sets nil ))quality 100%
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
