:: Preliminaries to Normed Spaces :: by Andrzej Trybulec :: :: Received March 23, 2010 :: Copyright (c) 2010-2017 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 SUBSET_1, STRUCT_0, NORMSP_1, FUNCT_1, NUMBERS, REAL_1, XBOOLE_0, FUNCT_5, CARD_1, METRIC_1, RELAT_2, SUPINF_2, XCMPLX_0, NAT_1, SEQ_1, RELAT_1, TARSKI, PARTFUN1, NORMSP_0; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_5, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, SEQ_1, STRUCT_0; constructors FUNCT_2, NUMBERS, STRUCT_0, FUNCT_5, FUNCOP_1, XCMPLX_0, RELSET_1, XREAL_0; registrations STRUCT_0, RELSET_1, XBOOLE_0, NUMBERS, XREAL_0, ORDINAL1, FUNCT_2; requirements BOOLE, SUBSET; definitions TARSKI, RELAT_1, FUNCT_1; equalities FUNCT_5, FUNCOP_1, STRUCT_0; theorems FUNCOP_1, TARSKI, FUNCT_1, RELAT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, XREAL_0, ORDINAL1; schemes FUNCT_1; begin definition let RNS be non empty 1-sorted; let s be sequence of RNS,n be Nat; redefine func s.n -> Element of RNS; coherence proof reconsider n as Element of NAT by ORDINAL1:def 12; s.n is Element of RNS; hence thesis; end; end; definition struct(1-sorted) N-Str (# carrier -> set, normF -> Function of the carrier, REAL #); end; 0 in REAL by XREAL_0:def 1; then reconsider f = op1 as Function of {0}, REAL by FUNCOP_1:46; reconsider z = 0 as Element of {0} by TARSKI:def 1; registration cluster non empty strict for N-Str; existence proof take N-Str(#{0},f#); thus thesis; end; end; definition :: NORMSP_1:def 1, CLVECT_1:def 13 let X be non empty N-Str, x be Element of X; func ||.x.|| -> Real equals (the normF of X).x; coherence; end; reserve X for non empty N-Str; definition let X; let f be (the carrier of X)-valued Function; func ||.f.|| -> Function means :Def2: dom it = dom f & for e being set st e in dom it holds it.e = ||. f/.e .||; existence proof deffunc F(object) = ||. f/.\$1 .||; consider g being Function such that A1: dom g = dom f and A2: for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3; take g; thus thesis by A1,A2; end; uniqueness proof let f1,f2 be Function such that A3: dom f1 = dom f and A4: for e being set st e in dom f1 holds f1.e = ||. f/.e .|| and A5: dom f2 = dom f and A6: for e being set st e in dom f2 holds f2.e = ||. f/.e .||; thus dom f1 = dom f2 by A3,A5; let e be object; assume A7: e in dom f1; hence f1.e = ||.f/.e .|| by A4 .= f2.e by A3,A5,A6,A7; end; end; registration let X; let f be (the carrier of X)-valued Function; cluster ||.f.|| -> REAL-valued; coherence proof let u be object; assume u in rng ||.f.||; then consider e being object such that A1: e in dom ||.f.|| and A2: u = ||.f.||.e by FUNCT_1:def 3; ||.f.||.e = ||. f/.e .|| by A1,Def2; hence u in REAL by A2; end; end; definition let C be non empty set, X; :: VFUNCT_1:def 5, VFUNCT_2:def 5, NCFCONT1:def 2, def 3, def 4 :: NFCONT_1:def 2 let f be PartFunc of C, the carrier of X; redefine func ||.f.|| -> PartFunc of C, REAL means dom it = dom f & for c being Element of C st c in dom it holds it.c = ||. f/.c .||; coherence proof dom ||.f.|| = dom f by Def2; then A1: dom ||.f.|| c= C by RELAT_1:def 18; rng ||.f.|| c= REAL proof let e be object; assume e in rng ||.f.||; then consider u being object such that A2: u in dom ||.f.|| and A3: e = ||.f.||.u by FUNCT_1:def 3; e = ||.f/.u.|| by A2,A3,Def2; hence e in REAL; end; hence ||.f.|| is PartFunc of C, REAL by A1,RELSET_1:4; end; compatibility proof let F be PartFunc of C, REAL; thus F = ||.f.|| implies dom F = dom f & for c being Element of C st c in dom F holds F.c = ||. f/.c .|| by Def2; assume that A4: dom F = dom f and A5: for c being Element of C st c in dom F holds F.c = ||. f/.c .||; for e being set st e in dom F holds F.e = ||. f/.e .|| proof let e be set; assume A6: e in dom F; dom F c= C by RELAT_1:def 18; then reconsider c = e as Element of C by A6; thus F.e = ||. f/.c .|| by A6,A5 .= ||. f/.e .||; end; hence F = ||.f.|| by A4,Def2; end; end; definition :: NORMSP_1:def 10, CLVECT_1:def 17 let X; let s be sequence of X; redefine func ||.s.|| -> Real_Sequence means for n being Nat holds it.n = ||. s.n .||; coherence proof A1: dom ||.s.|| = dom s by Def2 .= NAT by PARTFUN1:def 2; rng ||.s.|| c= REAL by RELAT_1:def 19; hence ||.s.|| is Real_Sequence by A1,FUNCT_2:2; end; compatibility proof let S be Real_Sequence; A2: dom S = NAT by PARTFUN1:def 2; A3: dom s = NAT by PARTFUN1:def 2; thus S = ||.s.|| implies for n being Nat holds S.n = ||. s.n .|| proof assume A4: S = ||.s.||; let n be Nat; A5: n in NAT by ORDINAL1:def 12; thus S.n = ||.s.||.n by A4 .= ||. s/.n .|| by Def2,A2,A4,A5 .= ||. s.n .|| by A3,A5,PARTFUN1:def 6; end; assume A6: for n being Nat holds S.n = ||. s.n .||; for e being set st e in dom s holds S.e = ||. s/.e .|| proof let e be set; assume A7: e in dom s; then reconsider n = e as Element of NAT by PARTFUN1:def 2; thus S.e = ||. s.n .|| by A6 .= ||. s/.e .|| by A7,PARTFUN1:def 6; end; hence S = ||.s.|| by A2,A3,Def2; end; end; definition struct(N-Str, ZeroStr) N-ZeroStr (# carrier -> set, ZeroF -> Element of the carrier, normF -> Function of the carrier, REAL #); end; registration cluster non empty strict for N-ZeroStr; existence proof take N-ZeroStr(#{0},z,f#); thus thesis; end; end; reserve X for non empty N-ZeroStr, x for Element of X; definition let X; attr X is discerning means ||.x.|| = 0 implies x = 0.X; attr X is reflexive means :Def6: ||.0.X.|| = 0; end; registration cluster reflexive discerning for non empty strict N-ZeroStr; existence proof reconsider S = N-ZeroStr(#{0},z,f#)as non empty strict N-ZeroStr; take S; ||.0.S.|| = 0 by FUNCOP_1:7; hence S is reflexive; let x be Element of S; thus thesis by TARSKI:def 1; end; end; registration let X be reflexive non empty N-ZeroStr; let x be zero Element of X; cluster ||.x.|| -> zero; coherence proof x = 0.X by STRUCT_0:def 12; hence thesis by Def6; end; end;