:: Continuity of Bounded Linear Operators on Normed Linear Spaces :: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama :: :: Received September 29, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1, SUBSET_1, RELAT_1, LOPBAN_1, MSSUBFAM, TARSKI, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, NFCONT_1, NFCONT_2, DUALSP01, FUNCT_5, UNIALG_1, FUNCOP_1, SEQ_4, XXREAL_2, XXREAL_0, XBOOLE_0, RLVECT_1, CFCONT_1, REWRITE1, METRIC_1, COMPLEX1, TOPS_1, LOPBAN_8; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_5, BINOP_1, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQ_4, STRUCT_0, PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1, NORMSP_3, LOPBAN_1, LOPBAN_5, NFCONT_1, NFCONT_2, PRVECT_3, DUALSP01; constructors SEQ_2, SEQ_4, NFCONT_1, NFCONT_2, COMSEQ_2, RELSET_1, NAT_D, RSSPACE3, NDIFF_7, REALSET1, NORMSP_3, LOPBAN_5; registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1, LOPBAN_1, PRVECT_3, NORMSP_0, NAT_1, NORMSP_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TARSKI; equalities RLVECT_1, LOPBAN_1, NORMSP_0, BINOP_1, PRVECT_3, LOPBAN_5; expansions NFCONT_1; theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, FUNCT_1, FUNCT_2, ORDINAL1, LOPBAN_1, PARTFUN1, NFCONT_1, VECTSP_1, SEQ_2, COMPLEX1, XXREAL_0, XCMPLX_1, NORMSP_0, PRVECT_3, LOPBAN_3, RLVECT_4, NFCONT_2, NDIFF_8, FUNCOP_1, NORMSP_1, NORMSP_3, DUALSP01, SEQ_4, FUNCT_5, INTEGR20, VALUED_1, XREAL_1, LOPBAN_2, LOPBAN_7; schemes FUNCT_2, INTEGR20; begin :: Uniform Continuity and Lipschitz Continuity of :: Bounded Linear Operators reserve S,T,W,Y for RealNormSpace; reserve f,f1,f2 for PartFunc of S,T; reserve Z for Subset of S; reserve i,n for Nat; theorem Th020: for E,F be RealNormSpace, E1 be Subset of E, f be PartFunc of E,F st E1 is dense & F is complete & dom f = E1 & f is_uniformly_continuous_on E1 holds (ex g be Function of E,F st g|E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x be Point of E holds ex seq be sequence of E st rng seq c= E1 & seq is convergent & lim seq = x & f/*seq is convergent & g.x = lim f/*seq ) & ( for x be Point of E, seq be sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds f/*seq is convergent & g.x = lim f/*seq ) ) & (for g1,g2 be Function of E,F st g1|E1 = f & g1 is_continuous_on the carrier of E & g2|E1 = f & g2 is_continuous_on the carrier of E holds g1 = g2) proof let E,F be RealNormSpace, E1 be Subset of E, f be PartFunc of E,F; assume that A1: E1 is dense and A2: F is complete and A3: dom f = E1 and A4: f is_uniformly_continuous_on E1; A6: for x be Point of E, seq be sequence of E st rng seq c= E1 & seq is convergent holds for s being Real st 0 < s holds ex n being Nat st for m being Nat st n <= m holds ||.(((f/*seq) . m) - ((f/*seq) . n)).|| < s proof let x be Point of E, seq be sequence of E; assume that A7: rng seq c= E1 and A8: seq is convergent; set fseq = f/*seq; let r be Real; assume 0 < r; then consider s being Real such that A10: 0 < s & for x1, x2 being Point of E st x1 in E1 & x2 in E1 & ||.x1 - x2.|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A4,NFCONT_2:def 1; consider n being Nat such that A11: for m being Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < s by A8,A10,LOPBAN_3:4; take n; let m be Nat; assume n <= m; then A13: ||.((seq . m) - (seq . n)).|| < s by A11; A14: n in NAT & m in NAT by ORDINAL1:def 12; B14: seq . m in rng seq & seq . n in rng seq by FUNCT_2:4,ORDINAL1:def 12; f /. (seq.m) = fseq.m & f /. (seq.n) = fseq.n by A3,A7,A14,FUNCT_2:109; hence ||.fseq. m - fseq.n.|| < r by A7,A10,A13,B14; end; A16: for x be Point of E, seq be sequence of E st rng seq c= E1 & seq is convergent holds f/*seq is convergent proof let x be Point of E, seq be sequence of E; assume that A17: rng seq c= E1 and A18: seq is convergent; for s being Real st 0 < s holds ex n being Nat st for m being Nat st n <= m holds ||.(((f/*seq) . m) - ((f/*seq) . n)).|| < s by A6,A17,A18; hence thesis by A2,LOPBAN_1:def 15,LOPBAN_3:5; end; A19: for x be Point of E, seq1,seq2 be sequence of E st rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & rng seq2 c= E1 & seq2 is convergent & lim seq2 = x holds lim (f/*seq1) = lim (f/*seq2) proof let x be Point of E, seq1,seq2 be sequence of E; assume that A20: rng seq1 c= E1 & seq1 is convergent & lim seq1 = x and A21: rng seq2 c= E1 & seq2 is convergent & lim seq2 = x; deffunc F2(Nat) = seq1.$1; deffunc F3(Nat) = seq2.$1; consider s being sequence of the carrier of E such that A22: for n being Nat holds s . (2 * n) = F2(n) & s . ((2 * n) + 1) = F3(n) from INTEGR20:sch 1; B23: now let y be object; assume y in rng s; then consider i be object such that A23: i in NAT & y=s.i by FUNCT_2:11; reconsider i as Nat by A23; consider k be Nat such that A24: i=2*k or i=2*k+1 by INTEGR20:14; reconsider k1=k, i1=i as Element of NAT by ORDINAL1:def 12; per cases by A24; suppose i = 2*k1; then s.i = seq1.k1 by A22; then s.i in rng seq1 by FUNCT_2:4; hence y in E1 by A20,A23; end; suppose i = 2*k1+1; then s.i = seq2.k1 by A22; then s.i in rng seq2 by FUNCT_2:4; hence y in E1 by A21,A23; end; end; then A28: rng s c= E1 by TARSKI:def 3; now let p be Real; assume A30: 0 < p; then consider n1 be Nat such that A31: for m be Nat st n1 <= m holds ||. seq1.m - x .|| < p by A20,NORMSP_1:def 7; consider n2 be Nat such that A32: for m be Nat st n2 <= m holds ||. seq2.m - x .||
x as sequence of E; for n be Nat holds seq1.n = x by FUNCOP_1:7,ORDINAL1:def 12; then A56: seq1 is convergent & lim seq1 = x by NORMSP_3:23; A58: rng seq1 c= E1 proof let y be object; assume y in rng seq1; then consider i be object such that A57: i in NAT & y=seq1.i by FUNCT_2:11; reconsider i as Nat by A57; thus y in E1 by A54,A57,FUNCOP_1:7; end; then f /* seq1 is convergent & lim f/*seq1 = f/. (lim seq1) by A52,A54,A56,NFCONT_1:18; then A59: lim f/*seq1 =f.x by A53,A56,PARTFUN1:def 6; consider seq2 be sequence of E such that A60: rng seq2 c= E1 & seq2 is convergent & lim seq2 = x & f/*seq2 is convergent & g.x= lim (f/*seq2) by A49; thus thesis by A19,A56,A58,A59,A60; end; then A61: g|E1 = f by A51,FUNCT_1:46; A62: for x be Point of E, seq be sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds f/*seq is convergent & g.x = lim f/*seq proof let x be Point of E, seq be sequence of E; assume A63: rng seq c= E1 & seq is convergent & lim seq = x; consider seq1 be sequence of E such that A64: rng seq1 c= E1 & seq1 is convergent & lim seq1 = x & f/*seq1 is convergent & g.x = lim f/*seq1 by A49; thus f/*seq is convergent by A16,A63; thus thesis by A19,A63,A64; end; for r being Real st 0 < r holds ex s being Real st 0 < s & for x1, x2 being Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.x1 - x2.|| < s holds ||.g /. x1 - g/. x2.|| < r proof let r0 be Real; assume A65: 0 < r0; set r1 = r0/2; A66: 0 < r1 & r1 < r0 by A65,XREAL_1:215,216; set r = r1/3; A67: 0 < r & r < r1 by A66,XREAL_1:221,222; consider s0 being Real such that A68: 0 < s0 & for x1, x2 being Point of E st x1 in E1& x2 in E1 & ||.x1 - x2.|| < s0 holds ||.f /. x1 - f/. x2.|| < r by A4,A66,NFCONT_2:def 1,XREAL_1:222; set s = s0/3; A69: 0 < s & s < s0 by A68,XREAL_1:221,222; take s; thus 0 < s by A68,XREAL_1:222; let x1, x2 be Point of E; assume A70: x1 in the carrier of E & x2 in the carrier of E & ||.x1 - x2.|| < s; consider seq1 be sequence of E such that A71: rng seq1 c= E1 & seq1 is convergent & lim seq1 = x1 & f/*seq1 is convergent & g.x1 = lim f/*seq1 by A49; consider M10 being Nat such that A72: for n being Nat st M10 <= n holds ||. seq1.n - x1.|| < s by A69,A71,NORMSP_1:def 7; consider M11 being Nat such that A73: for n being Nat st M11 <= n holds ||. (f/*seq1).n - g.x1.|| < r by A67,A71,NORMSP_1:def 7; set M1 = M10 + M11; A74: M10 + 0 <= M1 & M11 + 0 <= M1 by XREAL_1:7; consider seq2 be sequence of E such that A75: rng seq2 c= E1 & seq2 is convergent & lim seq2 = x2 & f/*seq2 is convergent & g.x2 = lim f/*seq2 by A49; consider M20 being Nat such that A76: for n being Nat st M20 <= n holds ||. seq2.n - x2.|| < s by A69,A75,NORMSP_1:def 7; consider M21 being Nat such that A77: for n being Nat st M21 <= n holds ||. (f/*seq2).n - g.x2.|| < r by A67,A75,NORMSP_1:def 7; set M2 = M20 + M21; A78: M20 + 0 <= M2 & M21 + 0 <= M2 by XREAL_1:7; set n = M1 + M2; A82: ||. seq1.n - x1.|| < s & ||. (f/*seq1).n - g.x1.|| < r by A72,A73,A74,XREAL_1:7; A83: ||. seq2.n - x2.|| < s & ||. (f/*seq2).n - g.x2.|| < r by A76,A77,A78,XREAL_1:7; seq2.n - seq1.n = seq2.n - x2 + x2 - seq1.n by RLVECT_4:1 .= ( seq2.n - x2 ) + ( x2-x1 + x1) - seq1.n by RLVECT_4:1 .= ( seq2.n - x2 ) + ( x2-x1 ) + x1 - seq1.n by RLVECT_1:def 3 .= ( seq2.n - x2 ) + ( x2-x1) + ( x1 - seq1.n ) by RLVECT_1:28; then A84: ||. seq2.n - seq1.n.|| <= ||. ( seq2.n - x2 ) + ( x2-x1 ) .|| + ||. x1 - seq1.n .|| by NORMSP_1:def 1; ||. ( seq2.n - x2 ) + ( x2-x1 ) .|| <= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| by NORMSP_1:def 1; then ||. ( seq2.n - x2 ) + ( x2-x1 ) .|| + ||. x1 - seq1.n .|| <= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| + ||. x1 - seq1.n .|| by XREAL_1:7; then A85: ||. seq2.n - seq1.n.|| <= ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| + ||. x1 - seq1.n .|| by A84,XXREAL_0:2; ||. x2-x1 .|| < s by A70,NORMSP_1:7; then A86: ||. ( seq2.n - x2 ).|| + ||. x2-x1 .|| < s+s by A83,XREAL_1:8; ||. x1 - seq1.n .|| < s by A82,NORMSP_1:7; then ||. ( seq2.n - x2 ).|| + ||. x2-x1 .||+ ||. x1 - seq1.n .|| < s+s+s by A86,XREAL_1:8; then ||. seq2.n - seq1.n.|| < s+s+s by A85,XXREAL_0:2; then A87: ||. seq1.n - seq2.n.|| < s + s+ s by NORMSP_1:7; A88: n in NAT by ORDINAL1:def 12; seq2.n in rng seq2 & seq1.n in rng seq1 by FUNCT_2:4,ORDINAL1:def 12; then A89: ||.f /. (seq1.n) - f/. (seq2.n).|| < r by A68,A71,A75,A87; g /. x1 - g/. x2 = g /. x1 - f /. (seq1.n) + f /. (seq1.n) - g/. x2 by RLVECT_4:1 .= (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) + f /. (seq2.n) ) - g/. x2 by RLVECT_4:1 .= (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) + f /. (seq2.n) - g/. x2 by RLVECT_1:def 3 .= (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) + ( f /. (seq2.n) - g/. x2 ) by RLVECT_1:28; then A90: ||.g /. x1 - g/. x2.|| <= ||. (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) .|| + ||. f /. (seq2.n) - g/. x2 .|| by NORMSP_1:def 1; ||. (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) .|| <= ||. g /. x1 - f /. (seq1.n) .|| + ||. f /. (seq1.n) - f /. (seq2.n) .|| by NORMSP_1:def 1; then ||. (g /. x1 - f /. (seq1.n)) + ( f /. (seq1.n) - f /. (seq2.n) ) .|| + ||. f /. (seq2.n) - g/. x2 .|| <= ||. g /. x1 - f /. (seq1.n) .|| + ||. f /. (seq1.n) - f /. (seq2.n) .|| + ||. f /. (seq2.n) - g/. x2 .|| by XREAL_1:7; then A91: ||.g /. x1 - g/. x2.|| <= ||. g /. x1 - f /. (seq1.n) .|| + ||. f /. (seq1.n) - f /. (seq2.n) .|| + ||. f /. (seq2.n) - g/. x2 .|| by A90,XXREAL_0:2; A92: ||. g /. x1 - f /. (seq1.n) .|| = ||. f /. (seq1.n) - g . x1 .|| by NORMSP_1:7 .= ||. (f/*seq1).n - g . x1 .|| by A3,A71,A88,FUNCT_2:109; A93: ||. f /. (seq2.n) - g/. x2 .|| = ||. (f/*seq2).n - g . x2 .|| by A3,A75,A88,FUNCT_2:109; ||. g /. x1 - f /. (seq1.n) .|| + ||. f /. (seq1.n) - f /. (seq2.n) .|| <= r+r by A82,A89,A92,XREAL_1:7; then ||. g /. x1 - f /. (seq1.n) .|| + ||. f /. (seq1.n) - f /. (seq2.n) .|| + ||. f /. (seq2.n) - g/. x2 .|| < r+r+r by A83,A93,XREAL_1:8; then ||.g /. x1 - g/. x2.|| < r+r+r by A91,XXREAL_0:2; hence ||.g /. x1 - g/. x2.|| < r0 by A66,XXREAL_0:2; end; hence ex g be Function of E,F st g | E1 = f & g is_uniformly_continuous_on the carrier of E & ( for x be Point of E holds ex seq be sequence of E st rng seq c= E1 & seq is convergent & lim seq = x & f/*seq is convergent & g.x = lim f/*seq ) & ( for x be Point of E, seq be sequence of E st rng seq c= E1 & seq is convergent & lim seq = x holds f/*seq is convergent & g.x = lim f/*seq ) by A49,A50,A61,A62,NFCONT_2:def 1; let g1,g2 be Function of E,F such that A95: g1|E1 = f & g1 is_continuous_on the carrier of E and A96: g2|E1 = f & g2 is_continuous_on the carrier of E; for x being Element of E holds g1 . x = g2.x proof let x be Element of E; consider seq being sequence of E such that A97: rng seq c= E1 & seq is convergent & lim seq = x by A1,NORMSP_3:14; A106: g1/*seq = f/*seq by A3,A95,A97,FUNCT_2:117 .= g2/*seq by A3,A96,A97,FUNCT_2:117; thus g1.x = g1/. (lim seq) by A97 .= lim g2/*seq by A95,A97,A106,NFCONT_1:18 .= g2/.x by A96,A97,NFCONT_1:18 .= g2.x; end; hence g1 = g2 by FUNCT_2:def 8; end; theorem for E,F,G be RealNormSpace, f be Point of R_NormSpace_of_BoundedLinearOperators (E,F), g be Point of R_NormSpace_of_BoundedLinearOperators (F,G) holds ex h be Point of R_NormSpace_of_BoundedLinearOperators (E,G) st h = g*f & ||.h.|| <= ||.g.||*||.f.|| proof let E,F,G be RealNormSpace, f be Point of R_NormSpace_of_BoundedLinearOperators (E,F), g be Point of R_NormSpace_of_BoundedLinearOperators (F,G); reconsider Lf=f as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9; reconsider Lg=g as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9; set Lh = Lg*Lf; reconsider Lh as Lipschitzian LinearOperator of E,G by LOPBAN_2:2; reconsider h = Lh as Point of R_NormSpace_of_BoundedLinearOperators (E,G) by LOPBAN_1:def 9; take h; thus h = g * f; A8: ||.h.|| = upper_bound (PreNorms(modetrans(h,E,G))) by LOPBAN_1:def 13 .= upper_bound PreNorms(Lh) by LOPBAN_1:29; for t be Real st t in PreNorms(Lh) holds t <= ||.g.|| * ||.f.|| proof let t be Real; assume t in PreNorms(Lh); then consider w be Point of E such that A9: t = ||. Lh.w .|| & ||.w.|| <= 1; A10: ||. Lh.w .|| = ||.Lg.(Lf.w).|| by FUNCT_2:15; A11: ||. Lf.w .|| <= ||.f.|| * ||.w.|| by LOPBAN_1:32; ||.f.|| * ||.w.|| <= ||.f.|| * 1 by A9,XREAL_1:64; then A12: ||. Lf.w .|| <= ||.f.|| by A11,XXREAL_0:2; A13: ||.Lg. (Lf.w) .|| <= ||.g.|| * ||. (Lf.w) .|| by LOPBAN_1:32; ||.g.|| * ||. (Lf.w) .|| <= ||.g.|| * ||.f.|| by A12,XREAL_1:64; hence thesis by A9,A10,A13,XXREAL_0:2; end; hence ||.h.|| <= ||.g.|| * ||.f.|| by A8,SEQ_4:45; end; theorem LMCONT1: for E,F be RealNormSpace, L be Lipschitzian LinearOperator of E,F holds L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E proof let E,F be RealNormSpace, L be Lipschitzian LinearOperator of E,F; consider K being Real such that A2: 0 <= K & for x being VECTOR of E holds ||. L.x.|| <= K * ||.x.|| by LOPBAN_1:def 8; set r = K+1; A3: K + 0 < r by XREAL_1:8; set E0 = the carrier of E; for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds ||.L/. x1 - L/. x2.|| <= r * ||. x1 -x2.|| proof let x1, x2 be Point of E; L/.x1 - L/.x2 = L.x1+(-1)*(L.x2) by RLVECT_1:16 .= L.x1+L. ((-1)*x2) by LOPBAN_1:def 5 .= L.(x1+(-1)*x2) by VECTSP_1:def 20 .= L.(x1-x2) by RLVECT_1:16; then A8: ||.L/. x1 - L/. x2.|| <= K * ||.x1-x2.|| by A2; K * ||.x1-x2.|| <= r * ||.x1-x2.|| by A3,XREAL_1:64; hence thesis by A8,XXREAL_0:2; end; hence L is_Lipschitzian_on E0 by A2,FUNCT_2:def 1; hence L is_uniformly_continuous_on E0 by NFCONT_2:9; end; theorem for E,F be RealNormSpace, E1 be SubRealNormSpace of E, f be Point of R_NormSpace_of_BoundedLinearOperators (E1,F) st F is complete & ex E0 be Subset of E st E0 = the carrier of E1 & E0 is dense holds (ex g be Point of R_NormSpace_of_BoundedLinearOperators (E,F) st dom g = the carrier of E & g| the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf be PartFunc of E,F st Lf = f & (for x be Point of E holds ex seq be sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf/*seq is convergent & g.x = lim Lf/*seq) & (for x be Point of E, seq be sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds Lf/*seq is convergent & g.x = lim Lf/*seq) ) & (for g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F) st g1| the carrier of E1 = f & g2| the carrier of E1 = f holds g1 = g2) proof let E,F be RealNormSpace, E1 be SubRealNormSpace of E, f be Point of R_NormSpace_of_BoundedLinearOperators (E1,F); assume that A1: F is complete and A2: ex E0 be Subset of E st E0 = the carrier of E1 & E0 is dense; consider E0 be Subset of E such that A3: E0 = the carrier of E1 & E0 is dense by A2; reconsider L = f as Lipschitzian LinearOperator of E1,F by LOPBAN_1:def 9; A4: dom L = the carrier of E1 & rng L c= the carrier of F by FUNCT_2:def 1; then L in PFuncs (the carrier of E,the carrier of F) by A3,PARTFUN1:def 3; then reconsider Lf = L as PartFunc of E,F by PARTFUN1:46; A5: dom Lf = E0 by A3,FUNCT_2:def 1; consider K being Real such that A6: 0 <= K & for x being VECTOR of E1 holds ||. L.x.|| <= K * ||.x.|| by LOPBAN_1:def 8; set r = K+1; A7: K + 0 < r by XREAL_1:8; for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds ||.Lf/. x1 - Lf/. x2.|| <= r * ||. x1 -x2.|| proof let x1, x2 be Point of E; assume x1 in E0 & x2 in E0; then reconsider xx1 = x1, xx2 = x2 as Point of E1 by A3; A10: (-1)*x2 =(-1)*xx2 by NORMSP_3:28; A11: x1-x2 = x1+ (-1)*x2 by RLVECT_1:16 .= xx1+(-1)*xx2 by A10,NORMSP_3:28 .= xx1 -xx2 by RLVECT_1:16; A12: Lf/.x1 = L.xx1 by A4,PARTFUN1:def 6; Lf/.x2 = L.xx2 by A4,PARTFUN1:def 6; then Lf/.x1 - Lf/.x2 = L.xx1+(-1)*(L.xx2) by A12,RLVECT_1:16 .= L.xx1+L. ((-1)*xx2) by LOPBAN_1:def 5 .= L.(xx1+(-1)*xx2) by VECTSP_1:def 20 .= L.(xx1-xx2) by RLVECT_1:16; then ||.Lf/. x1 - Lf/. x2.|| <= K * ||.xx1-xx2.|| by A6; then A14: ||.Lf/. x1 - Lf/. x2.|| <= K * ||.x1-x2.|| by A11,NORMSP_3:28; K * ||.x1-x2.|| <= r * ||.x1-x2.|| by A7,XREAL_1:64; hence thesis by A14,XXREAL_0:2; end; then Lf is_Lipschitzian_on E0 by A3,A6,FUNCT_2:def 1; then A15: Lf is_uniformly_continuous_on E0 by NFCONT_2:9; A16: (ex Pg be Function of E,F st Pg|E0 = Lf & Pg is_uniformly_continuous_on the carrier of E & (for x be Point of E holds ex seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x & Lf/*seq is convergent & Pg.x = lim Lf/*seq) & (for x be Point of E, seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds Lf/*seq is convergent & Pg.x = lim Lf/*seq ) ) & (for Pg1,Pg2 be Function of E,F st Pg1|E0 = Lf & Pg1 is_continuous_on the carrier of E & Pg2|E0 = Lf & Pg2 is_continuous_on the carrier of E holds Pg1 = Pg2) by A1,A3,A5,A15,Th020; consider Pg be Function of E,F such that A17: Pg|E0 = Lf and A18: Pg is_uniformly_continuous_on the carrier of E and A19: for x be Point of E holds ex seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x & Lf/*seq is convergent & Pg.x = lim Lf/*seq and A20: for x be Point of E, seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds Lf/*seq is convergent & Pg.x = lim Lf/*seq and A21: for x be Point of E holds ex seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x & Lf/*seq is convergent & Pg.x = lim Lf/*seq and A22: for x be Point of E, seq be sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds Lf/*seq is convergent & Pg.x = lim Lf/*seq by A16; A23: for x,y be Point of E holds Pg.(x+y) = Pg.x + Pg.y proof let x,y be Point of E; consider xseq be sequence of E such that A24: rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf/*xseq is convergent & Pg.x = lim Lf/*xseq by A19; consider yseq be sequence of E such that A25: rng yseq c= E0 & yseq is convergent & lim yseq = y & Lf/*yseq is convergent & Pg.y = lim Lf/*yseq by A19; A29: rng (xseq + yseq) c= E0 proof let y be object; assume y in rng (xseq+yseq); then consider n be Element of NAT such that A26: y = (xseq+yseq).n by FUNCT_2:113; xseq.n in rng xseq & yseq.n in rng yseq by FUNCT_2:4; then reconsider xn = xseq.n, yn = yseq.n as Point of E1 by A3,A24,A25; xseq.n + yseq.n = xn+yn by NORMSP_3:28; then xseq.n + yseq.n in E0 by A3; hence y in E0 by A26,NORMSP_1:def 2; end; A30: xseq + yseq is convergent by A24,A25,NORMSP_1:19; A31: lim (xseq + yseq) = x+y by A24,A25,NORMSP_1:25; A32: rng (xseq + yseq) c= dom Lf by A3,A29,FUNCT_2:def 1; A33: rng xseq c= dom Lf by A3,A24,FUNCT_2:def 1; A34: rng yseq c= dom Lf by A3,A25,FUNCT_2:def 1; B34: for n be Nat holds (Lf/*(xseq+yseq)).n = (Lf/*xseq).n + (Lf/*yseq).n proof let n be Nat; A35: n in NAT by ORDINAL1:def 12; xseq.n in rng xseq & yseq.n in rng yseq by FUNCT_2:4,ORDINAL1:def 12; then reconsider xn = xseq.n, yn = yseq.n as Point of E1 by A3,A24,A25; A37: xseq.n + yseq.n = xn + yn by NORMSP_3:28; then xseq.n + yseq.n in the carrier of E1; then A39: xseq.n + yseq.n in dom L by FUNCT_2:def 1; thus (Lf/*(xseq+yseq)).n = Lf/.((xseq+yseq).n) by A32,A35,FUNCT_2:109 .= Lf/.(xseq.n+yseq.n) by NORMSP_1:def 2 .= L.(xn+yn) by A37,A39,PARTFUN1:def 6 .= L/.xn + L/.yn by VECTSP_1:def 20 .= (Lf/*xseq).n + Lf/.(yseq.n) by A33,A35,FUNCT_2:109 .= (Lf/*xseq).n + (Lf/*yseq).n by A34,A35,FUNCT_2:109; end; A41: lim Lf/*(xseq +yseq) = lim (Lf/*xseq + Lf/*yseq) by B34,NORMSP_1:def 2 .= lim Lf/*xseq +lim Lf/*yseq by A24,A25,NORMSP_1:25; thus Pg.(x+y) = Pg.x + Pg.y by A20,A24,A25,A29,A30,A31,A41; end; for x be Point of E, a be Real holds Pg.(a*x) = a* Pg.x proof let x be Point of E, a be Real; consider xseq be sequence of E such that A42: rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf/*xseq is convergent & Pg.x = lim Lf/*xseq by A19; A46: rng (a*xseq) c= E0 proof let y be object; assume y in rng (a*xseq); then consider n be Element of NAT such that A43: y = (a*xseq).n by FUNCT_2:113; xseq.n in rng xseq by FUNCT_2:4; then reconsider xn = xseq.n as Point of E1 by A3,A42; a*xseq.n = a*xn by NORMSP_3:28; then a*xseq.n in E0 by A3; hence y in E0 by A43,NORMSP_1:def 5; end; A47: a*xseq is convergent by A42,NORMSP_1:22; A48: lim (a*xseq) = a*x by A42,NORMSP_1:28; A49: rng (a*xseq) c= dom Lf by A3,A46,FUNCT_2:def 1; A50: rng xseq c= dom Lf by A3,A42,FUNCT_2:def 1; B50: for n be Nat holds (Lf/*(a*xseq)).n = a*(Lf/*xseq).n proof let n be Nat; A51: n in NAT by ORDINAL1:def 12; xseq.n in rng xseq by FUNCT_2:4,ORDINAL1:def 12; then reconsider xn=xseq.n as Point of E1 by A3,A42; A53: a*xseq.n = a*xn by NORMSP_3:28; then a*xseq.n in the carrier of E1; then A55: a*xseq.n in dom L by FUNCT_2:def 1; thus (Lf/*((a*xseq))).n = Lf/.(((a*xseq)).n) by A49,A51,FUNCT_2:109 .= Lf/.(a*xseq.n) by NORMSP_1:def 5 .= L.(a*xn) by A53,A55,PARTFUN1:def 6 .= a * L/.xn by LOPBAN_1:def 5 .= a * (Lf/*xseq).n by A50,A51,FUNCT_2:109; end; lim Lf/*((a*xseq)) = lim (a*(Lf/*xseq)) by B50,NORMSP_1:def 5 .= a* lim Lf/*xseq by A42,NORMSP_1:28; hence Pg.(a*x) = a * Pg.x by A20,A42,A46,A47,A48; end; then reconsider Pg as LinearOperator of E,F by A23,LOPBAN_1:def 5,VECTSP_1:def 20; reconsider Pg as Lipschitzian LinearOperator of E,F by A18,NFCONT_2:7,LOPBAN_7:6; reconsider g = Pg as Point of R_NormSpace_of_BoundedLinearOperators (E,F) by LOPBAN_1:def 9; A58: dom g = the carrier of E by FUNCT_2:def 1; A61: ||.f.|| = upper_bound (PreNorms(modetrans(f,E1,F))) by LOPBAN_1:def 13 .= upper_bound PreNorms(L) by LOPBAN_1:29; A63: ||.g.|| = upper_bound (PreNorms(modetrans(g,E,F))) by LOPBAN_1:def 13 .= upper_bound PreNorms(Pg) by LOPBAN_1:29; for t be Real st t in PreNorms(L) holds t <= ||.g.|| proof let t be Real; assume t in PreNorms(L); then consider w be Point of E1 such that A64: t = ||. L.w .|| & ||.w.|| <= 1; A65: the carrier of E1 c= the carrier of E by DUALSP01:def 16; w in the carrier of E1; then reconsider w1 = w as Point of E by A65; A67: ||.w1.|| <= 1 by A64,NORMSP_3:28; A68: not PreNorms(Pg) is empty & PreNorms(Pg) is bounded_above by LOPBAN_1:27; L.w = Pg.w1 by A3,A17,FUNCT_1:49; then t in PreNorms(Pg) by A64,A67; hence t <= ||.g.|| by A63,A68,SEQ_4:def 1; end; then A69: ||.f.|| <= ||.g.|| by A61,SEQ_4:45; for t be Real st t in PreNorms(Pg) holds t <= ||.f.|| proof let t be Real; assume t in PreNorms(Pg); then consider x be Point of E such that A70: t = ||. Pg.x .|| & ||.x.|| <= 1; consider xseq be sequence of E such that A71: rng xseq c= E0 & xseq is convergent & lim xseq = x & Lf/*xseq is convergent & Pg.x = lim Lf/*xseq by A19; A72: ||. Pg.x .|| = lim ||.Lf/*xseq.|| by A71,LOPBAN_1:20; A73: ||.xseq.|| is convergent & lim ||.xseq.|| = ||. lim xseq.|| by A71,LOPBAN_1:20; A74: ||.Lf/*xseq.|| is convergent by A71,NORMSP_1:23; A75: ||.f.|| (#) ||.xseq.|| is convergent by A71,LOPBAN_1:20,SEQ_2:7; for n be Nat holds ||.Lf/*xseq.|| .n <= ( ||.f.|| (#) ||.xseq.||) .n proof let n be Nat; A77: n in NAT by ORDINAL1:def 12; A78: rng xseq c= dom Lf by A3,A71,FUNCT_2:def 1; xseq.n in rng xseq by FUNCT_2:4,ORDINAL1:def 12; then reconsider xn = xseq.n as Point of E1 by A3,A71; A80: dom Lf = the carrier of E1 by FUNCT_2:def 1; A81: ||.Lf/*xseq.|| .n = ||. (Lf/*xseq).n .|| by NORMSP_0:def 4 .= ||. Lf/.(xseq.n) .|| by A77,A78,FUNCT_2:109 .= ||. L.xn .|| by A80,PARTFUN1:def 6; ||. L.xn .|| <= ||.f.|| * ||.xn.|| by LOPBAN_1:32; then ||. L.xn .|| <= ||.f.|| * ||.xseq.n.|| by NORMSP_3:28; then ||. L.xn .|| <= ||.f.|| * ( ||.xseq.|| .n) by NORMSP_0:def 4; hence thesis by A81,VALUED_1:6; end; then lim ||.Lf/*xseq.|| <= lim(||.f.|| (#) ||.xseq.||) by A74,A75,SEQ_2:18; then A82: lim ||.Lf/*xseq.|| <= ||.f.|| * ||.x.|| by A71,A73,SEQ_2:8; ||.f.|| * ||.x.|| <= ||.f.|| * 1 by A70,XREAL_1:64; hence t <= ||.f.|| by A70,A72,A82,XXREAL_0:2; end; then ||.g.|| <= ||.f.|| by A63,SEQ_4:45; hence ex g be Point of R_NormSpace_of_BoundedLinearOperators (E,F) st dom g = the carrier of E & g| the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf be PartFunc of E,F st Lf = f & (for x be Point of E holds ex seq be sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf/*seq is convergent & g.x = lim Lf/*seq) & (for x be Point of E, seq be sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds Lf/*seq is convergent & g.x = lim Lf/*seq) by A3,A17,A21,A22,A58,A69,XXREAL_0:1; thus for g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F) st g1| the carrier of E1 = f & g2| the carrier of E1 = f holds g1 = g2 proof let g1,g2 be Point of R_NormSpace_of_BoundedLinearOperators (E,F); assume A84: g1| the carrier of E1 = f & g2| the carrier of E1 = f; reconsider Pg1 = g1, Pg2 = g2 as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9; A85: Pg1 is_continuous_on the carrier of E by LMCONT1,NFCONT_2:7; Pg2 is_continuous_on the carrier of E by LMCONT1,NFCONT_2:7; hence thesis by A1,A3,A5,A15,A84,A85,Th020; end; end; begin :: Basic Properties of Currying theorem for E,F,G be non empty set, f be Function of [:E,F:],G, x be object st x in E holds (curry f).x is Function of F,G proof let E,F,G be non empty set, f be Function of [:E,F:],G, x be object; assume A1: x in E; dom f = [:E,F:] by FUNCT_2:def 1; then consider g being Function such that A4: (curry f) . x = g & dom g = F & rng g c= rng f & for y being object st y in F holds g . y = f . (x,y) by A1,FUNCT_5:29,ZFMISC_1:90; thus (curry f) . x is Function of F,G by A4,XBOOLE_1:1,FUNCT_2:2; end; theorem for E,F,G be non empty set, f be Function of [:E,F:],G, y be object st y in F holds (curry' f).y is Function of E,G proof let E,F,G be non empty set, f be Function of [:E,F:],G, y be object; assume A1: y in F; dom f = [:E,F:] by FUNCT_2:def 1; then ex g being Function st (curry' f) . y = g & dom g = E & rng g c= rng f & for x being object st x in E holds g . x = f . (x,y) by A1,FUNCT_5:32,ZFMISC_1:90; hence (curry' f) . y is Function of E,G by XBOOLE_1:1,FUNCT_2:2; end; theorem LM4: for E,F,G be non empty set, f be Function of [:E,F:],G, x,y be object st x in E & y in F holds ( (curry f).x ).y = f.(x,y) proof let E,F,G be non empty set, f be Function of [:E,F:],G, x,y be object; assume that A1: x in E and A2: y in F; dom f = [:E,F:] by FUNCT_2:def 1; then ex g being Function st (curry f) . x = g & dom g = F & rng g c= rng f & for y being object st y in F holds g . y = f . (x,y) by A1,FUNCT_5:29,ZFMISC_1:90; hence ( (curry f).x ).y = f.(x,y) by A2; end; theorem LM5: for E,F,G be non empty set, f be Function of [:E,F:],G, x,y be object st x in E & y in F holds ( (curry' f).y ).x = f.(x,y) proof let E,F,G be non empty set, f be Function of [:E,F:],G, x,y be object; assume that A1: x in E and A2: y in F; dom f = [:E,F:] by FUNCT_2:def 1; then ex g being Function st (curry' f) . y = g & dom g = E & rng g c= rng f & for x being object st x in E holds g . x = f . (x,y) by A2,FUNCT_5:32,ZFMISC_1:90; hence ( (curry' f).y ).x = f.(x,y) by A1; end; definition ::: probably better define it for general modules let E,F,G be RealLinearSpace; let f be Function of [:the carrier of E,the carrier of F:],the carrier of G; attr f is Bilinear means ( for v being Point of E st v in dom (curry f) holds (curry f).v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom (curry' f) holds (curry' f).v is additive homogeneous Function of E,G ); end; begin :: Equivalence of Some Definitions of Continuity of Bounded :: Bilinear Operators theorem EX1: ::: functorial registration for E,F,G be RealLinearSpace holds ( [:the carrier of E,the carrier of F:] ) --> 0.G is Bilinear proof let E,F,G be RealLinearSpace; set f = ( [:the carrier of E,the carrier of F:] ) --> 0.G; A2: for x being Point of E holds (curry f).x is additive homogeneous Function of F,G proof let x be Point of E; reconsider L = (curry f).x as Function of F,G; A5: for y1,y2 be Point of F holds L.(y1+y2) = L.y1 + L.y2 proof let y1,y2 be Point of F; A11: L.(y1+y2) = f.(x,y1+y2) by LM4 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; A12: L.y1 = f.(x,y1) by LM4 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; L.y2 = f.(x,y2) by LM4 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; hence L.(y1+y2) = L.y1 + L.y2 by A11,A12,RLVECT_1:4; end; for y be Point of F, a be Real holds L.(a*y) = a * L.y proof let y be Point of F, a be Real; A18: L.(a*y) = f.(x,a*y) by LM4 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; L.y = f.(x,y) by LM4 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; hence L.(a*y) = a * L.y by A18,RLVECT_1:10; end; hence thesis by A5,LOPBAN_1:def 5,VECTSP_1:def 20; end; for x being Point of F st x in dom (curry' f) holds (curry' f).x is additive homogeneous Function of E,G proof let x be Point of F; assume x in dom (curry' f); reconsider L = (curry' f).x as Function of E,G; A22: for y1,y2 be Point of E holds L.(y1+y2) = L.y1+L.y2 proof let y1,y2 be Point of E; A28: L.(y1+y2) = f.(y1+y2,x) by LM5 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; A29: L.y1 = f.(y1,x) by LM5 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; L.y2 = f.(y2,x) by LM5 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; hence L.(y1+y2) = L.y1 + L.y2 by A28,A29,RLVECT_1:4; end; for y be Point of E, a be Real holds L.(a*y) = a * L.y proof let y be Point of E, a be Real; A35: L.(a*y) = f.(a*y,x) by LM5 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; L.y = f.(y,x) by LM5 .= 0.G by ZFMISC_1:87,FUNCOP_1:7; hence L.(a*y) = a * L.y by A35,RLVECT_1:10; end; hence thesis by A22,LOPBAN_1:def 5,VECTSP_1:def 20; end; hence f is Bilinear by A2; end; registration let E,F,G be RealLinearSpace; cluster Bilinear for Function of [: the carrier of E, the carrier of F:], the carrier of G; correctness proof ( [:the carrier of E,the carrier of F:] ) --> 0.G is Bilinear by EX1; hence thesis; end; end; theorem LM6: for E,F,G be RealLinearSpace, L be Function of [:the carrier of E,the carrier of F:], the carrier of G holds L is Bilinear iff ( ( for x1,x2 be Point of E, y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) ) & ( for x be Point of E, y be Point of F, a be Real holds L.(a * x, y) = a * L.(x,y) ) & ( for x be Point of E, y1,y2 be Point of F holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) ) & ( for x be Point of E, y be Point of F, a be Real holds L.(x, a*y) = a * L.(x,y) ) ) proof let E,F,G be RealLinearSpace, L be Function of [:the carrier of E,the carrier of F:], the carrier of G; A1: dom(curry L) = the carrier of E & dom(curry' L) = the carrier of F by FUNCT_2:def 1; hereby assume A2: L is Bilinear; thus for x1,x2 be Point of E, y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) proof let x1,x2 be Point of E, y be Point of F; reconsider Ly = (curry' L).y as additive homogeneous Function of E,G by A1,A2; A5: Ly.x1 = L. (x1,y) by LM5; A6: Ly.x2 = L. (x2,y) by LM5; thus L.(x1+x2,y) = Ly.(x1+x2) by LM5 .= L.(x1,y) + L.(x2,y) by A5,A6,VECTSP_1:def 20; end; thus for x be Point of E, y be Point of F, a be Real holds L.(a*x, y) = a * L.(x,y) proof let x be Point of E, y be Point of F, a be Real; reconsider Ly = (curry' L).y as additive homogeneous Function of E,G by A1,A2; thus L.(a*x, y) = Ly.(a*x) by LM5 .= a * Ly.x by LOPBAN_1:def 5 .= a * L.(x,y) by LM5; end; thus for x be Point of E, y1,y2 be Point of F holds L.(x, y1+y2) = L.(x,y1) + L.(x,y2) proof let x be Point of E, y1,y2 be Point of F; reconsider Lx = (curry L).x as additive homogeneous Function of F,G by A1,A2; A8: Lx.y1 = L.(x,y1) by LM4; A9: Lx.y2 = L.(x,y2) by LM4; thus L.(x,y1+y2) = Lx.(y1+y2) by LM4 .= L. (x,y1) + L. (x,y2) by A8,A9,VECTSP_1:def 20; end; thus for x be Point of E, y be Point of F, a be Real holds L.(x, a*y) = a * L.(x,y) proof let x be Point of E, y be Point of F, a be Real; reconsider Lx = (curry L).x as additive homogeneous Function of F,G by A1,A2; A10: Lx.y = L.(x,y) by LM4; thus L.(x, a*y) = Lx.(a*y) by LM4 .= a * L.(x,y) by A10,LOPBAN_1:def 5; end; end; assume that A11: for x1,x2 be Point of E, y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) and A12: for x be Point of E, y be Point of F, a be Real holds L.(a*x, y) = a * L.(x,y) and A13: for x be Point of E, y1,y2 be Point of F holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) and A14: for x be Point of E, y be Point of F, a be Real holds L.(x, a*y) = a * L.(x,y); A15: for x being Point of E st x in dom (curry L) holds (curry L).x is additive homogeneous Function of F,G proof let x be Point of E; assume x in dom (curry L); reconsider Lx = (curry L).x as Function of F,G; A16: for y1,y2 be Point of F holds Lx.(y1+y2) = Lx.y1+Lx.y2 proof let y1,y2 be Point of F; A17: L.(x,y1) = Lx.y1 by LM4; thus Lx.(y1+y2) = L.(x,y1+y2) by LM4 .= L.(x,y1) + L.(x,y2) by A13 .= Lx.y1 + Lx.y2 by A17,LM4; end; for y be Point of F, a be Real holds Lx.(a*y) = a * Lx.y proof let y be Point of F, a be Real; thus Lx.(a*y) = L. (x, a*y) by LM4 .= a * L.(x,y) by A14 .= a * Lx.y by LM4; end; hence thesis by A16,LOPBAN_1:def 5,VECTSP_1:def 20; end; for y being Point of F st y in dom (curry' L) holds (curry' L).y is additive homogeneous Function of E,G proof let y be Point of F; assume y in dom (curry' L); reconsider Ly = (curry' L).y as Function of E,G; A22: for x1,x2 be Point of E holds Ly.(x1+x2) = Ly.x1 + Ly.x2 proof let x1,x2 be Point of E; A23: L.(x1,y) = Ly.x1 by LM5; thus Ly.(x1+x2) = L.(x1+x2,y) by LM5 .= L.(x1,y) + L.(x2,y) by A11 .= Ly.x1+Ly.x2 by A23,LM5; end; for x be Point of E,a be Real holds Ly.(a*x) = a * Ly.x proof let x be Point of E, a be Real; thus Ly.(a*x) = L.(a*x,y) by LM5 .= a * L.(x,y) by A12 .= a * Ly.x by LM5; end; hence thesis by A22,LOPBAN_1:def 5,VECTSP_1:def 20; end; hence L is Bilinear by A15; end; definition let E,F,G be RealLinearSpace; let f be Function of [:E,F:],G; attr f is Bilinear means ex g be Function of [:the carrier of E,the carrier of F:], the carrier of G st f = g & g is Bilinear; end; registration let E,F,G be RealLinearSpace; cluster Bilinear for Function of [:E,F:],G; correctness proof set g = ( [:the carrier of E,the carrier of F:] ) --> 0.G; reconsider f = g as Function of [:E,F:],G; take f; thus thesis by EX1; end; end; definition let E,F,G be RealLinearSpace; let f be Function of [:E,F:],G; let x be Point of E; let y be Point of F; redefine func f.(x,y) -> Point of G; correctness proof f.[x,y] is Point of G; hence thesis; end; end; theorem for E,F,G be RealLinearSpace, L be Function of [:E,F:],G holds L is Bilinear iff ( ( for x1,x2 be Point of E, y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) ) & ( for x be Point of E, y be Point of F, a be Real holds L.(a*x,y) = a * L.(x,y) ) & ( for x be Point of E, y1,y2 be Point of F holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) ) & ( for x be Point of E, y be Point of F, a be Real holds L. (x, a*y) = a * L.(x,y) ) ) by LM6; definition let E,F,G be RealLinearSpace; mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G; end; definition let E,F,G be RealNormSpace; let f be Function of [:E,F:],G; attr f is Bilinear means ex g be Function of [:the carrier of E, the carrier of F:], the carrier of G st f = g & g is Bilinear; end; registration let E,F,G be RealNormSpace; cluster Bilinear for Function of [:E,F:],G; correctness proof set g = ( [:the carrier of E,the carrier of F:] ) --> 0.G; reconsider f = g as Function of [:E,F:],G; take f; thus thesis by EX1; end; end; definition let E,F,G be RealNormSpace; mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G; end; reserve E,F,G for RealNormSpace; reserve L for BilinearOperator of E,F,G; reserve x for Element of E; reserve y for Element of F; definition let E,F,G be RealNormSpace; let f be Function of [:E,F:], G; let x be Point of E; let y be Point of F; redefine func f.(x,y) -> Point of G; correctness proof f.[x,y] is Point of G; hence thesis; end; end; theorem LM8: for E,F,G be RealNormSpace, L be Function of [:E,F:],G holds L is Bilinear iff ( ( for x1,x2 be Point of E, y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) ) & ( for x be Point of E, y be Point of F, a be Real holds L.(a*x, y) = a * L.(x,y) ) & ( for x be Point of E, y1,y2 be Point of F holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) ) & ( for x be Point of E, y be Point of F, a be Real holds L.(x,a*y) = a * L.(x,y) ) ) by LM6; theorem for E,F,G be RealNormSpace, f be BilinearOperator of E,F,G holds ( f is_continuous_on the carrier of [:E,F:] iff f is_continuous_in 0.( [:E,F:] ) ) & ( f is_continuous_on the carrier of [:E,F:] iff ex K be Real st 0 <= K & for x be Point of E,y be Point of F holds ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| ) proof let E,F,G be RealNormSpace, f be BilinearOperator of E,F,G; A1: dom f = the carrier of [:E,F:] by FUNCT_2:def 1; A2: f. 0. [:E,F:] = f.(0.E,0.F) by PRVECT_3:18 .= f.(0* 0.E,0.F) by RLVECT_1:10 .= 0 * f.(0.E,0.F) by LM8 .= 0.G by RLVECT_1:10; A4: f is_continuous_in 0.( [:E,F:] ) implies ex K be Real st 0 <= K & for x be Point of E,y be Point of F holds ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| proof assume f is_continuous_in 0. [:E,F:]; then consider s be Real such that A5: 0 < s & for z be Point of [:E,F:] st z in dom f & ||. z - 0. [:E,F:] .|| < s holds ||. f/.z- f/. 0. [:E,F:] .|| < 1 by NFCONT_1:7; consider s1 be Real such that A7: 0 < s1 & s1 < s & [:Ball(0.E,s1),Ball(0.F,s1):] c= Ball(0. [:E,F:],s) by A5,NDIFF_8:22,PRVECT_3:18; set s2 = s1/2; A8: 0 < s2 & s2 < s1 by A7,XREAL_1:215,216; A9: now let x be Point of E, y be Point of F; assume ||.x.|| <= s2 & ||.y.|| <= s2; then A10: ||.x.|| < s1 & ||.y.|| < s1 by A8,XXREAL_0:2; reconsider z = [x,y] as Point of [:E,F:]; ||.x - 0.E .|| < s1 by A10,RLVECT_1:13; then ||.0.E -x .|| < s1 by NORMSP_1:7; then A12: x in Ball(0.E,s1); ||.y - 0.F .|| < s1 by A10,RLVECT_1:13; then ||.0.F -y .|| < s1 by NORMSP_1:7; then y in Ball(0.F,s1); then z in [:Ball(0.E,s1),Ball(0.F,s1):] by A12,ZFMISC_1:87; then z in Ball(0. [:E,F:],s) by A7; then ex z1 be Point of [:E,F:] st z = z1 & ||. 0. [:E,F:] - z1 .|| < s; then ||.z - 0. [:E,F:] .|| < s by NORMSP_1:7; then ||. f/.z - f/. 0. [:E,F:] .|| < 1 by A5,A1; hence ||. f.(x,y) .||< 1 by A2,RLVECT_1:13; end; A14: 0 < s2*s2 by A8,XREAL_1:129; take K = 1/(s2*s2); thus 0 <= K by A7; let x be Point of E,y be Point of F; A15: f.(0.E,y) = f.(0 * 0.E,y) by RLVECT_1:10 .= 0 * f.(0.E,y) by LM8 .= 0.G by RLVECT_1:10; A16: f.(x,0.F) = f.(x,0 * 0.F) by RLVECT_1:10 .= 0 * f.(x,0.F) by LM8 .= 0.G by RLVECT_1:10; thus ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| proof per cases; suppose C16: x <> 0.E & y <> 0.F; then ||.x.|| <> 0 & ||.y.|| <> 0 by NORMSP_0:def 5; then A17: 0 < ||.x.|| & 0 < ||.y.||; set x1 = (s2/||.x.||) * x; set y1 = (s2/||.y.||) * y; A19: ||.x1.|| = |. s2 / ||.x.|| .| * ||.x.|| by NORMSP_1:def 1 .= (s2 / ||.x.||) * ||.x.|| by A7,COMPLEX1:43 .= s2 by C16,NORMSP_0:def 5,XCMPLX_1:87; A21: ||.y1.|| = |. s2 / ||.y.|| .| * ||.y.|| by NORMSP_1:def 1 .= (s2/||.y.||)*||.y.|| by A7,COMPLEX1:43 .= s2 by C16,NORMSP_0:def 5,XCMPLX_1:87; A23: f. (x1,y1) = (s2 / ||.x.||) * f.(x, (s2 / ||.y.||) * y) by LM8; f.(x, (s2 / ||.y.||) * y) = (s2/||.y.||) * f.(x,y) by LM8; then A24: f.(x1,y1) = ((s2 / ||.x.||) * (s2 / ||.y.||) ) * ( f.(x,y) ) by A23,RLVECT_1:def 7 .= (s2 * s2) / (||.x.|| * ||.y.||) * f.(x,y) by XCMPLX_1:76; A25: 0 < ||.x.|| * ||.y.|| by A17,XREAL_1:129; ||.f. (x1,y1) .|| = |. (s2 * s2) / ( ||.x.|| * ||.y.||) .| * ||. f. (x,y) .|| by A24,NORMSP_1:def 1 .= (s2 * s2)/ (||.x.|| * ||.y.||) * ||. f.(x,y) .|| by A7,COMPLEX1:43; then A28: (s2 * s2) / (||.x.|| * ||.y.||) * ||. f.(x,y) .|| < 1 by A9,A19,A21; (s2 * s2) / (||.x.|| * ||.y.||) * ||. f.(x,y) .|| * (||.x.||*||.y.||) <= 1 * (||.x.|| * ||.y.||) by A28,XREAL_1:64; then (s2 * s2) / (||.x.||*||.y.||) * (||.x.||*||.y.||) * ||. f.(x,y) .|| <= ||.x.||*||.y.||; then (s2 * s2) * ||. f.(x,y) .|| <= ||.x.|| * ||.y.|| by A25,XCMPLX_1:87; then (s2 * s2) * ||. f.(x,y) .|| / (s2 * s2) <= ||.x.|| * ||.y.|| / (s2 * s2) by A7,XREAL_1:72; then ||. f.(x,y) .|| <= (||.x.|| * ||.y.||) / (s2 * s2) by A14,XCMPLX_1:89; then ||. f.(x,y) .|| <= 1 / (s2 * s2) * (||.x.|| * ||.y.||) by XCMPLX_1:99; hence ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||; end; suppose A29: x = 0.E or y = 0.F; then ||.x.|| = 0 or ||.y.|| = 0; hence ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.|| by A15,A16,A29; end; end; end; ( ex K be Real st 0 <= K & for x be Point of E,y be Point of F holds ||.f. (x,y) .|| <= K * ||.x.|| * ||.y.|| ) implies f is_continuous_on the carrier of [:E,F:] proof given K be Real such that A32: 0 <= K & for x be Point of E,y be Point of F holds ||. f.(x,y) .|| <= K * ||.x.|| * ||.y.||; A33: the carrier of [:E,F:] c= dom f by FUNCT_2:def 1; for z0 be Point of [:E,F:], r1 be Real st z0 in the carrier of [:E,F:] & 0 < r1 ex s be Real st 0 < s & for z1 be Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||. z1 - z0 .|| < s holds ||. f/.z1 - f/.z0 .|| < r1 proof let z0 be Point of [:E,F:],r1 be Real; assume A34: z0 in the carrier of [:E,F:] & 0 < r1; set r = r1/2; A35: 0 < r & r < r1 by A34,XREAL_1:215,216; consider x0 be Point of E,y0 be Point of F such that A36: z0 = [x0,y0] by PRVECT_3:18; set KXY0 = ( K + 1 ) * (||.x0.|| + 1 + ||.y0.||); set s1 = r / KXY0; K + 0 < K + 1 by XREAL_1:8; then A39: K * (||.x0.|| + 1 + ||.y0.||) < (K+1) * (||.x0.|| + 1 + ||.y0.||) by XREAL_1:68; A40: 0 < KXY0 by A32,XREAL_1:129; then A41: 0 < s1 by A35,XREAL_1:139; set s = min(s1,1); A42: s <= 1 & s <= s1 by XXREAL_0:17; A43: 0 < s by A41,XXREAL_0:21; then A44: ( K * (||.x0.|| + 1 + ||.y0.||)) * s <= KXY0 * s1 by A32,A39,A42,XREAL_1:66; take s; thus 0 < s by A41,XXREAL_0:21; let z1 be Point of [:E,F:]; assume A45: z1 in the carrier of [:E,F:] & ||. z1 - z0 .|| < s; consider x1 be Point of E,y1 be Point of F such that A46: z1 = [x1,y1] by PRVECT_3:18; A47: f.z1 - f.z0 = f.(x1,y1) - f.(x0,y1) + f.(x0,y1) - f.(x0,y0) by A36,A46,RLVECT_4:1 .= (f.(x1,y1) - f.(x0,y1)) + (f.(x0,y1) -f.(x0,y0)) by RLVECT_1:28; A49: f.(x1,y1) - f.(x0,y1) = f.(x1,y1) +(-1)* f.(x0,y1) by RLVECT_1:16 .= f.(x1,y1) + f.((-1)*x0,y1) by LM8 .= f.(x1+(-1)*x0,y1) by LM8 .= f.(x1-x0,y1) by RLVECT_1:16; A51: f.(x0,y1) - f.(x0,y0) = f.(x0,y1) +(-1)* f.(x0,y0) by RLVECT_1:16 .= f.(x0,y1) + f.(x0,(-1)*y0) by LM8 .= f.(x0, y1+(-1)*y0) by LM8 .= f.(x0,y1-y0) by RLVECT_1:16; A52: ||. f.(x1-x0,y1) .|| <= K * ||.x1-x0.|| * ||.y1.|| by A32; A53: ||. f.(x0,y1-y0) .|| <= K * ||.x0.|| * ||.y1-y0.|| by A32; -z0 = [-x0,-y0] by A36,PRVECT_3:18; then A54: z1 - z0 = [x1-x0,y1-y0] by A46,PRVECT_3:18; then ||.x1-x0.|| <= ||.z1- z0.|| by NDIFF_8:21; then A55: ||.x1-x0.|| < s by A45,XXREAL_0:2; ||.y1-y0.|| <= ||.z1- z0.|| by A54,NDIFF_8:21; then A56: ||.y1-y0.|| < s by A45,XXREAL_0:2; ||.x1-x0.|| * ||.y1.|| <= s * ||.y1.|| by A55,XREAL_1:64; then K * (||.x1-x0.|| * ||.y1.||) <= K * ( s * ||.y1.||) by A32,XREAL_1:64; then A57: ||.f.(x1-x0,y1) .|| <= K * s * ||.y1.|| by A52,XXREAL_0:2; ||.y1-y0.|| * ||.x0.|| <= s * ||.x0.|| by A56,XREAL_1:64; then K * ( ||.x0.|| * ||.y1-y0.|| ) <= K * ( s *||.x0.|| ) by A32,XREAL_1:64; then ||.f.(x0,y1-y0) .|| <= K * s * ||.x0.|| by A53,XXREAL_0:2; then A58: ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= K * s * ||.y1.|| + K * s * ||.x0.|| by A57,XREAL_1:7; ||.y1.|| = ||. y1 - y0 + y0 .|| by RLVECT_4:1; then A60: ||.y1.|| <= ||.y1-y0.|| + ||.y0.|| by NORMSP_1:def 1; ||. y1-y0 .|| + ||.y0.|| <= s + ||.y0.|| by A56,XREAL_1:7; then A61: ||.y1.|| <= s + ||.y0.|| by A60,XXREAL_0:2; s + ||.y0.|| <= 1 + ||.y0.|| by A42,XREAL_1:7; then ||.y1.|| <= 1 + ||.y0.|| by A61,XXREAL_0:2; then ||.y1.|| + ||.x0.|| <= 1 + ||.y0.|| + ||.x0.|| by XREAL_1:7; then s * (||.y1.|| + ||.x0.||) <= s * (1 + ||.y0.|| + ||.x0.||) by A43,XREAL_1:64; then s * (||.y1.|| + ||.x0.||) * K <= s * (1 + ||.y0.|| + ||.x0.||) * K by A32,XREAL_1:64; then ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= K * s * (||.x0.|| + 1+ ||.y0.||) by A58,XXREAL_0:2; then ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= KXY0 * (r/KXY0) by A44,XXREAL_0:2; then A64: ||. f.(x1-x0,y1) .|| + ||. f.(x0,y1-y0) .|| <= r by A40,XCMPLX_1:87; ||.f.z1 - f.z0 .|| <= ||. f.(x1,y1) -f.(x0,y1) .|| + ||. f.(x0,y1) - f.(x0,y0) .|| by A47,NORMSP_1:def 1; then ||. f/.z1 - f/.z0 .|| <= r by A49,A51,A64,XXREAL_0:2; hence ||. f/.z1 - f/.z0 .|| < r1 by A35,XXREAL_0:2; end; hence thesis by A33,NFCONT_1:19; end; hence thesis by A4; end;