(denumerable_enumerationnil 3322365875"" (skosimp)"" (typepred "X!1" )"" (expand "is_countably_infinite" )"" (skosimp)"" (typepred "f!1" )"" (lemma "bijective_inverse_exists" ("f" "f!1" ))"" (expand "exists1" )"" (flatten)"" (skolem - "g" )"" "bij_inv_is_bij_alt" ("f" "f!1" "g" "g" ))"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst - "g" )"1" (expand "member" )"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil denumerable_enumeration nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil function_inverse_defnil )nil function_inverse_def nil )"bool" function_inverse_def nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" exists1 nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil ))nil 3322366032"" (skosimp)"" (expand "denumerable_enumeration" ) (("" (propax) nil nil ))nil ))nil )"[nat -> (X)]" nil ))nil 3322366048"" (skosimp)"" (expand "restrict" )"" (expand "fullset" )"" (expand "image" )"" (apply-extensionality :hide? t)"" (lemma "denumerable_enumeration_bij" ("X" "X!1" ))"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst - "x!1" )"" (skosimp)"" (inst + "x!2" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" restrict nil )"set[R]" function_image nil )nil nil )"bool" functions nil )"bool" functions nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )"[nat -> (X)]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil denumerable_enumeration nil )"set" sets nil ))quality 100%
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
