:: The Continuous Functions on Normed Linear Spaces :: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama :: :: Received April 6, 2004 :: Copyright (c) 2004-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, SUBSET_1, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC, XBOOLE_0, ALGSTR_0, ARYTM_1, ARYTM_3, FUNCT_1, RELAT_1, STRUCT_0, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, COMPLEX1, VALUED_1, CFCONT_1, SEQ_1, SEQ_4, NFCONT_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, ALGSTR_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, RLVECT_1, SEQ_1, SEQ_2, SEQ_4, RCOMP_1, VFUNCT_1, NORMSP_0, NORMSP_1, XXREAL_0; constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, VFUNCT_1, RELSET_1, COMSEQ_2; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0, RLVECT_1, VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Continuous Functions on Normed Linear Spaces reserve n,m for Nat; reserve x,X,X1 for set; reserve s,g,r,p for Real; reserve S,T for RealNormSpace; reserve f,f1,f2 for PartFunc of S,T; reserve s1,s2 for sequence of S; reserve x0,x1,x2 for Point of S; reserve Y for Subset of S; theorem :: NFCONT_1:1 for S being non empty addLoopStr for seq1,seq2 be sequence of S holds seq1 - seq2 = seq1 +- seq2; theorem :: NFCONT_1:2 for seq be sequence of S holds -seq=(-1)*seq; definition let S, x0; mode Neighbourhood of x0 -> Subset of S means :: NFCONT_1:def 1 ex g be Real st 0{} & (dom f ) is compact & f is_continuous_on (dom f) ex x1,x2 st x1 in dom f & x2 in dom f & f/.x1 = upper_bound (rng f) & f/.x2 = lower_bound (rng f); theorem :: NFCONT_1:34 for f st dom f<>{} & (dom f) is compact & f is_continuous_on ( dom f) ex x1,x2 st x1 in dom f & x2 in dom f & ||.f.||/.x1 = upper_bound (rng ||.f.||) & ||.f.||/.x2 = lower_bound (rng ||.f.||); theorem :: NFCONT_1:35 (||.f.||)|X = ||.(f|X).||; theorem :: NFCONT_1:36 for f,Y st Y<>{} & Y c= dom f & Y is compact & f is_continuous_on Y ex x1,x2 st x1 in Y & x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/. x2 = lower_bound (||.f.||.:Y); theorem :: NFCONT_1:37 for f be PartFunc of the carrier of S,REAL for Y st Y<>{} & Y c= dom f & Y is compact & f is_continuous_on Y ex x1,x2 st x1 in Y & x2 in Y & f/.x1 = upper_bound (f.:Y) & f/.x2 = lower_bound (f.:Y); definition let S,T; let X,f; pred f is_Lipschitzian_on X means :: NFCONT_1:def 9 X c= dom f & ex r st 0