|
(continuity
(continuous_open_sets 0
(continuous_open_sets-1 nil 3300514488
("" (expand "continuous?")
(("" (expand "continuous_at?")
(("" (skosimp*)
(("" (split)
(("1" (skosimp*)
(("1" (lemma "image_inverse_image" ("f" "f!1" "Y" "Y!1"))
(("1" (rewrite "open_def[T1,S]" 1)
(("1" (skosimp)
(("1" (typepred "x!1")
(("1" (inst - "x!1")
(("1" (inst - "Y!1")
(("1" (split)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "neighbourhood?")
(("2"
(expand "interior_point?")
(("2"
(expand "inverse_image")
(("2"
(inst + "Y!1")
(("2"
(assert)
(("2"
(expand "subset?")
(("2" (skosimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "topology1") (("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "neighbourhood?")
(("2" (expand "interior_point?")
(("2" (skosimp*)
(("2" (typepred "U!2")
(("2" (inst - "U!2")
(("2" (assert)
(("2" (inst + "inverse_image(f!1, U!2)")
(("2"
(lemma "inverse_image_subset"
("Y1" "U!2" "Y2" "U!1" "f" "f!1"))
(("2" (assert)
(("2" (expand "inverse_image")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_at? const-decl "bool" continuity_def nil)
(T2 formal-type-decl nil continuity nil)
(T1 formal-type-decl nil continuity nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(image_inverse_image formula-decl nil function_image nil)
(neighbourhood? const-decl "bool" topology nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(Y!1 skolem-const-decl "set[T2]" continuity nil)
(open? const-decl "bool" topology nil)
(T formal-const-decl "topology[T2]" continuity nil)
(interior_point? const-decl "bool" topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(S formal-const-decl "topology[T1]" continuity nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(topology? const-decl "bool" topology_prelim nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(inverse_image const-decl "set[D]" function_image nil)
(open_def formula-decl nil topology nil)
(inverse_image_subset formula-decl nil function_image nil)
(continuous? const-decl "bool" continuity_def nil))
shostak))
(continuous_closed_sets 0
(continuous_closed_sets-1 nil 3300515647
("" (skosimp)
(("" (rewrite "continuous_open_sets")
(("" (split)
(("1" (skosimp*)
(("1" (expand "closed?")
(("1" (expand "member")
(("1" (inst - "complement(Y!1)")
(("1" (assert)
(("1" (expand "open?")
(("1" (expand "member")
(("1" (rewrite "inverse_image_complement") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "closed?")
(("2" (expand "open?")
(("2" (expand "member")
(("2" (inst - "complement(Y!1)")
(("2" (rewrite "complement_complement")
(("2" (assert)
(("2" (rewrite "inverse_image_complement")
(("2" (rewrite "complement_complement") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_open_sets formula-decl nil continuity nil)
(T1 formal-type-decl nil continuity nil)
(T2 formal-type-decl nil continuity nil)
(inverse_image const-decl "set[D]" function_image nil)
(complement_complement formula-decl nil sets_lemmas nil)
(member const-decl "bool" sets nil)
(inverse_image_complement formula-decl nil function_image nil)
(open? const-decl "bool" topology nil)
(complement const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(closed? const-decl "bool" topology nil))
shostak))
(continuous_basis 0
(continuous_basis-1 nil 3364124090
("" (skosimp)
(("" (rewrite "continuous_open_sets")
(("" (split)
(("1" (skosimp*)
(("1" (typepred "Y!1")
(("1" (typepred "B!1")
(("1" (expand "base?")
(("1" (flatten)
(("1" (inst -4 "Y!1")
(("1" (split -4)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "subset?")
(("2" (expand "open?")
(("2" (expand "member")
(("2"
(inst - "Y!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "B!1")
(("2" (expand "base?")
(("2" (flatten)
(("2" (expand "open?" -4)
(("2" (expand "member")
(("2" (inst - "Y!1")
(("2" (skosimp)
(("2" (replace -3 * rl)
(("2"
(case-replace
"inverse_image(f!1, Union(V!1)) =
Union({X | EXISTS Y: V!1(Y) & X=inverse_image(f!1, Y)})")
(("1" (hide -1)
(("1"
(lemma
"open_Union"
("Y"
"{X | EXISTS Y: V!1(Y) & X = inverse_image(f!1, Y)}"))
(("1"
(split -1)
(("1" (propax) nil nil)
("2"
(hide 2)
(("2"
(expand "every")
(("2"
(skosimp)
(("2"
(typepred "x!1")
(("2"
(skosimp)
(("2"
(replace -2)
(("2"
(hide -2)
(("2"
(inst - "Y!2")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(inst -3 "Y!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(expand "Union")
(("2"
(expand "inverse_image")
(("2"
(expand "member")
(("2"
(case-replace
"EXISTS (a: (V!1)): a(f!1(x!1))")
(("1"
(skosimp)
(("1"
(typepred "a!1")
(("1"
(inst
+
"inverse_image(f!1, a!1)")
(("1"
(expand
"inverse_image")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(inst + "a!1")
nil
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(skosimp)
(("2"
(inst + "Y!2")
(("2"
(replace -2 -3)
(("2"
(expand
"inverse_image")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_open_sets formula-decl nil continuity nil)
(T1 formal-type-decl nil continuity nil)
(T2 formal-type-decl nil continuity nil)
(Y!1 skolem-const-decl "set[T2]" continuity nil)
(Y!2 skolem-const-decl "set[T2]" continuity nil)
(V!1 skolem-const-decl "setofsets[T2]" continuity nil)
(f!1 skolem-const-decl "[T1 -> T2]" continuity nil)
(a!1 skolem-const-decl "(V!1)" continuity nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(every const-decl "bool" sets nil)
(B!1 skolem-const-decl "(base?[T2](T))" continuity nil)
(Y!2 skolem-const-decl "set[T2]" continuity nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(S formal-const-decl "topology[T1]" continuity nil)
(open_Union formula-decl nil topology nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inverse_image const-decl "set[D]" function_image nil)
(Union const-decl "set" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(topology? const-decl "bool" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(base? const-decl "bool" basis nil)
(T formal-const-decl "topology[T2]" continuity nil))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
