:: Preliminaries to Normed Spaces
:: by Andrzej Trybulec
::
:: Received March 23, 2010
:: Copyright (c) 2010-2026 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; :: redefines . (FUNCT_1, definition)
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 :: redefines ||. (NORMSP_0, definition)
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 :: redefines ||. (NORMSP_0, definition)
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;