:: Real Normed Space
:: by Jan Popio{\l}ek
::
:: Received September 20, 1990
:: Copyright (c) 1990-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, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1,
FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, RLSUB_1,
FUNCOP_1, CARD_1, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, ARYTM_1, NAT_1,
TARSKI, SEQ_2, ORDINAL2, NORMSP_1, NORMSP_0, RELAT_2, METRIC_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, FUNCT_2, BINOP_1,
RELAT_1, COMSEQ_2, SEQ_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, XXREAL_0, NORMSP_0;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
SEQ_2, RLSUB_1, VALUED_1, RELSET_1, NORMSP_0, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
STRUCT_0, RLVECT_1, ALGSTR_0, NORMSP_0, XCMPLX_0, VALUED_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
definition
struct(RLSStruct, N-ZeroStr) NORMSTR (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:], the
carrier, normF -> Function of the carrier, REAL #);
end;
registration
cluster non empty strict for NORMSTR;
end;
reserve a, b for Real;
definition
let IT be non empty NORMSTR;
attr IT is RealNormSpace-like means
:: NORMSP_1:def 1
for x, y being Point of IT, a holds ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
.|| <= ||.x.|| + ||.y.||;
end;
registration
cluster reflexive discerning RealNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian add-associative
right_zeroed right_complementable strict for non empty NORMSTR;
end;
definition
mode RealNormSpace is reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
non empty NORMSTR;
end;
reserve RNS for RealNormSpace;
reserve x, y, z, g, g1, g2 for Point of RNS;
theorem :: NORMSP_1:1
||.0.RNS.|| = 0;
theorem :: NORMSP_1:2
||.-x.|| = ||.x.||;
theorem :: NORMSP_1:3
||.x - y.|| <= ||.x.|| + ||.y.||;
theorem :: NORMSP_1:4
0 <= ||.x.||;
registration
let RNS,x;
cluster ||.x.|| -> non negative;
end;
theorem :: NORMSP_1:5
||.a * x + b * y.|| <= |.a.| * ||.x.|| + |.b.| * ||.y.||;
theorem :: NORMSP_1:6
||.x - y.|| = 0 iff x = y;
theorem :: NORMSP_1:7
||.x - y.|| = ||.y - x.||;
theorem :: NORMSP_1:8
||.x.|| - ||.y.|| <= ||.x - y.||;
theorem :: NORMSP_1:9
|.||.x.|| - ||.y.||.| <= ||.x - y.||;
theorem :: NORMSP_1:10
||.x - z.|| <= ||.x - y.|| + ||.y - z.||;
theorem :: NORMSP_1:11
x <> y implies ||.x - y.|| <> 0;
reserve S, S1, S2 for sequence of RNS;
reserve k, n, m, m1, m2 for Nat;
reserve r for Real;
reserve f for Function;
reserve d, s, t for set;
theorem :: NORMSP_1:12
for RNS being non empty 1-sorted, x being Element of RNS holds f is
sequence of RNS iff ( dom f = NAT & for d st d in NAT holds f.d is Element of
RNS );
theorem :: NORMSP_1:13
for RNS being non empty 1-sorted, x being Element of RNS ex S being
sequence of RNS st rng S = {x};
theorem :: NORMSP_1:14
for RNS being non empty 1-sorted, S being sequence of RNS st (ex x
being Element of RNS st for n being Nat holds S.n = x) ex x being Element of
RNS st rng S={x};
theorem :: NORMSP_1:15
for RNS being non empty 1-sorted, S being sequence of RNS st ex x
being Element of RNS st rng S = {x} holds for n holds S.n = S.(n+1);
theorem :: NORMSP_1:16
for RNS being non empty 1-sorted, S being sequence of RNS st for n
holds S.n = S.(n+1) holds for n, k holds S.n = S.(n+k);
theorem :: NORMSP_1:17
for RNS being non empty 1-sorted, S being sequence of RNS st for n, k
holds S.n = S.(n+k) holds for n, m holds S.n = S.m;
theorem :: NORMSP_1:18
for RNS being non empty 1-sorted, S being sequence of RNS st for n, m
holds S.n = S.m ex x being Element of RNS st for n being Nat holds S.n = x;
definition
let RNS be non empty addLoopStr;
let S1, S2 be sequence of RNS;
func S1 + S2 -> sequence of RNS means
:: NORMSP_1:def 2
for n holds it.n = S1.n + S2.n;
end;
definition
let RNS be non empty addLoopStr;
let S1, S2 be sequence of RNS;
func S1 - S2 -> sequence of RNS means
:: NORMSP_1:def 3
for n holds it.n = S1.n - S2.n;
end;
definition
let RNS be non empty addLoopStr;
let S be sequence of RNS;
let x be Element of RNS;
func S - x -> sequence of RNS means
:: NORMSP_1:def 4
for n holds it.n = S.n - x;
end;
definition
let RNS be non empty RLSStruct;
let S be sequence of RNS;
let a be Real;
func a * S -> sequence of RNS means
:: NORMSP_1:def 5
for n holds it.n = a * S.n;
end;
definition
let RNS, S;
attr S is convergent means
:: NORMSP_1:def 6
ex g st for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
end;
theorem :: NORMSP_1:19
S1 is convergent & S2 is convergent implies S1 + S2 is convergent;
theorem :: NORMSP_1:20
S1 is convergent & S2 is convergent implies S1 - S2 is convergent;
theorem :: NORMSP_1:21
S is convergent implies S - x is convergent;
theorem :: NORMSP_1:22
S is convergent implies a * S is convergent;
theorem :: NORMSP_1:23
S is convergent implies ||.S.|| is convergent;
definition
let RNS, S;
assume
S is convergent;
func lim S -> Point of RNS means
:: NORMSP_1:def 7
for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - it.|| < r;
end;
theorem :: NORMSP_1:24
S is convergent & lim S = g implies ||.S - g.|| is convergent & lim
||.S - g.|| = 0;
theorem :: NORMSP_1:25
S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) +
(lim S2);
theorem :: NORMSP_1:26
S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) -
(lim S2);
theorem :: NORMSP_1:27
S is convergent implies lim (S - x) = (lim S) - x;
theorem :: NORMSP_1:28
S is convergent implies lim (a * S) = a * (lim S);