|
(metric_space
(metric_zero 0
(metric_zero-1 nil 3359138177
("" (skosimp)
(("" (typepred "d")
(("" (expand "metric?")
(("" (expand "metric_zero?")
(("" (flatten) (("" (inst - "x!1" "y!1") nil nil)) nil))
nil))
nil))
nil))
nil)
((d formal-const-decl "metric" metric_space nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil metric_space nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_zero? const-decl "bool" metric_def nil))
shostak))
(metric_symmetric 0
(metric_symmetric-1 nil 3359138210
("" (typepred "d")
(("" (expand "metric?")
(("" (expand "metric_symmetric?") (("" (flatten) nil nil)) nil))
nil))
nil)
((metric_symmetric? const-decl "bool" metric_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil metric_space nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil))
shostak))
(metric_triangle 0
(metric_triangle-1 nil 3359138244
("" (typepred "d")
(("" (expand "metric?")
(("" (expand "metric_triangle?") (("" (flatten) nil nil)) nil))
nil))
nil)
((metric_triangle? const-decl "bool" metric_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil metric_space nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil))
shostak))
(metric_is_0 0
(metric_is_0-1 nil 3359138288
("" (skosimp) (("" (rewrite "metric_zero") nil nil)) nil)
((metric_zero formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil))
shostak))
(ball_centre 0
(ball_centre-1 nil 3359138314
("" (skosimp)
(("" (expand "member")
(("" (expand "ball")
(("" (rewrite "metric_is_0") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(metric_is_0 formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball const-decl "set[T]" metric_space_def nil))
shostak))
(metric_open_ball 0
(metric_open_ball-1 nil 3359138339
("" (skosimp)
(("" (expand "metric_open?")
(("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (case-replace "x!2=x!1")
(("1" (inst + "r!1")
(("1" (rewrite "subset_reflexive") nil nil)) nil)
("2" (case "r!1 - d(x!1, x!2) > 0")
(("1" (inst + "r!1-d(x!1,x!2)")
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (skosimp)
(("1" (expand "ball")
(("1"
(lemma "metric_triangle"
("x" "x!1" "y" "x!2" "z" "x!3"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (hide 3)
(("2" (expand "ball") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "subset?")
(("2" (inst - "x!2")
(("2" (rewrite "ball_centre")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_open? const-decl "bool" metric_space_def nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(ball const-decl "set[T]" metric_space_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(r!1 skolem-const-decl "posreal" metric_space nil)
(x!1 skolem-const-decl "T" metric_space nil)
(x!2 skolem-const-decl "T" metric_space nil)
(member const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(metric_triangle formula-decl nil metric_space nil)
(subset? const-decl "bool" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(ball_centre formula-decl nil metric_space nil))
shostak))
(metric_open_TCC1 0
(metric_open_TCC1-1 nil 3359138684
("" (expand "metric_open_set")
(("" (expand "emptyset")
(("" (expand "metric_open?")
(("" (skosimp)
(("" (skosimp)
(("" (expand "subset?")
(("" (inst - "x!1")
(("" (rewrite "ball_centre")
(("" (expand "member") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((emptyset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(ball_centre formula-decl nil metric_space 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(member const-decl "bool" sets nil)
(T formal-type-decl nil metric_space nil)
(metric_open? const-decl "bool" metric_space_def nil)
(metric_open_set const-decl "set[T]" metric_space nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(metric_closed_TCC1 0
(metric_closed_TCC1-1 nil 3359138684
("" (expand "metric_closed_set")
(("" (expand "metric_closed?")
(("" (rewrite "complement_complement")
(("" (rewrite "metric_open_TCC1") nil nil)) nil))
nil))
nil)
((metric_closed? const-decl "bool" metric_space_def nil)
(metric_open_TCC1 subtype-tcc nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(metric_open_set const-decl "set[T]" metric_space nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complement_complement formula-decl nil sets_lemmas nil)
(metric_closed_set const-decl "set[T]" metric_space nil))
shostak))
(ball_is_metric_open 0
(ball_is_metric_open-1 nil 3359138684
("" (skosimp)
(("" (expand "metric_open?")
(("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (case-replace "x!2=x!1")
(("1" (inst + "r!1")
(("1" (rewrite "subset_reflexive") nil nil)) nil)
("2" (lemma "metric_zero" ("x" "x!1" "y" "x!2"))
(("2" (assert)
(("2" (case "r!1-d(x!1,x!2)>0")
(("1" (inst + "r!1 - d(x!1, x!2)")
(("1" (expand "subset?")
(("1" (skosimp)
(("1" (expand "member")
(("1" (expand "ball")
(("1"
(lemma
"metric_triangle"
("x" "x!1" "y" "x!2" "z" "x!3"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (expand "ball") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "subset?")
(("2" (inst - "x!2")
(("2" (rewrite "ball_centre")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_open? const-decl "bool" metric_space_def nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(ball const-decl "set[T]" metric_space_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(r!1 skolem-const-decl "posreal" metric_space nil)
(x!1 skolem-const-decl "T" metric_space nil)
(x!2 skolem-const-decl "T" metric_space nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(metric_triangle formula-decl nil metric_space nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_zero formula-decl nil metric_space nil)
(ball_centre formula-decl nil metric_space nil))
shostak))
(metric_space_is_topology? 0
(metric_space_is_topology?-1 nil 3382769693
("" (expand "metric_induced_topology")
(("" (expand "topology?")
(("" (split)
(("1" (expand "topology_empty?")
(("1" (expand "member")
(("1" (expand "metric_open?")
(("1" (skosimp)
(("1" (expand "emptyset")
(("1" (skosimp)
(("1" (expand "subset?")
(("1" (inst - "x!1")
(("1" (expand "member")
(("1" (expand "ball")
(("1" (rewrite "metric_is_0")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "topology_full?")
(("2" (expand "fullset")
(("2" (expand "member")
(("2" (expand "metric_open?")
(("2" (skosimp)
(("2" (expand "subset?")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "topology_Union?")
(("3" (expand "subset?")
(("3" (expand "member")
(("3" (skosimp)
(("3" (expand "metric_open?")
(("3" (skosimp)
(("3" (split 1)
(("1" (flatten)
(("1" (expand "Union")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1"
(inst - "a!1")
(("1"
(assert)
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "r!1")
(("1"
(expand "subset?")
(("1"
(skosimp)
(("1"
(inst - "x!2")
(("1"
(expand "member")
(("1"
(inst + "a!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "subset?")
(("2" (expand "Union")
(("2" (expand "member")
(("2"
(inst - "x!1")
(("2"
(lemma
"ball_centre"
("x" "x!1" "r" "r!1"))
(("2"
(expand "member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "topology_intersection?")
(("4" (skosimp)
(("4" (typepred "A!1")
(("4" (typepred "B!1")
(("4" (expand "intersection")
(("4" (expand "metric_open?")
(("4" (expand "member")
(("4" (skosimp)
(("4" (inst - "x!1")
(("4" (inst - "x!1")
(("4" (split 1)
(("1"
(flatten)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst + "min(r!1,r!2)")
(("1"
(hide -4 -6)
(("1"
(expand "subset?")
(("1"
(skosimp)
(("1"
(inst - "x!2")
(("1"
(inst - "x!2")
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(expand "min")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(skosimp)
(("2"
(assert)
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2"
(rewrite "ball_centre")
(("2"
(expand "member")
(("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)
((topology? const-decl "bool" topology_prelim "topology/")
(topology_intersection? const-decl "bool" topology_prelim
"topology/")
(d formal-const-decl "metric" metric_space nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(set type-eq-decl nil sets nil)
(intersection const-decl "set" sets nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(topology_Union? const-decl "bool" topology_prelim "topology/")
(Union const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(ball_is_metric_open application-judgement "metric_open"
metric_space nil)
(ball_centre formula-decl nil metric_space nil)
(topology_full? const-decl "bool" topology_prelim "topology/")
(fullset const-decl "set" sets nil)
(topology_empty? const-decl "bool" topology_prelim "topology/")
(metric_open? const-decl "bool" metric_space_def nil)
(emptyset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(metric_is_0 formula-decl nil metric_space nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball const-decl "set[T]" metric_space_def nil)
(T formal-type-decl nil metric_space nil)
(member const-decl "bool" sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil))
nil))
(metric_space_is_hausdorff? 0
(metric_space_is_hausdorff?-1 nil 3359138686
("" (expand "hausdorff?")
(("" (expand "is_T2?")
(("" (skosimp)
(("" (lemma "metric_zero" ("x" "x!1" "y" "y!1"))
(("" (assert)
(("" (name "R" "d(x!1,y!1)/2")
(("" (inst + "ball(x!1,R)" "ball(y!1,R)")
(("1" (split 3)
(("1" (expand "disjoint?")
(("1" (expand "intersection")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (skosimp)
(("1" (expand "ball")
(("1"
(lemma
"metric_triangle"
("x" "x!1" "y" "x!2" "z" "y!1"))
(("1"
(lemma
"metric_symmetric"
("x" "y!1" "y" "x!2"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "ball_centre" ("x" "x!1" "r" "R"))
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "ball_centre" ("x" "y!1" "r" "R"))
(("3" (expand "member") (("3" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "metric_induced_topology")
(("2" (propax) nil nil)) nil)
("3" (expand "metric_induced_topology")
(("3" (propax) nil nil)) nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((is_T2? const-decl "bool" topology_prelim "topology/")
(metric_zero formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(d formal-const-decl "metric" metric_space nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(intersection const-decl "set" sets nil)
(metric_symmetric formula-decl nil metric_space nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(metric_triangle formula-decl nil metric_space nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(ball_centre formula-decl nil metric_space nil)
(y!1 skolem-const-decl "T" metric_space nil)
(x!1 skolem-const-decl "T" metric_space nil)
(ball const-decl "set[T]" metric_space_def nil)
(set type-eq-decl nil sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(R skolem-const-decl "nnreal" metric_space nil)
(> const-decl "bool" reals nil)
(ball_is_metric_open application-judgement "metric_open"
metric_space nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(hausdorff? const-decl "bool" topology_prelim "topology/")
(metric_space_is_topology? name-judgement "(topology?)"
metric_space nil))
shostak))
(metric_space_is_hausdorff 0
(metric_space_is_hausdorff-1 nil 3384417346
("" (judgement-tcc) nil nil)
((T formal-type-decl nil metric_space nil)
(hausdorff_space? const-decl "bool" topology_prelim "topology/")
(metric_space_is_topology? name-judgement "(topology?)"
metric_space nil)
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
metric_space nil))
nil))
(metric_open_def 0
(metric_open_def-1 nil 3359138576
("" (skosimp)
(("" (expand "open?")
(("" (expand "member")
(("" (expand "metric_induced_topology") (("" (propax) nil nil))
nil))
nil))
nil))
nil)
((open? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(member const-decl "bool" sets nil))
shostak))
(metric_closed_def 0
(metric_closed_def-1 nil 3359138599
("" (skosimp)
(("" (expand "metric_closed?")
(("" (expand "closed?")
(("" (expand "metric_induced_topology")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((metric_closed? const-decl "bool" metric_space_def nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(member const-decl "bool" sets nil)
(closed? const-decl "bool" topology "topology/"))
shostak))
(metric_open_is_open 0
(metric_open_is_open-1 nil 3359138623
("" (skosimp) (("" (rewrite "metric_open_def" 1 :dir rl) nil nil))
nil)
((metric_open_def formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_open? const-decl "bool" metric_space_def nil)
(metric_open nonempty-type-eq-decl nil metric_space nil))
shostak))
(open_is_metric_open 0
(open_is_metric_open-1 nil 3359138648
("" (skosimp) (("" (rewrite "metric_open_def") nil nil)) nil)
((metric_open_def formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/"))
shostak))
(metric_closed_is_closed 0
(metric_closed_is_closed-1 nil 3359138658
("" (skosimp) (("" (rewrite "metric_closed_def" 1 :dir rl) nil nil))
nil)
((metric_closed_def formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_closed? const-decl "bool" metric_space_def nil)
(metric_closed nonempty-type-eq-decl nil metric_space nil))
shostak))
(closed_is_metric_closed 0
(closed_is_metric_closed-1 nil 3359138674
("" (skosimp) (("" (rewrite "metric_closed_def") nil nil)) nil)
((metric_closed_def formula-decl nil metric_space nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(closed? const-decl "bool" topology "topology/")
(closed nonempty-type-eq-decl nil topology "topology/"))
shostak))
(metric_adherent_iff_adherent 0
(metric_adherent_iff_adherent-1 nil 3406977548
("" (skosimp)
(("" (expand "metric_adherent?")
(("" (expand "adherent_point?")
(("" (split)
(("1" (flatten)
(("1" (skosimp*)
(("1" (expand "neighbourhood?")
(("1" (expand "interior_point?")
(("1" (skosimp)
(("1" (expand "member")
(("1" (typepred "U!2")
(("1" (typepred "U!1")
(("1" (rewrite "metric_open_def" -1 :dir rl)
(("1" (expand "metric_open?")
(("1"
(expand "nonempty?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst -4 "x!1")
(("1"
(assert)
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst -3 "r!1")
(("1"
(skosimp)
(("1"
(inst
-
"x!2")
(("1"
(assert)
(("1"
(inst
-
"x!2")
(("1"
(assert)
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" (skosimp*)
(("2" (expand "intersection")
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "ball(x!1, r!1)")
(("2" (split -1)
(("1" (skosimp)
(("1" (inst - "x!2") (("1" (assert) nil nil))
nil))
nil)
("2" (expand "neighbourhood?")
(("2" (expand "interior_point?")
(("2" (inst + "ball(x!1, r!1)")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(split)
(("1" (skosimp) nil nil)
("2"
(lemma
"ball_centre"
("x" "x!1" "r" "r!1"))
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_adherent? const-decl "bool" metric_space_def nil)
(interior_point? const-decl "bool" topology "topology/")
(member const-decl "bool" sets nil)
(metric_open? const-decl "bool" metric_space_def nil)
(intersection const-decl "set" sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(ball_is_metric_open application-judgement "metric_open"
metric_space nil)
(subset? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(metric_open_def formula-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil metric_space nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(neighbourhood? const-decl "bool" topology "topology/")
(ball const-decl "set[T]" metric_space_def nil)
(ball_centre formula-decl nil metric_space nil)
(adherent_point? const-decl "bool" topology "topology/"))
shostak))
(metric_closure_is_Cl 0
(metric_closure_is_Cl-1 nil 3406977926
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "metric_closure")
(("" (expand "Cl")
(("" (rewrite "metric_adherent_iff_adherent") nil nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(Cl const-decl "set[T]" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(metric_closure const-decl "set[T]" metric_space_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(metric? const-decl "bool" metric_def nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(metric_space_is_hausdorff name-judgement "hausdorff" metric_space
nil)
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
metric_space nil)
(Cl_is_closed application-judgement
"closed[T, (metric_induced_topology)]" metric_space nil)
(metric_adherent_iff_adherent formula-decl nil metric_space nil))
shostak))
(metric_convergence_def 0
(metric_convergence_def-1 nil 3390467646
("" (expand "metric_converges_to")
(("" (expand "convergence?")
(("" (skosimp)
(("" (split)
(("1" (skosimp*)
(("1" (inst - "ball(x!1, r!1)")
(("1" (lemma "ball_centre" ("x" "x!1" "r" "r!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "U!1")
(("2" (expand "open?")
(("2" (expand "member")
(("2" (expand "metric_induced_topology")
(("2" (expand "metric_open?")
(("2" (inst - "x!1")
(("2" (assert)
(("2" (skosimp)
(("2" (inst - "r!1")
(("2"
(skosimp)
(("2"
(inst + "n!1")
(("2"
(skosimp)
(("2"
(inst - "i!1")
(("2"
(assert)
(("2"
(expand "subset?")
(("2"
(inst - "u!1(i!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergence? const-decl "bool" topological_convergence
"topology/")
(ball_is_metric_open application-judgement "metric_open"
metric_space nil)
(T formal-type-decl nil metric_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(metric? const-decl "bool" metric_def nil)
(metric nonempty-type-eq-decl nil metric_def nil)
(d formal-const-decl "metric" metric_space nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ball const-decl "set[T]" metric_space_def nil)
(member const-decl "bool" sets nil)
(ball_centre formula-decl nil metric_space nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(metric_open? const-decl "bool" metric_space_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(subset? const-decl "bool" sets nil)
(sequence type-eq-decl nil sequences nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(metric_converges_to const-decl "bool" metric_space_def nil))
shostak))
(compact_is_weierstrass_bolzano 0
(compact_is_weierstrass_bolzano-1 nil 3406536163
("" (flatten)
(("" (lemma "compact_def[T,(metric_induced_topology)]")
(("" (flatten)
(("" (hide -2)
(("" (split)
(("1" (expand "weierstrass_bolzano?")
(("1" (skosimp)
(("1"
(name "AA"
"lambda (n:nat): metric_closure({x | exists (m:nat): m>n & x = u!1(m)})")
(("1"
(case "forall (n,m:nat): n > m => subset?(AA(n),AA(m))")
(("1" (inst -3 "image(AA,fullset[nat])")
(("1" (hide -4)
(("1" (split -3)
(("1" (expand "fullset")
(("1" (expand "image")
(("1"
(expand "Intersection")
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(case
"forall (n:nat): AA(n)(x!1)")
(("1"
(hide -2)
(("1"
(replace -3 -1 rl)
(("1"
(assert)
(("1"
(expand
"metric_closure"
-1)
(("1"
(expand
"metric_adherent?")
(("1"
(expand
"intersection")
(("1"
(expand
"nonempty?")
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(name
"NEXT"
"lambda (i:nat,k:posnat): (choose({j:nat | j>i & d(x!1,u!1(j)) <1/k}),k+1)")
(("1"
(name
"SEQ"
"lambda (n:nat): u!1((iterate[[nat, posnat]](NEXT, n)(0, 1))`1)")
(("1"
(inst
+
"SEQ")
(("1"
(split)
(("1"
(expand
"subseq?")
(("1"
(expand
"SEQ")
(("1"
(inst
+
"lambda (i:nat): (iterate[[nat, posnat]](NEXT, i)(0, 1))`1")
(("1"
(skosimp)
nil
nil)
("2"
(expand
"strict_increasing?")
(("2"
(skolem
+
("i!1"
"j!1"))
(("2"
(assert)
(("2"
(flatten)
(("2"
(lemma
"iterate_add_applied[[nat, posnat]]"
("f"
"NEXT"
"x"
"(0, 1)"
"n"
"i!1"
"m"
"j!1-i!1"))
(("1"
(assert)
(("1"
(replace
-1
1
rl)
(("1"
(name-replace
"DRL1"
"(iterate[[nat, posnat]](NEXT, i!1)(0, 1))")
(("1"
(hide-all-but
(1
-4
-2))
(("1"
(case
"forall (pn:posnat,x:[[nat, posnat]]): x`1 < (iterate(NEXT, pn)(x))`1")
(("1"
(inst
-
"j!1-i!1"
"DRL1")
nil
nil)
("2"
(hide
2)
(("2"
(induct
"pn")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil)
("3"
(skosimp*)
(("3"
(case-replace
"j!2=0")
(("1"
(hide
-2
-1
-3
-4)
(("1"
(expand
"iterate")
(("1"
(expand
"iterate")
(("1"
(expand
"NEXT")
(("1"
(lemma
"choose_member"
("a"
"{j: nat | j > x!2`1 & d(x!1, u!1(j)) < 1 / x!2`2}"))
(("1"
(case-replace
"empty?({j: nat | j > x!2`1 & d(x!1, u!1(j)) < 1 / x!2`2})")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.62 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.
|
