| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 267 kB |
|
Quelle cross_metric_uniform_continuity.prf Sprache: Lisp |
|||||||||
|
(cross_metric_uniform_continuity
(IMP_cross_metric_spaces_TCC1 0 (IMP_cross_metric_spaces_TCC1-1 nil 3460217227 ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil) ((fullset_metric_space1 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (IMP_cross_metric_spaces_TCC2 0 (IMP_cross_metric_spaces_TCC2-1 nil 3460217227 ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil) ((fullset_metric_space2 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (IMP_continuity_ms_def_TCC1 0 (IMP_continuity_ms_def_TCC1-1 nil 3460217227 ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil) ((product_is_metric formula-decl nil cross_metric_spaces nil) (T1 formal-nonempty-type-decl nil cross_metric_uniform_continuity nil) (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 "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_uniform_continuity nil) (T2 formal-nonempty-type-decl nil cross_metric_uniform_continuity nil) (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_uniform_continuity nil)) nil)) (IMP_continuity_ms_def_TCC2 0 (IMP_continuity_ms_def_TCC2-1 nil 3460217227 ("" (lemma "fullset_metric_space3") (("" (propax) nil nil)) nil) ((fullset_metric_space3 formula-decl nil cross_metric_uniform_continuity nil)) nil)) (multiary_Heine 0 (multiary_Heine-2 nil 3565651140 ("" (skosimp*) (("" (label "comp" -1) (("" (label "cont" -2) (("" (label "unif" 1) (("" (lemma "one_variable_unif_cont_sequence") (("" (label "epsq" -1) (("" (inst "epsq" "X!1" "Y!1" "f!1") (("" (assert) (("" (skosimp*) (("" (lemma "compact_sequence_limit[T1,d1]") (("" (label "csl" -1) (("" (inst "csl" "X!1") (("" (assert) (("" (prop) (("1" (inst "csl" "(LAMBDA (n: nat): IF n = 0 THEN seq!1(1)`1 ELSE seq!1(n)`1 ENDIF)") (("1" (skosimp*) (("1" (lemma "product_cont_product_subset") (("1" (label "pcps" -1) (("1" (inst "pcps" "X!1" "Y!1" "f!1") (("1" (assert) (("1" (inst "pcps" "p!1" "y!1" "epsilon!1/2") (("1" (skosimp*) (("1" (lemma "archimedean") (("1" (label "arch" -1) (("1" (inst "arch" "delta!1/2") (("1" (skosimp *) (("1" (inst "csl" "1/n!1" "n!1") (("1" (skosimp*) (("1" (typepred "n!2") (("1" (label "n!2T" -1) (("1" (lemma "fullset_metric_space1") (("1" (expand "metric_space?") (("1" (prop) (("1" (label "sz1" -1) (("1" (label "sym1" -2) (("1" (label "tri1" -3) (("1" (lemma "fullset_metric_space3") (("1" (expand "metric_space?") (("1" (prop) (("1" (label "sz3" -1) (("1" (label "sym3" -2) (("1" (label "tri3" -3) (("1" (expand "space_symmetric?") (("1" (expand "space_triangle?") (("1" (hide "sz1" "sz3") (("1" (lemma "fullset_metric_space2") (("1" (expand "metric_space?") (("1" (prop) (("1" (hide -2 -3) (("1" (label "sz2" -1) (("1" (expand "space_zero?") (("1" (copy "tri1") (("1" (hide "tri1") (("1" (inst-cp -1 "seq!1(n!2)`2" "seq!1(n!2)`1" "p!1") (("1" (label "tri1a" -1) (("1" (label "tri1inst" -2) (("1" (inst "epsq" "n!2") (("1" (copy "epsq") (("1" (hide "epsq") (("1" (prop) (("1" (label "mbs1" -1) (("1" (label "mbs2" -2) (("1" (label "mbs3" -3) (("1" (hide "mbs1" "mbs2" "mbs3") (("1" (label "s12lt" -1) (("1" (label "s3ylt" -2) (("1" (label "d3gt" -3) (("1" (copy "csl") (("1" (label "cls2" -1) (("1" (copy "sym1") (("1" (inst -1 "seq!1(n!2)`1" "seq!1(n!2)`2") (("1" (replace -1 "s12lt") (("1" (hide -1) (("1" (copy "cls2") (("1" (label "cls3" -1) (("1" (add-formulas "s12lt" "cls3") (("1" (label "tri_inst1" -1) (("1" (add-formulas "tri_inst1" "tri1inst") (("1" (label "tri_inst2" -1) (("1" (both-sides "-" "d1(seq!1(n!2)`1, p!1) + d1(seq!1(n!2)`2, seq!1(n!2)`1)" "tri_inst2") (("1" (assert) (("1" (copy "arch") (("1" (label "arch2" -1) (("1" (add-formulas "arch2" "arch2") (("1" (add-formulas -1 "tri_inst2") (("1" (assert) (("1" (lemma "both_sides_div_pos_lt2") (("1" (label "both_sides_div_pos_lt2" -1) (("1" (inst "both_sides_div_pos_lt2" "n!2" "n!1" "1") (("1" (prop) (("1" (hide -2) (("1" (add-formulas -1 -2) (("1" (both-sides "-" "2 * (1 / n!1) + 1 / n!2" -1) (("1" (assert) (("1" (label "d1sp1" -1) (("1" (copy "pcps") (("1" (hide "pcps") (("1" (label "pcps2" -1) (("1" (copy "pcps2") (("1" (label "pcps3" -1) (("1" (inst "pcps3" "seq!1(n!2)`2" "seq!1(n!2)`3") (("1" (prop) (("1" (inst "pcps2" "seq!1(n!2)`1" "y!1") (("1" (inst "sym1" "p!1" "seq!1(n!2)`1") (("1" (replace "sym1") (("1" (inst "sz2" "y!1" "y!1") (("1" (copy "arch") (("1" (label "arch3" -1) (("1" (add-formulas "cls2" "arch") (("1" (assert) (("1" (assert) (("1" (both-sides "-" "1/n!1" -1) (("1" (assert) (("1" (inst "tri3" "f!1(seq!1(n!2)`1,y!1)" "f!1(p!1,y!1)" "f!1(seq!1(n!2)`2, seq!1(n!2)`3)") (("1" (hide-all-but ("pcps3" "pcps2" "tri3" "sym3" "d3gt" "arch3")) (("1" (inst "sym3" "f!1(seq!1(n!2)`1, y!1)" "f!1(p!1, y!1)") (("1" (replace "sym3") (("1" (add-formulas "tri3" "pcps3") nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.36Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28