|
(subspace
(induced_subspace_topology 0
(induced_subspace_topology-1 nil 3301590214
("" (expand "induced_topology")
(("" (typepred "S")
(("" (expand "topology?")
(("" (flatten)
(("" (name "SS" "image(restrict[T1, T2, bool], S)")
(("" (replace -1)
(("" (split)
(("1" (hide-all-but (-2 1))
(("1" (expand "topology_empty?")
(("1" (assert)
(("1" (expand "SS")
(("1" (expand "image")
(("1" (inst + "emptyset[T1]")
(("1" (expand "restrict")
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(typepred "x!1")
(("1"
(expand "emptyset")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -3 1))
(("2" (expand "topology_full?")
(("2" (expand "member")
(("2" (replace -1 1 rl)
(("2" (expand "image")
(("2" (expand "restrict")
(("2" (inst + "fullset[T1]")
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(expand "fullset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "topology_Union?")
(("3" (skosimp)
(("3"
(case "EXISTS (V:setofsets[T1]): subset?(V,S) & image(restrict[T1,T2,bool],V) = U!1")
(("1" (skosimp)
(("1" (inst - "V!1")
(("1" (assert)
(("1" (expand "restrict")
(("1"
(expand "image")
(("1"
(replace -4 1 rl)
(("1"
(assert)
(("1"
(inst + "Union(V!1)")
(("1"
(expand "Union")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(case-replace
"EXISTS (a: (V!1)): a(x!1)")
(("1"
(skosimp)
(("1"
(typepred "a!1")
(("1"
(expand "subset?")
(("1"
(inst - "a!1")
(("1"
(expand "member")
(("1"
(inst + "a!1")
(("1"
(expand
"restrict")
(("1"
(propax)
nil
nil))
nil)
("2"
(replace
-4
1
rl)
(("2"
(assert)
(("2"
(expand
"restrict")
(("2"
(inst
+
"a!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(replace
-4
-1
rl)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(replace
-1)
(("2"
(assert)
(("2"
(typepred
"x!2")
(("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)
("2" (hide 2)
(("2"
(inst +
"{A:(S) | EXISTS (B:(U!1)): B = restrict[T1,T2,bool](A)}")
(("2" (split)
(("1" (expand "subset?")
(("1"
(expand "extend")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t)
(("2"
(expand "extend")
(("2"
(expand "restrict")
(("2"
(expand "image")
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2"
(expand "member")
(("2"
(case-replace "U!1(x!1)")
(("1"
(replace -3 -2 rl)
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "x!2")
(("1"
(replace -2 1 rl)
(("1"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide-all-but (-1 -5 1))
(("4" (expand "topology_intersection?")
(("4" (skosimp)
(("4" (typepred "A!1")
(("4" (typepred "B!1")
(("4" (replace -3 * rl)
(("4" (hide -3)
(("4"
(expand "restrict")
(("4"
(expand "image")
(("4"
(skosimp*)
(("4"
(replace -1)
(("4"
(replace -2)
(("4"
(assert)
(("4"
(typepred "x!1")
(("4"
(typepred "x!2")
(("4"
(inst - "x!2" "x!1")
(("4"
(inst
+
"intersection(x!2, x!1)")
(("4"
(apply-extensionality
1
:hide?
t)
(("4"
(expand
"intersection")
(("4"
(expand
"member")
(("4"
(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)
((S formal-const-decl "topology" subspace 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)
(T1 formal-type-decl nil subspace nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(intersection const-decl "set" sets nil)
(x!2 skolem-const-decl "(S)" subspace nil)
(x!1 skolem-const-decl "(S)" subspace nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(Union const-decl "set" sets nil)
(a!1 skolem-const-decl "(V!1)" subspace nil)
(V!1 skolem-const-decl "setofsets[T1]" subspace nil)
(U!1 skolem-const-decl "setofsets[T2]" subspace nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(x!2 skolem-const-decl "(S)" subspace nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(fullset const-decl "set" sets nil)
(topology_full? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(SS skolem-const-decl "set[[T2 -> bool]]" subspace nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(T2_pred const-decl "[T1 -> boolean]" subspace nil)
(T2 formal-subtype-decl nil subspace nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(image const-decl "set[R]" function_image nil)
(restrict const-decl "R" restrict nil)
(induced_topology const-decl "setofsets[T2]" subspace nil))
shostak))
(subspace_is_topology 0
(subspace_is_topology-1 nil 3346049587
("" (lemma "induced_subspace_topology") (("" (propax) nil nil)) nil)
((induced_subspace_topology formula-decl nil subspace nil)) nil)))
¤ Dauer der Verarbeitung: 0.35 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.
|
