|
(heine_borel
(real_heine_borel 0
(real_heine_borel-1 nil 3397538876
("" (skosimp)
(("" (expand "compact?")
(("" (expand "compact_subset?")
(("" (skosimp)
((""
(lemma "heine_borel_aux" ("a" "a!1" "b" "b!1" "C" "U!1"))
(("" (replace -2)
(("" (replace -3)
(("" (expand "open_cover?" -3)
(("" (flatten)
(("" (split -1)
(("1" (skosimp)
(("1" (inst + "U!2")
(("1" (assert)
(("1" (expand "finite_cover?")
(("1"
(hide -1 -2 -5 -6)
(("1"
(expand "cover?")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -3)
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2"
(expand "member")
(("2"
(expand
"metric_induced_topology")
(("2"
(expand "open?")
(("2"
(expand "member")
(("2"
(expand
"metric_induced_topology")
(("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)
((compact? const-decl "bool" topology "topology/")
(open_cover? const-decl "bool" topology_prelim "topology/")
(finite_cover? const-decl "bool" topology_prelim "topology/")
(cover? const-decl "bool" topology_prelim "topology/")
(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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(metric_induced_topology_is_second_countable name-judgement
"second_countable" real_topology nil)
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_topology nil)
(metric_space_is_hausdorff name-judgement "hausdorff" real_topology
nil)
(every const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(heine_borel_aux formula-decl nil heine_borel_scaf nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(compact_subset? const-decl "bool" topology_prelim "topology/"))
shostak)))
¤ Dauer der Verarbeitung: 0.1 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.
|
