|
(real_intervals
(rationals_TCC1 0
(rationals_TCC1-1 nil 3452487339
(""
(lemma "Union_is_borel"
("A"
"image[rational,set[real]](lambda (q:rational): singleton[real](q),fullset[rational])"))
(("1"
(case-replace "(Union(extend
[setof[real], borel[real, metric_induced_topology],
bool, FALSE]
(restrict
[set[real],
borel
[real,
metric_induced_topology
],
boolean]
(image[rational, set[real]]
(LAMBDA (q: rational): singleton[real](q),
fullset[rational])))))={x:real | rational_pred(x)}")
(("1" (hide -1 2)
(("1" (apply-extensionality :hide? t)
(("1" (expand "fullset")
(("1" (expand "image")
(("1" (expand "restrict")
(("1" (expand "extend")
(("1" (case-replace "rational_pred(x!1)")
(("1" (expand "Union")
(("1" (inst + "singleton[real](x!1)")
(("1" (expand "singleton")
(("1" (propax) nil nil)) nil)
("2" (prop)
(("1" (inst + "x!1") nil nil)
("2" (rewrite "singleton_is_borel") nil
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "Union")
(("2" (skosimp)
(("2" (typepred "a!1")
(("2" (assert)
(("2"
(skosimp)
(("2"
(replace -1)
(("2"
(typepred "x!2")
(("2"
(expand "singleton")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(lemma "countable_image[rational, set[real]]"
("f" "LAMBDA (q: rational): singleton[real](q)" "S"
"fullset[rational]"))
(("2" (split -1)
(("1" (expand "image" -1)
(("1" (assert)
(("1"
(name-replace "XX" "(image[rational, set[real]]
(LAMBDA (q: rational): singleton[real](q),
fullset[rational]))")
(("1" (expand "restrict")
(("1" (expand "is_countable")
(("1" (skosimp)
(("1" (typepred "f!1")
(("1"
(inst +
"lambda (b:borel): if XX(b) then f!1(b) else 0 endif")
(("1" (expand "restrict")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "is_countable_cross[int,posnat]")
(("2" (inst - "fullset[int]" "fullset[posnat]")
(("2" (split)
(("1" (expand "fullset")
(("1" (expand "cross_product")
(("1" (expand "is_countable")
(("1" (skosimp)
(("1" (typepred "f!1")
(("1"
(inst +
"lambda (q:rational): f!1(numerator(q),denominator(q))")
(("1"
(expand "injective?")
(("1"
(skosimp)
(("1"
(inst
-
"(numerator(x1!1), denominator(x1!1))"
"(numerator(x2!1), denominator(x2!1))")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(flatten)
(("1"
(case
"numerator(x1!1)/denominator(x1!1)=numerator(x2!1)/denominator(x2!1)")
(("1"
(rewrite
"rational_def"
-1)
(("1"
(rewrite
"rational_def"
-1)
nil
nil))
nil)
("2"
(assert)
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "fullset")
(("2" (expand "is_countable")
(("2"
(inst +
"lambda (i:int): 2*abs(i) + if i <0 then 1 else 0 endif")
(("2" (expand "injective?")
(("2" (skosimp)
(("2"
(case "x1!1>=0")
(("1"
(case "x2!1>=0")
(("1" (grind) nil nil)
("2" (grind) nil nil))
nil)
("2"
(case "x2!1>=0")
(("1" (grind) nil nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (expand "fullset")
(("3" (expand "is_countable")
(("3" (inst + "lambda (pn:posnat): pn-1")
(("3" (expand "injective?")
(("3" (skosimp) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((XX skolem-const-decl "set[set[real]]" real_intervals nil)
(f!1 skolem-const-decl "(injective?[(XX), nat])" real_intervals
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)
(image const-decl "set[R]" function_image nil)
(is_countable_cross formula-decl nil countable_cross
"metric_space/")
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(cross_product const-decl "set[[T1, T2]]" cross_product
"topology/")
(denominator const-decl "posnat" rational_props_aux "power/")
(numerator const-decl "int" rational_props_aux "power/")
(rat nonempty-type-eq-decl nil rationals nil)
(f!1 skolem-const-decl "(injective?[({z | TRUE}), nat])"
real_intervals nil)
(rational_def formula-decl nil rational_props_aux "power/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(< const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(countable_image formula-decl nil countable_image "sets_aux/")
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(Union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(singleton_is_borel formula-decl nil hausdorff_borel
"measure_integration/")
(TRUE const-decl "bool" booleans nil)
(x!1 skolem-const-decl "real" real_intervals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(singleton_is_compact application-judgement
"compact[real, metric_induced_topology]" real_intervals nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" countable_props "sets_aux/")
(real_minus_real_is_real application-judgement "real" reals nil)
(metric_space_is_hausdorff name-judgement "hausdorff[real]"
real_topology "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_topology "metric_space/")
(metric_induced_topology_is_second_countable name-judgement
"second_countable" real_topology "metric_space/")
(Union_is_borel formula-decl nil borel "measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(borel? const-decl "sigma_algebra" borel "measure_integration/")
(borel nonempty-type-eq-decl nil borel "measure_integration/")
(set type-eq-decl nil sets nil)
(is_countable const-decl "bool" countability "sets_aux/")
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(restrict const-decl "R" restrict nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(image const-decl "set[R]" function_image nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets 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/"))
nil)))
¤ Dauer der Verarbeitung: 0.3 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.
|
