:: LOPBAN_6 semantic presentation begin theorem :: LOPBAN_6:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "s0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s0"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "y")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set (Var "s0")) ")" ))) & (Bool (Set (Set (Var "y")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set (Var "s0")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y"))) ")" ))) ; scheme :: LOPBAN_6:sch 1 RecExD3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool P1[(Set (Var "n")) "," (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))]) ")" ) ")" )) provided (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))])))) proof end; theorem :: LOPBAN_6:2 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set (Var "y1")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y1")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ")" )))))) ; theorem :: LOPBAN_6:3 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ")" )))))) ; theorem :: LOPBAN_6:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "B0")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "B0")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "B1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B0")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B1")) ")" )))))) ; theorem :: LOPBAN_6:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "a")) ($#k1_convex1 :::"*"::: ) (Set (Var "B0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_convex1 :::"*"::: ) (Set "(" (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B0")) ")" ))))))) ; theorem :: LOPBAN_6:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "x1")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "B0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1")) ")" ) ($#k5_rusub_4 :::"+"::: ) (Set "(" (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B0")) ")" ))))))) ; theorem :: LOPBAN_6:7 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V1")) "," (Set (Var "W1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "V1"))) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "W1")))) "holds" (Bool (Set (Set (Var "V")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "V1")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "W1"))))))) ; theorem :: LOPBAN_6:8 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "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 "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "V1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "x")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "V1"))))))))) ; theorem :: LOPBAN_6:9 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_convex1 :::"*"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_convex1 :::"*"::: ) (Set (Var "V1")))))))) ; theorem :: LOPBAN_6:10 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_normsp_2 :::"TopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "V1")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V1"))))))) ; theorem :: LOPBAN_6:11 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_convex1 :::"*"::: ) (Set "(" ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ")" )))))) ; theorem :: LOPBAN_6:12 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "V")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: LOPBAN_6:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_lopban_5 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )))) "holds" (Bool (Set (Var "V")) "is" ($#v1_convex1 :::"convex"::: ) )))))) ; theorem :: LOPBAN_6:14 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ))))) ; theorem :: LOPBAN_6:15 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealBanachSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "T")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "BX1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "TBX1")) "," (Set (Var "BYr")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "BYr")) ($#r1_hidden :::"="::: ) (Set ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "Y")) ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "TBX1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_lopban_5 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Num 1) ")" ")" ))) & (Bool (Set (Var "BYr")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "TBX1"))))) "holds" (Bool (Set (Var "BYr")) ($#r1_tarski :::"c="::: ) (Set (Var "TBX1"))))))))) ; theorem :: LOPBAN_6:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealBanachSpace":::) (Bool "for" (Set (Var "T")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "T1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "T1")) ($#r1_funct_2 :::"="::: ) (Set (Var "T"))) & (Bool (Set (Var "T1")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Var "T1")) "is" ($#v1_t_0topsp :::"open"::: ) )))) ;