:: BROUWER2  semantic presentation begin  



















theorem :: BROUWER2:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ) ")" )))))) ; 
 
theorem :: BROUWER2:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "u")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "u"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ))) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "w"))))) ; 
 
theorem :: BROUWER2:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Set (Var "S"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" )) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "S")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "S"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" )))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "p"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "S"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" ))  ")" )  ")" ))))) ; 
 
theorem :: BROUWER2:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" )) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool  "ex" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st" (Bool (Set (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_topreal9 :::"halfline"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) )))))) ; 
 
theorem :: BROUWER2:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set  "("  ($#k2_topreal9 :::"cl_Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" ))))) ; 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A" be   ($#v9_rltopsp1 :::"bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set "p"  ($#k5_rusub_4 :::"+"::: )  "A") ->   ($#v9_rltopsp1 :::"bounded"::: )   ; 
end; begin  
theorem :: BROUWER2:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v2_tops_1 :::"boundary"::: )  ))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k2_brouwer :::"Tdisk"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")" ))  ")" )))) ; 
 
theorem :: BROUWER2:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v2_tops_1 :::"boundary"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Bool  "not" (Set (Var "B")) "is"   ($#v2_tops_1 :::"boundary"::: )  ))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "B"))))  ")" )))) ; 
 
theorem :: BROUWER2:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v2_tops_1 :::"boundary"::: )  ))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set (Var "h")) "is"   ($#v2_abian :::"with_fixpoint"::: )  )))) ; 
 
theorem :: BROUWER2:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v2_tops_1 :::"boundary"::: )  ))) "holds"  (Bool  "for" (Set (Var "FR")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "FR")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A"))))) "holds"  (Bool  "not" (Bool (Set (Var "FR"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")))))))) ;