:: RCOMP_1 semantic presentation begin definitionlet "g", "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[."::: redefine func :::"[.":::"g" "," "s":::".]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RCOMP_1:def 1 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool "g" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) "s") ")" ) "}" ; end; :: deftheorem defines :::"[."::: RCOMP_1:def 1 : (Bool "for" (Set (Var "g")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "g")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" ) "}" )); definitionlet "g", "s" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"]."::: redefine func :::"].":::"g" "," "s":::".["::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RCOMP_1:def 2 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool "g" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) "s") ")" ) "}" ; end; :: deftheorem defines :::"]."::: RCOMP_1:def 2 : (Bool "for" (Set (Var "g")) "," (Set (Var "s")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "g")) "," (Set (Var "s")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) "}" )); theorem :: RCOMP_1:1 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) ")" )) ; theorem :: RCOMP_1:2 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "iff" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p")))) ")" )) ; theorem :: RCOMP_1:3 (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p")))) ")" )) ; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "X" is :::"compact"::: means :: RCOMP_1:def 3 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) "X")) "holds" (Bool "ex" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "s2")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s1"))) & (Bool (Set (Var "s2")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s2"))) ($#r2_hidden :::"in"::: ) "X") ")" ))); end; :: deftheorem defines :::"compact"::: RCOMP_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "s2")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s1"))) & (Bool (Set (Var "s2")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s2"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ))) ")" )); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "X" is :::"closed"::: means :: RCOMP_1:def 4 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) "X") & (Bool (Set (Var "s1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"closed"::: RCOMP_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "s1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "X" is :::"open"::: means :: RCOMP_1:def 5 (Bool (Set "X" ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_rcomp_1 :::"closed"::: ) ); end; :: deftheorem defines :::"open"::: RCOMP_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) ) "iff" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" )); theorem :: RCOMP_1:4 (Bool "for" (Set (Var "s")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "s")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "s1")) "is" ($#v1_comseq_2 :::"bounded"::: ) ))) ; theorem :: RCOMP_1:5 (Bool "for" (Set (Var "s")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "s")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ; theorem :: RCOMP_1:6 (Bool "for" (Set (Var "s")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "s")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) "is" ($#v1_rcomp_1 :::"compact"::: ) )) ; theorem :: RCOMP_1:7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_rcomp_1 :::".["::: ) ) "is" ($#v3_rcomp_1 :::"open"::: ) )) ; registrationlet "p", "q" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_xxreal_1 :::"]."::: ) "p" "," "q" ($#k4_xxreal_1 :::".["::: ) ) -> ($#v3_rcomp_1 :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_xxreal_1 :::"[."::: ) "p" "," "q" ($#k1_xxreal_1 :::".]"::: ) ) -> ($#v2_rcomp_1 :::"closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: RCOMP_1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ; registration cluster ($#v1_rcomp_1 :::"compact"::: ) -> ($#v2_rcomp_1 :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ))); end; theorem :: RCOMP_1:9 (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "s1")) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ))) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "s2")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s1"))) & (Bool (Set (Var "s2")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s2"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))))) ; theorem :: RCOMP_1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) )) ; theorem :: RCOMP_1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) )) ; theorem :: RCOMP_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ; theorem :: RCOMP_1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ; theorem :: RCOMP_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ; theorem :: RCOMP_1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_rcomp_1 :::"compact"::: ) ) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )))) ; registration cluster bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() ($#v3_rcomp_1 :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ))); end; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; mode :::"Neighbourhood"::: "of" "r" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RCOMP_1:def 6 (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" "r" ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set "(" "r" ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) ")" )); end; :: deftheorem defines :::"Neighbourhood"::: RCOMP_1:def 6 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) ")" )) ")" ))); registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster -> ($#v3_rcomp_1 :::"open"::: ) for ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" "r"; end; theorem :: RCOMP_1:16 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))))) ; theorem :: RCOMP_1:17 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "N1"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "N2"))) ")" )))) ; theorem :: RCOMP_1:18 (Bool "for" (Set (Var "X")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))))) ; theorem :: RCOMP_1:19 (Bool "for" (Set (Var "X")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )))) ; theorem :: RCOMP_1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Var "r")) "st" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) )) ; theorem :: RCOMP_1:21 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool "not" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: RCOMP_1:22 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) ) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool "not" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: RCOMP_1:23 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) ) & (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" )) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )))) ; definitionlet "g" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "s" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[."::: redefine func :::"[.":::"g" "," "s":::".["::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RCOMP_1:def 7 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool "g" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) "s") ")" ) "}" ; end; :: deftheorem defines :::"[."::: RCOMP_1:def 7 : (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "g")) "," (Set (Var "s")) ($#k3_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) "}" ))); definitionlet "g" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; let "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"]."::: redefine func :::"].":::"g" "," "s":::".]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RCOMP_1:def 8 "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool "g" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) "s") ")" ) "}" ; end; :: deftheorem defines :::"]."::: RCOMP_1:def 8 : (Bool "for" (Set (Var "g")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "g")) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "r")) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" ) "}" )));