|
(real_borel
(borel_generated_by_rational_open_interval 0
(borel_generated_by_rational_open_interval-1 nil 3425663944
(""
(lemma "borel_countable_basis"
("B" "fullset[rational_open_interval]"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (lemma "countable_rational_open_interval")
(("2" (expand "fullset")
(("2" (expand "extend")
(("2" (expand "is_countable")
(("2" (skosimp)
(("2" (typepred "f!1")
(("2" (inst + "f!1")
(("2" (split)
(("1" (skosimp) (("1" (prop) nil nil)) nil)
("2" (expand "injective?")
(("2" (skosimp)
(("2" (inst - "x1!1" "x2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset")
(("2" (expand "extend")
(("2" (hide 2)
(("2" (expand "metric_induced_topology")
(("2" (expand "base?")
(("2" (split)
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (skosimp)
(("1" (prop)
(("1" (skosimp)
(("1" (replace -1)
(("1"
(lemma "metric_open_ball"
("x" "q!1" "r" "pq!1"))
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "A!1")
(("2"
(inst +
"{X:set[real]| EXISTS (q:rat,pq:posrat): X=ball(q,pq) & subset?[real](X,A!1)}")
(("2" (split)
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (skosimp)
(("1"
(skosimp)
(("1"
(prop)
(("1" (inst + "q!1" "pq!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality :hide? t)
(("2" (case-replace "A!1(x!1)")
(("1" (expand "Union")
(("1"
(expand "metric_open?")
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(lemma
"density"
("x" "x!1-r!1" "y" "x!1"))
(("1"
(lemma
"density"
("x" "x!1" "y" "x!1+r!1"))
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst
+
"ball((r!3+r!2)/2,abs((r!3-r!2)/2))")
(("1"
(expand "ball")
(("1"
(grind)
nil
nil))
nil)
("2"
(inst
+
"(r!2 + r!3) / 2"
"abs((r!3 - r!2) / 2)")
(("1"
(expand "subset?")
(("1"
(skosimp)
(("1"
(inst - "x!2")
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(grind)
nil
nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(expand "Union")
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(skosimp)
(("2"
(expand "subset?")
(("2"
(inst - "x!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)
((real_minus_real_is_real application-judgement "real" reals nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(A!1 skolem-const-decl "({S | metric_open?(S)})" real_borel nil)
(r!2 skolem-const-decl "rat" real_borel nil)
(r!3 skolem-const-decl "rat" real_borel nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}"
real_defs nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(density formula-decl nil rational_props nil)
(metric_open? const-decl "bool" metric_space_def "metric_space/")
(subset? const-decl "bool" sets nil)
(metric_open_ball formula-decl nil metric_space "metric_space/")
(member const-decl "bool" sets nil)
(countable_rational_open_interval formula-decl nil real_topology
"metric_space/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(f!1 skolem-const-decl "(injective?[({x | TRUE}), nat])" real_borel
nil)
(injective? const-decl "bool" functions 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)
(TRUE const-decl "bool" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(is_countable const-decl "bool" countability "sets_aux/")
(metric_induced_topology_is_second_countable name-judgement
"second_countable" real_topology "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_topology "metric_space/")
(metric_space_is_hausdorff name-judgement "hausdorff[real]"
real_topology "metric_space/")
(borel_countable_basis formula-decl nil borel nil)
(topology? const-decl "bool" topology_prelim "topology/")
(topology nonempty-type-eq-decl nil topology_prelim "topology/")
(base? const-decl "bool" basis "topology/")
(set type-eq-decl nil sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(> const-decl "bool" reals nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(rational_open_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/"))
shostak))
(borel_generated_by_open_interval 0
(borel_generated_by_open_interval-1 nil 3425664555
("" (apply-extensionality :hide? t)
(("1" (expand "fullset")
(("1" (rewrite "borel_generated_by_rational_open_interval")
(("1" (expand "fullset")
(("1"
(case-replace "generated_sigma_algebra(extend
[setof[real], rational_open_interval,
bool, FALSE]
({x: rational_open_interval | TRUE}))
(x!1)")
(("1" (expand "extend")
(("1" (expand "generated_sigma_algebra")
(("1" (expand "Intersection")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1" (inst - "a!1")
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (skosimp*)
(("1"
(prop)
(("1"
(skosimp)
(("1"
(inst - "x!2")
(("1"
(prop)
(("1"
(inst + "q!1" "pq!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "extend")
(("2" (expand "generated_sigma_algebra")
(("2" (expand "Intersection")
(("2" (skosimp)
(("2" (typepred "a!1")
(("2" (expand "subset?" -2)
(("2" (expand "member")
(("2" (inst -3 "a!1")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp*)
(("2"
(prop)
(("2"
(skosimp)
(("2"
(replace -1)
(("2"
(hide -1 2)
(("2"
(name
"VV"
"{X:set[real]| EXISTS (q:rat,pq:posrat): X = ball(q,pq) & subset?[real](ball(q,pq),ball(x!3,r!1))}")
(("2"
(case-replace
"ball(x!3, r!1) = Union(VV)")
(("1"
(expand
"sigma_algebra?")
(("1"
(expand
"sigma_algebra_union?")
(("1"
(flatten)
(("1"
(inst - "VV")
(("1"
(expand
"member")
(("1"
(split -5)
(("1"
(propax)
nil
nil)
("2"
(hide-all-but
1)
(("2"
(lemma
"countable_rational_open_interval")
(("2"
(expand
"is_countable")
(("2"
(skosimp)
(("2"
(typepred
"f!1")
(("2"
(inst
+
"lambda (x:(VV)): f!1(x)")
(("1"
(expand
"injective?")
(("1"
(skosimp)
(("1"
(typepred
"x1!1")
(("1"
(typepred
"x2!1")
(("1"
(inst
-
"x1!1"
"x2!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(typepred
"x!4")
(("2"
(expand
"VV")
(("2"
(skosimp)
(("2"
(expand
"fullset")
(("2"
(inst
+
"q!1"
"pq!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(typepred
"x!4")
(("3"
(replace
-3
-1
rl)
(("3"
(assert)
(("3"
(skosimp)
(("3"
(inst
-7
"x!4")
(("3"
(assert)
(("3"
(prop)
(("3"
(inst
+
"q!1"
"pq!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality
:hide?
t)
(("2"
(case-replace
"ball(x!3, r!1)(x!4)")
(("1"
(expand
"Union")
(("1"
(hide -3 -2)
(("1"
(expand
"ball")
(("1"
(case
"x!3-r!1)
(("1"
(flatten)
(("1"
(lemma
"density"
("x"
"x!3-r!1"
"y"
"x!4"))
(("1"
(lemma
"density"
("x"
"x!4"
"y"
"x!3+r!1"))
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(name
"XX"
"(r!2+r!3)/2")
(("1"
(name
"RR"
"(r!2-r!3)/2")
(("1"
(inst
+
"ball(XX,RR)")
(("1"
(expand
"ball")
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"VV")
(("2"
(inst
+
"XX"
"RR")
(("1"
(expand
"ball")
(("1"
(grind)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"Union")
(("2"
(skosimp)
(("2"
(typepred
"a!2")
(("2"
(expand
"VV")
(("2"
(hide
-3)
(("2"
(skosimp)
(("2"
(hide
-4
-5)
(("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(inst
-
"x!4")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"metric_induced_topology[real, (LAMBDA (x, y: real): abs(x - y))]")
(("2" (expand "hausdorff_space?") (("2" (propax) nil nil)) nil))
nil))
nil)
((a!1 skolem-const-decl "({Y |
sigma_algebra?(Y) AND
subset?(LAMBDA (t: setof[real]):
IF EXISTS q, pq: t = ball(q, pq) THEN TRUE ELSE FALSE ENDIF,
Y)})" real_borel nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(density formula-decl nil rational_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
(RR skolem-const-decl "rat" real_borel nil)
(XX skolem-const-decl "rat" real_borel nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(x!5 skolem-const-decl "real" real_borel nil)
(minus_real_is_real application-judgement "real" reals nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(is_countable const-decl "bool" countability "sets_aux/")
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(f!1 skolem-const-decl
"(injective?[(fullset[rational_open_interval]), nat])" real_borel
nil)
(VV skolem-const-decl "[set[real] -> boolean]" real_borel nil)
(countable_rational_open_interval formula-decl nil real_topology
"metric_space/")
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(Union const-decl "set" sets nil)
(Intersection const-decl "set" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(member const-decl "bool" sets nil)
(a!1 skolem-const-decl "({Y |
sigma_algebra?(Y) AND
subset?(LAMBDA (t: setof[real]):
IF EXISTS x, r: t = ball(x, r) THEN TRUE ELSE FALSE ENDIF,
Y)})" real_borel nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(rational_open_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(TRUE const-decl "bool" booleans nil)
(borel_generated_by_rational_open_interval formula-decl nil
real_borel nil)
(metric_induced_topology_is_second_countable name-judgement
"second_countable" real_topology "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_topology "metric_space/")
(metric_space_is_hausdorff name-judgement "hausdorff[real]"
real_topology "metric_space/")
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel? const-decl "sigma_algebra" borel nil)
(generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(set type-eq-decl nil sets nil) (> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(open_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(open_interval_borel_rew 0
(open_interval_borel_rew-1 nil 3509858353
("" (skosimp)
(("" (lemma "open_is_borel" ("X" "A!1"))
(("1" (expand "real_borel") (("1" (propax) nil nil)) nil)
("2" (typepred "A!1")
(("2" (skosimp)
(("2" (replace -1)
(("2" (assert)
(("2" (hide 2)
(("2" (expand "open?")
(("2" (expand "member")
(("2" (expand "metric_induced_topology")
(("2" (assert)
(("2" (rewrite "metric_open_ball") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(open_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(ball const-decl "set[T]" metric_space_def "metric_space/")
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(open nonempty-type-eq-decl nil topology "topology/")
(open? const-decl "bool" topology "topology/")
(set type-eq-decl nil sets nil)
(open_is_borel formula-decl nil borel nil)
(real_borel const-decl "sigma_algebra" real_borel nil)
(metric_open_ball formula-decl nil metric_space "metric_space/")
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(closed_interval_borel_rew 0
(closed_interval_borel_rew-1 nil 3509858388
("" (skosimp)
(("" (typepred "B!1")
(("" (skosimp)
(("" (typepred "closed_ball(x!1, r!1)")
(("" (expand "real_borel")
(("" (lemma "closed_is_borel" ("Y" "B!1"))
(("1" (propax) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(closed_is_borel formula-decl nil borel nil)
(real_borel const-decl "sigma_algebra" real_borel nil))
shostak))
(left_semiclosed_interval_borel_rew 0
(left_semiclosed_interval_borel_rew-1 nil 3509858573
("" (skosimp)
(("" (typepred "L!1")
(("" (skosimp)
(("" (expand "real_borel")
(("" (lemma "closed_is_borel" ("Y" "L!1"))
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((left_semiclosed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_inf const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_borel const-decl "sigma_algebra" real_borel nil)
(closed_is_borel formula-decl nil borel nil))
shostak))
(right_semiclosed_interval_borel_rew 0
(right_semiclosed_interval_borel_rew-1 nil 3509858604
("" (skosimp)
(("" (expand "real_borel")
(("" (typepred "R!1")
(("" (skosimp)
(("" (lemma "closed_is_borel" ("Y" "R!1"))
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_borel const-decl "sigma_algebra" real_borel nil)
(closed_is_borel formula-decl nil borel nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl "bool" topology "topology/")
(closed nonempty-type-eq-decl nil topology "topology/")
(inf_closed const-decl "closed" real_topology "metric_space/")
(right_semiclosed_interval nonempty-type-eq-decl nil real_topology
"metric_space/"))
shostak))
(open_interval_is_borel 0
(open_interval_is_borel-1 nil 3425663719
("" (skolem + "X!1")
(("" (lemma "open_interval_borel_rew" ("A" "X!1"))
(("" (expand "real_borel") (("" (propax) nil nil)) nil)) nil))
nil)
((open_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(ball const-decl "set[T]" metric_space_def "metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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) (set type-eq-decl nil sets 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(open_interval_borel_rew formula-decl nil real_borel nil)
(real_borel const-decl "sigma_algebra" real_borel nil))
nil))
(closed_interval_is_borel 0
(closed_interval_is_borel-1 nil 3425710076
("" (skolem + "A!1")
(("" (lemma "closed_interval_borel_rew" ("B" "A!1"))
(("" (expand "real_borel") (("" (propax) nil nil)) nil)) nil))
nil)
((closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(closed_interval_borel_rew formula-decl nil real_borel nil)
(real_borel const-decl "sigma_algebra" real_borel nil))
nil))
(left_semiclosed_interval_is_borel 0
(left_semiclosed_interval_is_borel-1 nil 3509858281
("" (skolem + "X!1")
(("" (lemma "left_semiclosed_interval_borel_rew" ("L" "X!1"))
(("" (expand "real_borel") (("" (propax) nil nil)) nil)) nil))
nil)
((left_semiclosed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_inf const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(left_semiclosed_interval_borel_rew formula-decl nil real_borel
nil)
(real_borel const-decl "sigma_algebra" real_borel nil))
nil))
(right_semiclosed_interval_is_borel 0
(right_semiclosed_interval_is_borel-1 nil 3509858281
("" (skolem + "X!1")
(("" (lemma "right_semiclosed_interval_borel_rew" ("R" "X!1"))
(("" (expand "real_borel") (("" (propax) nil nil)) nil)) nil))
nil)
((right_semiclosed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(inf_closed const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(right_semiclosed_interval_borel_rew formula-decl nil real_borel
nil)
(real_borel const-decl "sigma_algebra" real_borel nil))
nil))
(borel_generated_by_left_semiclosed_interval 0
(borel_generated_by_left_semiclosed_interval-1 nil 3509858895
("" (apply-extensionality :hide? t)
((""
(lemma "generated_sigma_algebra_subset2"
("X" "fullset[left_semiclosed_interval]" "Y" "(borel?)"))
(("" (split)
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (inst - "x!1")
(("1" (case-replace "borel?(x!1)")
(("1" (rewrite "borel_generated_by_open_interval")
(("1" (expand "fullset")
(("1" (expand "extend")
(("1" (expand "generated_sigma_algebra")
(("1" (expand "Intersection")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst -3 "a!1")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(prop)
(("1"
(skosimp)
(("1"
(hide 2)
(("1"
(name
"AA"
"lambda (n:nat): difference[real](closed_inf(x!3-r!1+1/(1+n)),closed_inf(x!3+r!1))")
(("1"
(case-replace
"x!2=IUnion(AA)")
(("1"
(hide -1 -3 -2)
(("1"
(case
"forall (n:nat): a!1(AA(n))")
(("1"
(assert)
(("1"
(expand
"sigma_algebra?")
(("1"
(flatten)
(("1"
(hide
-5
-3
-2)
(("1"
(expand
"sigma_algebra_union?")
(("1"
(inst
-2
"image(AA,fullset[nat])")
(("1"
(lemma
"countable_image[nat,set[real]]")
(("1"
(inst
-
"fullset[nat]"
"AA")
(("1"
(split
-1)
(("1"
(expand
"image"
-1)
(("1"
(replace
-1)
(("1"
(split
-3)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.73 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.
|
