:: Preliminaries to Normed Spaces
:: by Andrzej Trybulec
::
:: Received March 23, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
begin
definition
attr
c
1
is
strict
;
struct
N-Str
->
1-sorted
;
aggr
N-Str
(#
carrier
,
normF
#)
->
N-Str
;
sel
normF
c
1
->
Function
of the
carrier
of
c
1
,
REAL
;
end;
op1
=
1
-->
0
by
CARD_1:49
;
then
reconsider
f
=
op1
as
Function
of 1,
REAL
by
FUNCOP_1:46
;
reconsider
z
=
0
as
Element
of 1
by
CARD_1:49
,
TARSKI:def 1
;
registration
cluster
non
empty
strict
for
N-Str
;
existence
ex
b
1
being
N-Str
st
( not
b
1
is
empty
&
b
1
is
strict
)
proof
end;
end;
definition
let
X
be non
empty
N-Str
;
let
x
be
Element
of
X
;
func
||.
x
.||
->
Real
equals
:: NORMSP_0:def 1
the
normF
of
X
.
x
;
coherence
the
normF
of
X
.
x
is
Real
;
end;
::
deftheorem
defines
||.
NORMSP_0:def 1 :
for
X
being non
empty
N-Str
for
x
being
Element
of
X
holds
||.
x
.||
=
the
normF
of
X
.
x
;
definition
let
X
be non
empty
N-Str
;
let
f
be the
carrier
of
X
-valued
Function
;
func
||.
f
.||
->
Function
means
:
Def2
:
:: NORMSP_0:def 2
(
dom
it
=
dom
f
& ( for
e
being
set
st
e
in
dom
it
holds
it
.
e
=
||.
(
f
/.
e
)
.||
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
e
being
set
st
e
in
dom
b
1
holds
b
1
.
e
=
||.
(
f
/.
e
)
.||
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
e
being
set
st
e
in
dom
b
1
holds
b
1
.
e
=
||.
(
f
/.
e
)
.||
) &
dom
b
2
=
dom
f
& ( for
e
being
set
st
e
in
dom
b
2
holds
b
2
.
e
=
||.
(
f
/.
e
)
.||
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
||.
NORMSP_0:def 2 :
for
X
being non
empty
N-Str
for
f
being the
carrier
of
b
1
-valued
Function
for
b
3
being
Function
holds
(
b
3
=
||.
f
.||
iff (
dom
b
3
=
dom
f
& ( for
e
being
set
st
e
in
dom
b
3
holds
b
3
.
e
=
||.
(
f
/.
e
)
.||
) ) );
registration
let
X
be non
empty
N-Str
;
let
f
be the
carrier
of
X
-valued
Function
;
cluster
||.
f
.||
->
REAL
-valued
;
coherence
||.
f
.||
is
REAL
-valued
proof
end;
end;
definition
let
C
be non
empty
set
;
let
X
be non
empty
N-Str
;
let
f
be
PartFunc
of
C
, the
carrier
of
X
;
:: original:
||.
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
)
.||
) );
coherence
||.
f
.||
is
PartFunc
of
C
,
REAL
proof
end;
compatibility
for
b
1
being
PartFunc
of
C
,
REAL
holds
(
b
1
=
||.
f
.||
iff (
dom
b
1
=
dom
f
& ( for
c
being
Element
of
C
st
c
in
dom
b
1
holds
b
1
.
c
=
||.
(
f
/.
c
)
.||
) ) )
proof
end;
end;
::
deftheorem
defines
||.
NORMSP_0:def 3 :
for
C
being non
empty
set
for
X
being non
empty
N-Str
for
f
being
PartFunc
of
C
, the
carrier
of
X
for
b
4
being
PartFunc
of
C
,
REAL
holds
(
b
4
=
||.
f
.||
iff (
dom
b
4
=
dom
f
& ( for
c
being
Element
of
C
st
c
in
dom
b
4
holds
b
4
.
c
=
||.
(
f
/.
c
)
.||
) ) );
definition
let
X
be non
empty
N-Str
;
let
s
be
sequence
of
X
;
:: original:
||.
redefine
func
||.
s
.||
->
Real_Sequence
means
:: NORMSP_0:def 4
for
n
being
Element
of
NAT
holds
it
.
n
=
||.
(
s
.
n
)
.||
;
coherence
||.
s
.||
is
Real_Sequence
proof
end;
compatibility
for
b
1
being
Real_Sequence
holds
(
b
1
=
||.
s
.||
iff for
n
being
Element
of
NAT
holds
b
1
.
n
=
||.
(
s
.
n
)
.||
)
proof
end;
end;
::
deftheorem
defines
||.
NORMSP_0:def 4 :
for
X
being non
empty
N-Str
for
s
being
sequence
of
X
for
b
3
being
Real_Sequence
holds
(
b
3
=
||.
s
.||
iff for
n
being
Element
of
NAT
holds
b
3
.
n
=
||.
(
s
.
n
)
.||
);
definition
attr
c
1
is
strict
;
struct
N-ZeroStr
->
N-Str
,
ZeroStr
;
aggr
N-ZeroStr
(#
carrier
,
ZeroF
,
normF
#)
->
N-ZeroStr
;
end;
registration
cluster
non
empty
strict
for
N-ZeroStr
;
existence
ex
b
1
being
N-ZeroStr
st
( not
b
1
is
empty
&
b
1
is
strict
)
proof
end;
end;
definition
let
X
be non
empty
N-ZeroStr
;
attr
X
is
discerning
means
:: NORMSP_0:def 5
for
x
being
Element
of
X
st
||.
x
.||
=
0
holds
x
=
0.
X
;
attr
X
is
reflexive
means
:
Def6
:
:: NORMSP_0:def 6
||.
(
0.
X
)
.||
=
0
;
end;
::
deftheorem
defines
discerning
NORMSP_0:def 5 :
for
X
being non
empty
N-ZeroStr
holds
(
X
is
discerning
iff for
x
being
Element
of
X
st
||.
x
.||
=
0
holds
x
=
0.
X
);
::
deftheorem
Def6
defines
reflexive
NORMSP_0:def 6 :
for
X
being non
empty
N-ZeroStr
holds
(
X
is
reflexive
iff
||.
(
0.
X
)
.||
=
0
);
registration
cluster
non
empty
strict
discerning
reflexive
for
N-ZeroStr
;
existence
ex
b
1
being non
empty
strict
N-ZeroStr
st
(
b
1
is
reflexive
&
b
1
is
discerning
)
proof
end;
end;
registration
let
X
be non
empty
reflexive
N-ZeroStr
;
cluster
||.
(
0.
X
)
.||
->
zero
;
coherence
||.
(
0.
X
)
.||
is
empty
by
Def6
;
end;