|
(borel_functions
(borel_function_def 0
(borel_function_def-1 nil 3358644189
("" (expand "borel_function?")
(("" (skosimp)
(("" (split)
(("1" (skosimp*)
(("1" (typepred "X!1")
(("1" (lemma "open_is_borel[T2,T]" ("X" "X!1"))
(("1" (inst - "X!1") nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2"
(name "C"
"{X:set[T2] | borel?[T1,S](inverse_image[T1, T2](f!1,X))}")
(("2"
(case "forall (X:set[T2]): open?[T2,T](X) => member(X,C)")
(("1" (case "subset?(borel?[T2,T],C)")
(("1" (expand "subset?")
(("1" (inst - "B!1")
(("1" (expand "member")
(("1" (expand "C") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2"
(lemma "generated_sigma_algebra_subset2"
("X" "fullset[open[T2,T]]" "Y" "C"))
(("2" (split -1)
(("1" (expand "borel?") (("1" (propax) nil nil))
nil)
("2" (hide 2)
(("2" (expand "fullset")
(("2" (expand "extend")
(("2" (expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (expand "sigma_algebra?")
(("3" (split)
(("1" (expand "subset_algebra_empty?")
(("1"
(expand "member")
(("1"
(expand "C")
(("1"
(inst -1 "emptyset[T2]")
(("1"
(split -1)
(("1" (propax) nil nil)
("2"
(typepred "T")
(("2"
(expand "topology?")
(("2"
(flatten)
(("2"
(expand
"topology_empty?")
(("2"
(expand "open?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subset_algebra_complement?")
(("2"
(skosimp)
(("2"
(typepred "x!1")
(("2"
(expand "C" -1)
(("2"
(expand "member")
(("2"
(expand "C")
(("2"
(lemma
"complement_is_borel[T1,S]"
("a"
"inverse_image[T1, T2](f!1, x!1)"))
(("1"
(case-replace
"complement(inverse_image[T1, T2](f!1, x!1)) = inverse_image[T1, T2](f!1, complement(x!1))")
(("1"
(hide-all-but 1)
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(expand "complement")
(("1"
(expand
"inverse_image")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "sigma_algebra_union?")
(("3"
(skosimp)
(("3"
(expand "member")
(("3"
(expand "C")
(("3"
(case-replace
"inverse_image[T1, T2](f!1, Union(X!1)) = Union(image[set[T2],set[T1]](inverse_image[T1, T2](f!1),X!1))")
(("1"
(hide -1)
(("1"
(typepred "borel?[T1,S]")
(("1"
(expand "sigma_algebra?")
(("1"
(flatten)
(("1"
(expand
"sigma_algebra_union?")
(("1"
(inst
-
"image[set[T2], set[T1]](inverse_image[T1, T2](f!1), X!1)")
(("1"
(split -3)
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil)
("2"
(hide-all-but
(-3 1))
(("2"
(lemma
"countable_image[set[T2],set[T1]]"
("S"
"X!1"
"f"
"inverse_image[T1, T2](f!1)"))
(("2"
(assert)
(("2"
(expand
"image"
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(typepred
"x!1")
(("3"
(expand
"image")
(("3"
(skosimp)
(("3"
(expand
"inverse_image"
-1)
(("3"
(inst
-5
"x!2")
(("3"
(expand
"member")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(expand "inverse_image")
(("2"
(expand "Union")
(("2"
(expand "member")
(("2"
(case-replace
"EXISTS (a: (X!1)): a(f!1(x!1))")
(("1"
(skosimp)
(("1"
(inst
+
"a!1 o f!1")
(("1"
(expand "o")
(("1"
(propax)
nil
nil))
nil)
("2"
(expand "o")
(("2"
(expand
"inverse_image")
(("2"
(expand
"image")
(("2"
(expand
"member")
(("2"
(inst
+
"a!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(typepred
"a!1")
(("2"
(expand
"inverse_image")
(("2"
(expand
"member")
(("2"
(expand
"image")
(("2"
(skosimp)
(("2"
(replace
-1)
(("2"
(assert)
(("2"
(inst
+
"x!2")
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)
("2" (hide 2 -1)
(("2" (skosimp)
(("2" (inst - "X!1")
(("2" (expand "member")
(("2" (expand "C") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(inverse_image const-decl "set[D]" function_image nil)
(image const-decl "set[R]" function_image nil)
(Union const-decl "set" sets nil)
(image const-decl "set[R]" function_image nil)
(countable_image formula-decl nil countable_image "sets_aux/")
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(f!1 skolem-const-decl "[T1 -> T2]" borel_functions nil)
(X!1 skolem-const-decl "setofsets[T2]" borel_functions nil)
(O const-decl "T3" function_props nil)
(a!1 skolem-const-decl "(X!1)" borel_functions nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(complement_is_borel formula-decl nil borel nil)
(complement const-decl "set" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(topology_empty? const-decl "bool" topology_prelim "topology/")
(emptyset const-decl "set" sets nil)
(emptyset_is_clopen name-judgement "clopen[T2, T]" borel_functions
nil)
(emptyset_is_compact name-judgement "compact[T2, T]"
borel_functions nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(fullset const-decl "set" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(generated_sigma_algebra_subset2 formula-decl nil
subset_algebra_def nil)
(C skolem-const-decl "[set[T2] -> bool]" borel_functions nil)
(subset? const-decl "bool" sets nil)
(X!1 skolem-const-decl "set[T2]" borel_functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T1 formal-type-decl nil borel_functions nil)
(S formal-const-decl "topology[T1]" borel_functions nil)
(inverse_image const-decl "set[D]" function_image nil)
(open_is_borel formula-decl nil borel nil)
(borel nonempty-type-eq-decl nil borel nil)
(borel? const-decl "sigma_algebra" borel nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T2 formal-type-decl nil borel_functions nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(topology? const-decl "bool" topology_prelim "topology/")
(topology nonempty-type-eq-decl nil topology_prelim "topology/")
(T formal-const-decl "topology[T2]" borel_functions nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(borel_function? const-decl "bool" borel_functions nil))
shostak))
(const_borel_function 0
(const_borel_function-1 nil 3384771865
("" (skosimp)
(("" (expand "borel_function?")
(("" (skosimp)
(("" (typepred "B!1")
(("" (expand "const_fun")
(("" (expand "inverse_image")
(("" (expand "member")
(("" (case "B!1(c!1)")
(("1" (lemma "fullset_is_borel[T1,S]")
(("1"
(case-replace "{x_1: T1 | B!1(c!1)}=fullset[T1]")
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "fullset")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2"
(case-replace "{x_1: T1 | B!1(c!1)}=emptyset[T1]")
(("1" (lemma "emptyset_is_borel[T1,S]")
(("1" (propax) nil nil)) nil)
("2" (apply-extensionality 1 :hide? t)
(("2" (expand "emptyset")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((borel_function? const-decl "bool" borel_functions nil)
(borel nonempty-type-eq-decl nil borel nil)
(borel? const-decl "sigma_algebra" borel nil)
(T formal-const-decl "topology[T2]" borel_functions nil)
(topology nonempty-type-eq-decl nil topology_prelim "topology/")
(topology? const-decl "bool" topology_prelim "topology/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil borel_functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inverse_image const-decl "set[D]" function_image nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(fullset_is_clopen name-judgement "clopen[T1, S]" borel_functions
nil)
(S formal-const-decl "topology[T1]" borel_functions nil)
(T1 formal-type-decl nil borel_functions nil)
(fullset_is_borel formula-decl nil borel nil)
(emptyset_is_borel formula-decl nil borel nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(emptyset_is_compact name-judgement "compact[T1, S]"
borel_functions nil)
(emptyset_is_clopen name-judgement "clopen[T1, S]" borel_functions
nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(const_fun const-decl "[S -> T]" const_fun_def "structures/"))
shostak))
(continuous_is_borel 0
(continuous_is_borel-1 nil 3384786870
("" (skolem + ("g"))
(("" (typepred "g")
(("" (rewrite "continuous_open_sets")
(("" (rewrite "borel_function_def")
(("" (skosimp)
(("" (inst - "X!1")
(("" (split)
(("1"
(lemma "open_is_borel[T1,S]"
("X" "inverse_image[T1,T2](g, X!1)"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil)
("2" (typepred "X!1") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous type-eq-decl nil continuity_def "topology/")
(continuous? const-decl "bool" continuity_def "topology/")
(T formal-const-decl "topology[T2]" borel_functions nil)
(S formal-const-decl "topology[T1]" borel_functions nil)
(topology nonempty-type-eq-decl nil topology_prelim "topology/")
(topology? const-decl "bool" topology_prelim "topology/")
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil borel_functions nil)
(T1 formal-type-decl nil borel_functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(borel_function_def formula-decl nil borel_functions nil)
(open nonempty-type-eq-decl nil topology "topology/")
(open? const-decl "bool" topology "topology/")
(set type-eq-decl nil sets nil)
(open_is_borel formula-decl nil borel nil)
(inverse_image const-decl "set[D]" function_image nil)
(continuous_open_sets formula-decl nil continuity "topology/"))
nil)))
¤ Dauer der Verarbeitung: 0.15 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.
|
