:: RLTOPSP1 semantic presentation begin theorem :: RLTOPSP1:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "M")))))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: RLTOPSP1:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "FX")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "FX")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "FX"))) ")" )))))) ; theorem :: RLTOPSP1:3 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))))))) ; theorem :: RLTOPSP1:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "N")) ")" ) where x "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) "}" )) "holds" (Bool (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))))) ; theorem :: RLTOPSP1:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: RLTOPSP1:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M")) ")" )))))) ; theorem :: RLTOPSP1:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M")) ")" ) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N")) ")" )))))) ; theorem :: RLTOPSP1:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "N"))))))) ; theorem :: RLTOPSP1:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))))))) ; theorem :: RLTOPSP1:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V")))))) ; theorem :: RLTOPSP1:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "V1")) ($#r1_tarski :::"c="::: ) (Set (Var "W1"))) & (Bool (Set (Var "V2")) ($#r1_tarski :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "V1")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W1")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "W2")))))) ; theorem :: RLTOPSP1:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "V2")))) "holds" (Bool (Set (Var "V1")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "V1")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V2")))))) ; theorem :: RLTOPSP1:13 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: RLTOPSP1:14 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "M")))))) ; theorem :: RLTOPSP1:15 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "M")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N")) ")" )))))) ; theorem :: RLTOPSP1:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); redefine attr "M" is :::"convex"::: means :: RLTOPSP1:def 1 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "M")) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r2_hidden :::"in"::: ) "M"))); end; :: deftheorem defines :::"convex"::: RLTOPSP1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "M"))))) ")" ))); registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k3_convex1 :::"conv"::: ) "M") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: RLTOPSP1:17 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: RLTOPSP1:18 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k3_convex1 :::"conv"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set "(" (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "M")) ")" )))))) ; theorem :: RLTOPSP1:19 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_tarski :::"c="::: ) (Set (Var "M2")))) "holds" (Bool (Set ($#k2_convex1 :::"Convex-Family"::: ) (Set (Var "M2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_convex1 :::"Convex-Family"::: ) (Set (Var "M1")))))) ; theorem :: RLTOPSP1:20 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_tarski :::"c="::: ) (Set (Var "M2")))) "holds" (Bool (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "M1"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_convex1 :::"conv"::: ) (Set (Var "M2")))))) ; theorem :: RLTOPSP1:21 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set (Var "M")))))) ; definitionlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "v", "w" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"LSeg"::: "(" "v" "," "w" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: RLTOPSP1:def 2 "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "v" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" ) ")" ) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" ; commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" ))) ; end; :: deftheorem defines :::"LSeg"::: RLTOPSP1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) where r "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" ))); registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "v", "w" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "v" "," "w" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_convex1 :::"convex"::: ) ; end; theorem :: RLTOPSP1:22 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "M")))) ")" ))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "V")); attr "P" is :::"convex-membered"::: means :: RLTOPSP1:def 3 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) )); end; :: deftheorem defines :::"convex-membered"::: RLTOPSP1:def 3 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_rltopsp1 :::"convex-membered"::: ) ) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) )) ")" ))); registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rltopsp1 :::"convex-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ")" )); end; theorem :: RLTOPSP1:23 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_rltopsp1 :::"convex-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v1_convex1 :::"convex"::: ) ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"-"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: RLTOPSP1:def 4 (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_convex1 :::"*"::: ) "A"); end; :: deftheorem defines :::"-"::: RLTOPSP1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_rltopsp1 :::"-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_convex1 :::"*"::: ) (Set (Var "A")))))); theorem :: RLTOPSP1:24 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k2_rltopsp1 :::"-"::: ) (Set (Var "M")) ")" ))) ")" )))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "A" is :::"symmetric"::: means :: RLTOPSP1:def 5 (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_rltopsp1 :::"-"::: ) "A")); end; :: deftheorem defines :::"symmetric"::: RLTOPSP1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_rltopsp1 :::"symmetric"::: ) ) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rltopsp1 :::"-"::: ) (Set (Var "A")))) ")" ))); registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rltopsp1 :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; theorem :: RLTOPSP1:25 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v2_rltopsp1 :::"symmetric"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "A" is :::"circled"::: means :: RLTOPSP1:def 6 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) "A") ($#r1_tarski :::"c="::: ) "A")); end; :: deftheorem defines :::"circled"::: RLTOPSP1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_rltopsp1 :::"circled"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" ))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_rltopsp1 :::"circled"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; theorem :: RLTOPSP1:26 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v3_rltopsp1 :::"circled"::: ) )) ; registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_rltopsp1 :::"circled"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; theorem :: RLTOPSP1:27 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) ; registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A", "B" be ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set "A" ($#k6_rusub_4 :::"+"::: ) "B") -> ($#v3_rltopsp1 :::"circled"::: ) ; end; theorem :: RLTOPSP1:28 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#v3_rltopsp1 :::"circled"::: ) -> ($#v2_rltopsp1 :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; registrationlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k3_convex1 :::"conv"::: ) "M") -> ($#v3_rltopsp1 :::"circled"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is :::"circled-membered"::: means :: RLTOPSP1:def 7 (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "V")) "is" ($#v3_rltopsp1 :::"circled"::: ) )); end; :: deftheorem defines :::"circled-membered"::: RLTOPSP1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_rltopsp1 :::"circled-membered"::: ) ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "V")) "is" ($#v3_rltopsp1 :::"circled"::: ) )) ")" ))); registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_rltopsp1 :::"circled-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ")" )); end; theorem :: RLTOPSP1:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#v4_rltopsp1 :::"circled-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v3_rltopsp1 :::"circled"::: ) ))) ; theorem :: RLTOPSP1:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#v4_rltopsp1 :::"circled-membered"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v3_rltopsp1 :::"circled"::: ) ))) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"RLTopStruct"::: -> ($#l1_rlvect_1 :::"RLSStruct"::: ) "," ($#l1_pre_topc :::"TopStruct"::: ) ; aggr :::"RLTopStruct":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult":::, :::"topology"::: #) -> ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#g1_rltopsp1 :::"RLTopStruct"::: ) "(#" "X" "," "O" "," "F" "," "G" "," "T" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rltopsp1 :::"strict"::: ) for ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; attr "X" is :::"add-continuous"::: means :: RLTOPSP1:def 8 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x2"))) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "V2"))) & (Bool (Set (Set (Var "V1")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V2"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))); attr "X" is :::"Mult-continuous"::: means :: RLTOPSP1:def 9 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_convex1 :::"*"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ) ")" )))))); end; :: deftheorem defines :::"add-continuous"::: RLTOPSP1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_rltopsp1 :::"add-continuous"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x2"))) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "V2"))) & (Bool (Set (Set (Var "V1")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "V2"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))) ")" )); :: deftheorem defines :::"Mult-continuous"::: RLTOPSP1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v7_rltopsp1 :::"Mult-continuous"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_convex1 :::"*"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ) ")" )))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v5_rltopsp1 :::"strict"::: ) ($#v6_rltopsp1 :::"add-continuous"::: ) ($#v7_rltopsp1 :::"Mult-continuous"::: ) for ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; end; definitionmode LinearTopSpace is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v6_rltopsp1 :::"add-continuous"::: ) ($#v7_rltopsp1 :::"Mult-continuous"::: ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; end; theorem :: RLTOPSP1:31 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x2"))) (Bool "ex" (Set (Var "V1")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x1"))(Bool "ex" (Set (Var "V2")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x2")) "st" (Bool (Set (Set (Var "V1")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "V2"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))))))) ; theorem :: RLTOPSP1:32 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) (Bool "ex" (Set (Var "r")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_convex1 :::"*"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))))))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"transl"::: "(" "a" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "X" means :: RLTOPSP1:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"transl"::: RLTOPSP1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_rltopsp1 :::"transl"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))))) ")" )))); theorem :: RLTOPSP1:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_rltopsp1 :::"transl"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V"))))))) ; theorem :: RLTOPSP1:34 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_rltopsp1 :::"transl"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))))) ; theorem :: RLTOPSP1:35 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_rltopsp1 :::"transl"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_rltopsp1 :::"transl"::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set (Var "X")) ")" )))) ; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k3_rltopsp1 :::"transl"::: ) "(" "a" "," "X" ")" ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) ; end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "E" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set "x" ($#k5_rusub_4 :::"+"::: ) "E") -> ($#v3_pre_topc :::"open"::: ) ; end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "E" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "K" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set "K" ($#k6_rusub_4 :::"+"::: ) "E") -> ($#v3_pre_topc :::"open"::: ) ; end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "D" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set "x" ($#k5_rusub_4 :::"+"::: ) "D") -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: RLTOPSP1:36 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "V1")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "V2"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "V1")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "V2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "V")))))) ; theorem :: RLTOPSP1:37 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V")) ")" )))))) ; theorem :: RLTOPSP1:38 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V")) ")" )))))) ; theorem :: RLTOPSP1:39 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "holds" (Bool (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x"))))))) ; theorem :: RLTOPSP1:40 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; mode local_base of "X" is ($#m1_yellow13 :::"basis"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) "X"); end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; attr "X" is :::"locally-convex"::: means :: RLTOPSP1:def 11 (Bool "ex" (Set (Var "P")) "being" ($#m1_yellow13 :::"local_base":::) "of" "X" "st" (Bool (Set (Var "P")) "is" ($#v1_rltopsp1 :::"convex-membered"::: ) )); end; :: deftheorem defines :::"locally-convex"::: RLTOPSP1:def 11 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v8_rltopsp1 :::"locally-convex"::: ) ) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "P")) "is" ($#v1_rltopsp1 :::"convex-membered"::: ) )) ")" )); definitionlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "E" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "E" is :::"bounded"::: means :: RLTOPSP1:def 12 (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) "X") (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "s")))) "holds" (Bool "E" ($#r1_tarski :::"c="::: ) (Set (Set (Var "t")) ($#k1_convex1 :::"*"::: ) (Set (Var "V")))) ")" ) ")" ))); end; :: deftheorem defines :::"bounded"::: RLTOPSP1:def 12 : (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v9_rltopsp1 :::"bounded"::: ) ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "s")))) "holds" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "t")) ($#k1_convex1 :::"*"::: ) (Set (Var "V")))) ")" ) ")" ))) ")" ))); registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v9_rltopsp1 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); cluster ($#v9_rltopsp1 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; theorem :: RLTOPSP1:41 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "V1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "V2"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: RLTOPSP1:42 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "Q")) "is" ($#v9_rltopsp1 :::"bounded"::: ) )))) ; theorem :: RLTOPSP1:43 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "P")) where P "is" ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool verum) "}" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v9_rltopsp1 :::"bounded"::: ) ))) ; theorem :: RLTOPSP1:44 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "U")) where U "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) : (Bool verum) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X"))))) ; theorem :: RLTOPSP1:45 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "O")) "being" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "U")) ")" ) where a "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")), U "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#m2_yellow13 :::"basis"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; let "r" be ($#m1_subset_1 :::"Real":::); func :::"mlt"::: "(" "r" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "X" means :: RLTOPSP1:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "r" ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"mlt"::: RLTOPSP1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_rltopsp1 :::"mlt"::: ) "(" (Set (Var "r")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))))) ")" )))); theorem :: RLTOPSP1:46 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rltopsp1 :::"RLTopStruct"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_rltopsp1 :::"mlt"::: ) "(" (Set (Var "r")) "," (Set (Var "X")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))))))) ; theorem :: RLTOPSP1:47 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_rltopsp1 :::"mlt"::: ) "(" (Set (Var "r")) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))))) ; theorem :: RLTOPSP1:48 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_rltopsp1 :::"mlt"::: ) "(" (Set (Var "r")) "," (Set (Var "X")) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_rltopsp1 :::"mlt"::: ) "(" (Set "(" (Set (Var "r")) ($#k2_real_1 :::"""::: ) ")" ) "," (Set (Var "X")) ")" )))) ; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "r" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k4_rltopsp1 :::"mlt"::: ) "(" "r" "," "X" ")" ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) ; end; theorem :: RLTOPSP1:49 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: RLTOPSP1:50 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))) "is" ($#v4_pre_topc :::"closed"::: ) )))) ; theorem :: RLTOPSP1:51 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V")) ")" )))))) ; theorem :: RLTOPSP1:52 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "A")) ")" )))))) ; theorem :: RLTOPSP1:53 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k1_convex1 :::"*"::: ) (Set (Var "A")) ")" ))))) ; theorem :: RLTOPSP1:54 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")))))))) ; theorem :: RLTOPSP1:55 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "for" (Set (Var "r")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "V" be ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "r" be ($#m1_subset_1 :::"Real":::); cluster (Set "r" ($#k1_convex1 :::"*"::: ) "V") -> ($#v9_rltopsp1 :::"bounded"::: ) ; end; theorem :: RLTOPSP1:56 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "U")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "U")) "is" ($#v2_rltopsp1 :::"symmetric"::: ) ) & (Bool (Set (Set (Var "U")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "U"))) ($#r1_tarski :::"c="::: ) (Set (Var "W"))) ")" )))) ; theorem :: RLTOPSP1:57 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "K")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool (Set (Set (Var "K")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "V"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "C")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "V")))))))) ; theorem :: RLTOPSP1:58 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ))))) ; theorem :: RLTOPSP1:59 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Var "V")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v7_pre_topc :::"T_1"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v6_rltopsp1 :::"add-continuous"::: ) ($#v7_rltopsp1 :::"Mult-continuous"::: ) -> ($#v8_pre_topc :::"Hausdorff"::: ) for ($#l1_rltopsp1 :::"RLTopStruct"::: ) ; end; theorem :: RLTOPSP1:60 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "A")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "V")) ")" ) where V "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) : (Bool verum) "}" )))) ; theorem :: RLTOPSP1:61 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RLTOPSP1:62 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "B")) ")" ))))) ; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "C" be ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "C") -> ($#v1_convex1 :::"convex"::: ) ; end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "C" be ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "C") -> ($#v1_convex1 :::"convex"::: ) ; end; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "B" be ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "B") -> ($#v3_rltopsp1 :::"circled"::: ) ; end; theorem :: RLTOPSP1:63 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#v3_rltopsp1 :::"circled"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) "is" ($#v3_rltopsp1 :::"circled"::: ) ))) ; registrationlet "X" be ($#l1_rltopsp1 :::"LinearTopSpace":::); let "E" be ($#v9_rltopsp1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "E") -> ($#v9_rltopsp1 :::"bounded"::: ) ; end; theorem :: RLTOPSP1:64 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_rltopsp1 :::"circled"::: ) ) & (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" )))) ; theorem :: RLTOPSP1:65 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "for" (Set (Var "U")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "U")) "is" ($#v1_convex1 :::"convex"::: ) )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_rltopsp1 :::"circled"::: ) ) & (Bool (Set (Var "W")) "is" ($#v1_convex1 :::"convex"::: ) ) & (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" )))) ; theorem :: RLTOPSP1:66 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) (Bool "ex" (Set (Var "P")) "being" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "P")) "is" ($#v4_rltopsp1 :::"circled-membered"::: ) ))) ; theorem :: RLTOPSP1:67 (Bool "for" (Set (Var "X")) "being" ($#l1_rltopsp1 :::"LinearTopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v8_rltopsp1 :::"locally-convex"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_yellow13 :::"local_base":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "P")) "is" ($#v1_rltopsp1 :::"convex-membered"::: ) ))) ; begin theorem :: RLTOPSP1:68 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))) ; theorem :: RLTOPSP1:69 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))) ; theorem :: RLTOPSP1:70 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: RLTOPSP1:71 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")))) "or" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))) ")" )))) ;