:: Preliminaries to Normed Spaces :: by Andrzej Trybulec :: :: Received March 23, 2010 :: Copyright (c) 2010-2018 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; 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; end; definition struct(1-sorted) N-Str (# carrier -> set, normF -> Function of the carrier, REAL #); end; registration cluster non empty strict for N-Str; 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 :: NORMSP_0:def 1 (the normF of X).x; end; reserve X for non empty N-Str; definition let X; let f be (the carrier of X)-valued Function; func ||.f.|| -> Function means :: NORMSP_0:def 2 dom it = dom f & for e being set st e in dom it holds it.e = ||. f/.e .||; end; registration let X; let f be (the carrier of X)-valued Function; cluster ||.f.|| -> REAL-valued; 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 :: NORMSP_0:def 3 dom it = dom f & for c being Element of C st c in dom it holds it.c = ||. f/.c .||; end; definition :: NORMSP_1:def 10, CLVECT_1:def 17 let X; let s be sequence of X; redefine func ||.s.|| -> Real_Sequence means :: NORMSP_0:def 4 for n being Nat holds it.n = ||. s.n .||; 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; end; reserve X for non empty N-ZeroStr, x for Element of X; definition let X; attr X is discerning means :: NORMSP_0:def 5 ||.x.|| = 0 implies x = 0.X; attr X is reflexive means :: NORMSP_0:def 6 ||.0.X.|| = 0; end; registration cluster reflexive discerning for non empty strict N-ZeroStr; end; registration let X be reflexive non empty N-ZeroStr; let x be zero Element of X; cluster ||.x.|| -> zero; end;