(subspacenil 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" "1" "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" "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" "Union(V!1)" )"1" expand "Union" )"1" "1" "EXISTS (a: (V!1)): a(x!1)" )"1" "1" "a!1" )"1" expand "subset?" )"1" "a!1" )"1" expand "member" )"1" "a!1" )"1" expand "restrict" )"1" nil nil ))nil )"2" replace "2" assert )"2" expand "restrict" )"2" "a!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "a!1" )"2" replace "2" assert )"2" "2" replace "2" assert )"2" "x!2" )"2" "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" "{A:(S) | EXISTS (B:(U!1)): B = restrict[T1,T2,bool](A)}" )"2" (split)"1" (expand "subset?" )"1" expand "extend" )"1" expand "member" )"1" "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" "x!1" )"2" expand "member" )"2" "U!1(x!1)" )"1" replace -3 -2 rl)"1" assert )"1" "1" "x!2" )"1" replace -2 1 rl)"1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "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" "4" replace -1)"4" replace -2)"4" assert )"4" "x!1" )"4" "x!2" )"4" "x!2" "x!1" )"4" "intersection(x!2, x!1)" )"4" "4" expand "intersection" )"4" expand "member" )"4" 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 )"topology" subspace nil )nil topology_prelim nil )"bool" topology_prelim nil )nil sets nil )nil defined_types nil )nil subspace nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"(S)" subspace nil )"(S)" subspace nil )"bool" topology_prelim nil )"bool" topology_prelim nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"set" sets nil )"(V!1)" subspace nil )"setofsets[T1]" subspace nil )"setofsets[T2]" subspace nil )"(partial_order?[set[T]])" nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"R" extend nil )"bool" booleans nil )"[bool, bool -> bool]" booleans nil )"(S)" subspace nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"set" sets nil )"bool" topology_prelim nil )"finite_set" finite_sets nil )"bool" sets nil )"set" sets nil )"set[[T2 -> bool]]" subspace nil )"bool" topology_prelim nil )"[T1 -> boolean]" subspace nil )nil subspace nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"set[R]" function_image nil )"R" restrict nil )"setofsets[T2]" subspace nil ))nil 3346049587"" (lemma "induced_subspace_topology" ) (("" (propax) nil nil )) nil )nil subspace nil )) nil )))quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
