| products/sources/formale sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ae_continuous_def.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(ae_continuous_def
(ae_continuous_def 0 (ae_continuous_def-1 nil 3451821924 ("" (skosimp) (("" (expand "*") (("" (expand "phi") (("" (expand "member") (("" (expand "ae_continuous?") (("" (case-replace "{x_1: real | a!1 < x_1 AND x_1 < b!1 AND NOT continuous_at?(LAMBDA (x: real): IF closed(a!1, b!1)(x) THEN 1 ELSE 0 ENDIF * f!1(x), x_1)}={x | a!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" (case-replace "IF closed(a!1, b!1)(x!1) THEN 1 ELSE 0 ENDIF * f!1(x!1)=f!1(x!1)") (("1" (hide -1) (("1" (case-replace "FORALL (epsilon:posreal): EXISTS (delta:posreal): FORALL (x: real): ball(x!1, delta)(x) => ball(f!1(x!1), epsilon)(f!1(x))") (("1" (assert) (("1" (skosimp) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (name "DEL" "min(min(b!1-x!1,x!1-a!1),delta!1)") (("1" (case "0 (("1" (flatten) (("1" (inst + "DEL") (("1" (skosimp) (("1" (inst -4 "x!2") (("1" (case-replace "closed(a!1, b!1)(x!2)") (("1" (assert) (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2 -4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (skosimp) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (name "DEL" "min(min(b!1-x!1,x!1-a!1),delta!1)") (("2" (case "0 (("1" (flatten) (("1" (inst + "DEL") (("1" (skosimp) (("1" (inst -7 "x!2") (("1" (case-replace "closed(a!1, b!1)(x!2)") (("1" (assert) (("1" (hide 1) (("1" (expand "ball") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -7) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -4 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 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) ((* const-decl "[T -> real]" real_fun_ops "reals/") (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_space_is_hausdorff name-judgement "hausdorff[T]" real_continuity "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_continuity "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (continuous_at? const-decl "bool" continuity_def "topology/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (a!1 skolem-const-decl "real" ae_continuous_def nil) (b!1 skolem-const-decl "real" ae_continuous_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_continuous_at_def formula-decl nil metric_continuity "metric_space/") (metric_continuous_at? const-decl "bool" metric_continuity "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "real" ae_continuous_def nil) (delta!1 skolem-const-decl "posreal" ae_continuous_def nil) (DEL skolem-const-decl "{p: real | p <= min(b!1 - x!1, x!1 - a!1) AND p <= delta!1}" ae_continuous_def nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (delta!1 skolem-const-decl "posreal" ae_continuous_def nil) (DEL skolem-const-decl "{p: real | p <= min(b!1 - x!1, x!1 - a!1) AND p <= delta!1}" ae_continuous_def nil) (ae_continuous? const-decl "bool" ae_continuous_def nil) (phi const-decl "nat" measure_space "measure_integration/")) shostak)) (continuous_at_is_ae_continuous 0 (continuous_at_is_ae_continuous-1 nil 3452491324 ("" (skosimp) (("" (expand "ae_continuous?") (("" (case-replace "{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) ((ae_continuous? const-decl "bool" ae_continuous_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (null_emptyset judgement-tcc nil measure_theory "measure_integration/") (emptyset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (continuous_at? const-decl "bool" continuity_def "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_continuity "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[T]" real_continuity "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration/") (subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (outer_negligible_emptyset name-judgement "outer_negligible[real, lebesgue_outer_measure]" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (continuous_is_ae_continuous 0 (continuous_is_ae_continuous-1 nil 3452491205 ("" (skosimp) (("" (expand "ae_continuous?") (("" (case-replace "{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) ((ae_continuous? const-decl "bool" ae_continuous_def nil) (continuous? const-decl "bool" continuity_def "topology/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (null_emptyset judgement-tcc nil measure_theory "measure_integration/") (emptyset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (continuous_at? const-decl "bool" continuity_def "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_continuity "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[T]" real_continuity "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration/") (subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (outer_negligible_emptyset name-judgement "outer_negligible[real, lebesgue_outer_measure]" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
