|
(real_fun_on_compact_sets
(IMP_continuity_ms_def_TCC1 0
(IMP_continuity_ms_def_TCC1-1 nil 3460717941
("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil)
((fullset_metric_space formula-decl nil real_fun_on_compact_sets
nil))
nil))
(IMP_continuity_ms_def_TCC2 0
(IMP_continuity_ms_def_TCC2-1 nil 3460717941
("" (lemma "real_metric_space")
(("" (inst - "fullset[real]") nil nil)) 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)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(real_metric_space formula-decl nil real_metric_space nil))
nil))
(cont_on_compact_max 0
(cont_on_compact_max-1 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"
(label "bbel" -2)
(("1"
(hide "bbel")
(("1"
(lemma "real_complete")
(("1"
(label "lub" -1)
(("1"
(inst "lub" "image(f!1,S!1)")
(("1"
(expand "bounded_above?")
(("1"
(skosimp*)
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(expand
"least_upper_bound?")
(("1"
(prop)
(("1"
(label "lub2" -2)
(("1"
(name
"seq"
"(LAMBDA (n: nat): choose({s: T | S!1(s) AND y!1-f!1(s) < 1/(n+1)}))")
(("1"
(label
"seq_def"
-1)
(("1"
(inst
"csl"
"seq")
(("1"
(skosimp*)
(("1"
(inst-cp
"maxexists"
"p!1")
(("1"
(label
"maxexists2"
2)
(("1"
(copy
"lub")
(("1"
(label
"lub3"
-1)
(("1"
(expand
"upper_bound?"
"lub")
(("1"
(skosimp*)
(("1"
(inst
"lub"
"f!1(t!1)")
(("1"
(case
"y!1 = f!1(t!1)")
(("1"
(replace
-1)
(("1"
(expand
"upper_bound?"
"lub3")
(("1"
(inst
"maxexists2"
"t!1")
(("1"
(skosimp*)
(("1"
(inst
"lub3"
"f!1(t!2)")
(("1"
(expand
"image")
(("1"
(inst
+
"t!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name
"A"
"y!1 - f!1(t!1)")
(("2"
(expand
"continuous?")
(("2"
(inst
"cont"
"p!1")
(("2"
(expand
"continuous_at?")
(("2"
(expand
"member")
(("2"
(expand
"ball")
(("2"
(inst
"cont"
"A/2")
(("1"
(skosimp*)
(("1"
(lemma
"archimedean")
(("1"
(inst
-
"A/4")
(("1"
(skosimp*)
(("1"
(lemma
"both_sides_div_pos_lt2")
(("1"
(inst
-
"n!1+1"
"n!1"
"1")
(("1"
(assert)
(("1"
(add-formulas
-1
-2)
(("1"
(both-sides
"-"
"1/n!1"
-1)
(("1"
(assert)
(("1"
(inst
"csl"
"delta!1/2"
"n!1")
(("1"
(skosimp*)
(("1"
(typepred
"n!2")
(("1"
(both-sides
"+"
"1"
-1)
(("1"
(label
"n1n2"
-1)
(("1"
(label
"arch1"
-2)
(("1"
(label
"Adef"
-3)
(("1"
(inst
"cont"
"seq(n!2)")
(("1"
(prop)
(("1"
(grind
"cont")
(("1"
(hide
"compact")
(("1"
(typepred
"seq(n!2)")
(("1"
(label
"ge2"
-2)
(("1"
(lemma
"both_sides_div_pos_ge2")
(("1"
(label
"recip"
-1)
(("1"
(inst
"recip"
"n!1 + 1"
"n!2 + 1"
"1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
"compact")
(("2"
(typepred
"seq(n!2)")
(("2"
(label
"n!2le"
-2)
(("2"
(label
"seqn!2tp"
-1)
(("2"
(lemma
"both_sides_div_pos_ge2")
(("2"
(label
"bsxyz"
-1)
(("2"
(inst
"bsxyz"
"n!1 + 1"
"n!2+1"
"1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide
"compact")
(("3"
(typepred
"seq(n!2)")
(("3"
(label
"n!2le"
-2)
(("3"
(label
"seqn!2tp"
-1)
(("3"
(lemma
"both_sides_div_pos_ge2")
(("3"
(label
"bsxyz"
-1)
(("3"
(inst
"bsxyz"
"n!1 + 1"
"n!2 + 1"
"1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(hide
"compact")
(("4"
(typepred
"seq(n!2)")
(("4"
(label
"n!2le"
-2)
(("4"
(label
"seqn!2tp"
-1)
(("4"
(lemma
"both_sides_div_pos_ge2")
(("4"
(label
"bsxyz"
-1)
(("4"
(inst
"bsxyz"
"n!1 + 1"
"n!2 + 1"
"1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"fullset_metric_space")
(("2"
(expand
"metric_space?")
(("2"
(expand
"space_symmetric?")
(("2"
(prop)
(("2"
(inst
-2
"p!1"
"seq(n!2)")
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil)
("3"
(expand
"fullset")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(iff)
(("2"
(prop)
(("1"
(cancel-by
1
"n!1*n!1")
(("1"
(grind-reals)
nil
nil))
nil)
("2"
(cancel-by
1
"n!1*n!1")
(("2"
(grind-reals)
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"
(inst
+
"t!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"nonempty?")
(("2"
(expand
"empty?")
(("2"
(expand
"member")
(("2"
(inst
"lub2"
"y!1-1/(1+n!1)")
(("2"
(prop)
(("1"
(assert)
nil
nil)
("2"
(expand
"upper_bound?"
+)
(("2"
(expand
"image")
(("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(expand
"image")
(("2"
(skosimp*)
(("2"
(inst
-
"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"
(name
"seq"
"(LAMBDA (n: nat): choose({s: T | S!1(s) AND f!1(s) > n}))")
(("1"
(inst "csl" "seq")
(("1"
(skosimp*)
(("1"
(lemma
"axiom_of_archimedes")
(("1"
(inst
-
"f!1(p!1)")
(("1"
(skosimp*)
(("1"
(expand
"continuous?")
(("1"
(inst
"cont"
"p!1")
(("1"
(expand
"continuous_at?")
(("1"
(inst
"cont"
"1")
(("1"
(skosimp*)
(("1"
(inst
"csl"
"delta!1"
"max(i!1,0) + 2")
(("1"
(skosimp*)
(("1"
(typepred
"n!1")
(("1"
(inst
"cont"
"seq(n!1)")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.31 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.
|
