|
(metric_continuity
(metric_continuous_at_def 0
(metric_continuous_at_def-1 nil 3359022978
("" (skosimp)
(("" (expand "metric_continuous_at?")
(("" (expand "continuous_at?")
(("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (split)
(("1" (skosimp*)
(("1" (expand "member")
(("1" (inst - "ball(f!1(x0!1), epsilon!1)")
(("1" (split -1)
(("1" (skosimp)
(("1" (typepred "U!1")
(("1" (lemma "metric_open_def" ("S" "U!1"))
(("1" (assert)
(("1"
(expand "metric_open?")
(("1"
(inst - "x0!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "r!1")
(("1"
(skosimp)
(("1"
(expand "subset?")
(("1"
(inst - "x!1")
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(expand
"inverse_image")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(lemma "metric_open_ball"
("x" "f!1(x0!1)" "r" "epsilon!1"))
(("2" (rewrite "metric_open_def")
(("2" (inst + "ball(f!1(x0!1), epsilon!1)")
(("2"
(lemma
"ball_centre"
("x" "f!1(x0!1)" "r" "epsilon!1"))
(("2"
(assert)
(("2"
(rewrite "subset_reflexive")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "U!2")
(("2" (lemma "metric_open_def[T2,d2]" ("S" "U!2"))
(("2" (assert)
(("2" (expand "metric_open?")
(("2" (inst - "f!1(x0!1)")
(("2" (assert)
(("2" (skosimp)
(("2"
(inst - "r!1")
(("2"
(skosimp)
(("2"
(inst + "ball(x0!1, delta!1)")
(("1"
(lemma
"ball_centre"
("x" "x0!1" "r" "delta!1"))
(("1"
(assert)
(("1"
(expand "subset?")
(("1"
(skosimp)
(("1"
(assert)
(("1"
(inst -4 "x!1")
(("1"
(assert)
(("1"
(expand
"inverse_image")
(("1"
(expand "member")
(("1"
(inst
-2
"f!1(x!1)")
(("1"
(inst
-
"f!1(x!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"metric_open_def"
1
:dir
rl)
(("2"
(rewrite "metric_open_ball")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_continuous_at? const-decl "bool" metric_continuity nil)
(neighbourhood? const-decl "bool" topology "topology/")
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(d1 formal-const-decl "metric[T1]" metric_continuity nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(ball_is_metric_open application-judgement "metric_open"
metric_continuity nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(ball_is_metric_open application-judgement "metric_open"
metric_continuity nil)
(inverse_image const-decl "set[D]" function_image nil)
(subset? const-decl "bool" sets nil)
(metric_open? const-decl "bool" metric_space_def nil)
(metric_open_def formula-decl nil metric_space nil)
(metric_open_ball formula-decl nil metric_space nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(ball_centre formula-decl nil metric_space nil)
(T1 formal-type-decl nil metric_continuity nil)
(ball const-decl "set[T]" metric_space_def nil)
(d2 formal-const-decl "metric[T2]" metric_continuity nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil metric_continuity nil)
(interior_point? const-decl "bool" topology "topology/")
(continuous_at? const-decl "bool" continuity_def "topology/"))
shostak))
(metric_continuous_def 0
(metric_continuous_def-1 nil 3324700803
("" (skosimp)
(("" (expand "continuous?")
(("" (expand "metric_continuous?")
(("" (split)
(("1" (skosimp*)
(("1" (inst - "x!1")
(("1"
(lemma "metric_continuous_at_def"
("f" "f!1" "x0" "x!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "x!1")
(("2"
(lemma "metric_continuous_at_def"
("f" "f!1" "x0" "x!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuity_def "topology/")
(T1 formal-type-decl nil metric_continuity nil)
(metric_continuous_at_def formula-decl nil metric_continuity nil)
(T2 formal-type-decl nil metric_continuity nil)
(metric_continuous? const-decl "bool" metric_continuity nil))
shostak))
(metric_continuity_limit 0
(metric_continuity_limit-1 nil 3359166753
("" (skosimp)
(("" (expand "convergence?")
(("" (skosimp*)
(("" (rewrite "metric_continuous_at_def" -2 :dir rl)
(("" (expand "continuous_at?")
(("" (inst -2 "U!1")
(("" (split -2)
(("1" (expand "neighbourhood?")
(("1" (expand "interior_point?")
(("1" (skosimp)
(("1" (typepred "U!2")
(("1" (inst -4 "U!2")
(("1" (assert)
(("1" (skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst -4 "i!1")
(("1"
(assert)
(("1"
(expand "o")
(("1"
(expand "subset?")
(("1"
(inst - "u!1(i!1)")
(("1"
(expand "member")
(("1"
(expand
"inverse_image")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "neighbourhood?")
(("2" (expand "interior_point?")
(("2" (typepred "U!1")
(("2" (inst + "U!1")
(("2" (expand "member")
(("2" (rewrite "subset_reflexive") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergence? const-decl "bool" topological_convergence
"topology/")
(metric_continuous_at_def formula-decl nil metric_continuity nil)
(T1 formal-type-decl nil metric_continuity nil)
(T2 formal-type-decl nil metric_continuity nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d2 formal-const-decl "metric[T2]" metric_continuity nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(subset_reflexive formula-decl nil sets_lemmas nil)
(neighbourhood? const-decl "bool" topology "topology/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(subset? const-decl "bool" sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(sequence type-eq-decl nil sequences nil)
(O const-decl "T3" function_props nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(d1 formal-const-decl "metric[T1]" metric_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(interior_point? const-decl "bool" topology "topology/")
(continuous_at? const-decl "bool" continuity_def "topology/"))
shostak))
(metric_continuous_is_continuous 0
(metric_continuous_is_continuous-1 nil 3383401763
("" (skosimp)
(("" (typepred "x!1")
(("" (rewrite "metric_continuous_def") nil nil)) nil))
nil)
((metric_continuous type-eq-decl nil metric_continuity nil)
(metric_continuous? const-decl "bool" metric_continuity nil)
(T2 formal-type-decl nil metric_continuity nil)
(T1 formal-type-decl nil metric_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_continuous_def formula-decl nil metric_continuity nil))
nil))
(continuous_is_metric_continuous 0
(continuous_is_metric_continuous-1 nil 3383401763
("" (skosimp)
(("" (typepred "x!1")
(("" (rewrite "metric_continuous_def") nil nil)) nil))
nil)
((continuous type-eq-decl nil continuity_def "topology/")
(continuous? const-decl "bool" continuity_def "topology/")
(d2 formal-const-decl "metric[T2]" metric_continuity nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(d1 formal-const-decl "metric[T1]" metric_continuity nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil metric_continuity nil)
(T1 formal-type-decl nil metric_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_continuous_def formula-decl nil metric_continuity nil))
nil))
(uniform_continuous 0
(uniform_continuous-1 nil 3337412454
("" (skosimp)
(("" (rewrite "metric_continuous_def")
(("" (expand "metric_continuous?")
(("" (expand "uniform_continuous?")
(("" (expand "metric_continuous_at?")
(("" (expand "ball")
(("" (expand "member")
(("" (skosimp*)
(("" (inst - "epsilon!1")
(("" (skosimp)
(("" (inst + "delta!1")
(("" (skosimp)
(("" (inst - "x!2" "x!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_continuous_def formula-decl nil metric_continuity nil)
(T1 formal-type-decl nil metric_continuity nil)
(T2 formal-type-decl nil metric_continuity nil)
(uniform_continuous? const-decl "bool" metric_continuity nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(member const-decl "bool" sets nil)
(metric_continuous_at? const-decl "bool" metric_continuity nil)
(metric_continuous? const-decl "bool" metric_continuity nil))
shostak))
(uniform_continuous_is_continuous 0
(uniform_continuous_is_continuous-1 nil 3383401763
("" (skosimp)
(("" (typepred "x!1")
(("" (lemma "uniform_continuous" ("f" "x!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((uniform_continuous type-eq-decl nil metric_continuity nil)
(uniform_continuous? const-decl "bool" metric_continuity nil)
(T2 formal-type-decl nil metric_continuity nil)
(T1 formal-type-decl nil metric_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(uniform_continuous formula-decl nil metric_continuity nil))
nil))
(compact_uniform_continuous 0
(compact_uniform_continuous-1 nil 3359167367
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "uniform_continuous?")
(("1" (skosimp*)
(("1" (rewrite "metric_continuous_def")
(("1"
(name "DELTA"
"LAMBDA x: {delta| forall (y:T1): d1(x,y)<2*delta => d2(f!1(x),f!1(y)))
(("1" (case "forall x: nonempty?[posreal](DELTA(x))")
(("1"
(name "Delta"
"LAMBDA x: choose[posreal](DELTA(x))")
(("1" (hide -3)
(("1" (case "forall x: Delta(x)>0")
(("1" (expand "compact_subset?")
(("1"
(inst -5
"image((LAMBDA x: ball(x,Delta(x))),fullset[T1])")
(("1" (split -5)
(("1"
(skosimp)
(("1"
(expand "finite_cover?")
(("1"
(flatten)
(("1"
(name "N" "card(V!1)")
(("1"
(name
"Centres"
"{x| V!1(ball(x,Delta(x)))}")
(("1"
(name
"F"
"lambda x: ball(x,Delta(x))")
(("1"
(replace -1)
(("1"
(case "nonempty?(V!1)")
(("1"
(lemma
"nonempty_card[set[T1]]"
("S" "V!1"))
(("1"
(assert)
(("1"
(replace -5)
(("1"
(case
"surjective?[(Centres),(V!1)](F)")
(("1"
(lemma
"surjective_inverse_exists[(Centres),(V!1)]"
("f" "F"))
(("1"
(skosimp)
(("1"
(expand
"restrict")
(("1"
(expand
"inverse?")
(("1"
(case
"injective?[(V!1),(Centres)](g!1)")
(("1"
(name
"X"
"image(g!1, fullset[(V!1)])")
(("1"
(case
"bijective?[(V!1),(X)](g!1)")
(("1"
(case
"is_finite(X)")
(("1"
(case
"card(X) = N")
(("1"
(lemma
"comp_inverse_right_alt[(V!1), (X)]"
("f"
"g!1"
"g"
"F"))
(("1"
(expand
"restrict")
(("1"
(name
"SS"
"image[(X),posreal](Delta,X)")
(("1"
(lemma
"finite_image[(X),posreal]"
("f"
"Delta"
"S"
"X"))
(("1"
(replace
-2)
(("1"
(hide
-2)
(("1"
(case
"nonempty?(SS)")
(("1"
(lemma
"min_lem"
("SS"
"SS"
"a"
"min(SS)"))
(("1"
(assert)
(("1"
(case
"forall x: exists (y:(X)): F(y)(x)")
(("1"
(inst
+
"min(SS)")
(("1"
(skosimp)
(("1"
(expand
"F"
-1)
(("1"
(expand
"ball"
(-1
-25
1))
(("1"
(inst
-
"x0!1")
(("1"
(skosimp)
(("1"
(typepred
"y!1")
(("1"
(inst
-
"Delta(y!1)")
(("1"
(lemma
"metric_triangle"
("x"
"y!1"
"y"
"x0!1"
"z"
"x!1"))
(("1"
(case
"d1(y!1, x!1) < 2*Delta(y!1)")
(("1"
(hide
-2)
(("1"
(inst
-26
"y!1")
(("1"
(lemma
"choose_member[posreal]"
("a"
"DELTA(y!1)"))
(("1"
(split
-1)
(("1"
(expand
"member")
(("1"
(expand
"DELTA"
-1
1)
(("1"
(inst
-
"x!1")
(("1"
(split
-1)
(("1"
(lemma
"choose_member[posreal]"
("a"
"DELTA(y!1)"))
(("1"
(split
-1)
(("1"
(expand
"member")
(("1"
(expand
"DELTA"
-1
1)
(("1"
(inst
-
"x0!1")
(("1"
(split
-1)
(("1"
(lemma
"metric_triangle"
("x"
"f!1(x0!1)"
"y"
"f!1(y!1)"
"z"
"f!1(x!1)"))
(("1"
(rewrite
"metric_symmetric"
-2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"Delta"
-5)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"Delta")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"SS")
(("2"
(expand
"restrict")
(("2"
(expand
"image")
(("2"
(inst
+
"y!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil)
("2"
(hide
-23
2)
(("2"
(skosimp)
(("2"
(expand
"cover?")
(("2"
(expand
"Union")
(("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(inst
-19
"x!1")
(("2"
(split
-19)
(("1"
(skosimp)
(("1"
(typepred
"a!1")
(("1"
(inst
-19
"a!1")
(("1"
(assert)
(("1"
(expand
"fullset")
(("1"
(expand
"image")
(("1"
(skosimp)
(("1"
(typepred
"g!1(a!1)")
(("1"
(inst
-13
"a!1")
(("1"
(split
-13)
(("1"
(inst
+
"g!1(a!1)")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(expand
"X")
(("2"
(expand
"fullset")
(("2"
(expand
"image")
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.98 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
