:: Real Normed Space
:: by Jan Popio{\l}ek
::
:: Received September 20, 1990
:: Copyright (c) 1990 Association of Mizar Users
deffunc H1( NORMSTR ) -> Element of the carrier of $1 = 0. $1;
:: deftheorem defines ||. NORMSP_1:def 1 :
consider V being RealLinearSpace;
Lm1:
the carrier of ((0). V) = {(0. V)}
by RLSUB_1:def 3;
reconsider niltonil = the carrier of ((0). V) --> 0 as Function of the carrier of ((0). V), REAL by FUNCOP_1:57;
0. V is VECTOR of ((0). V)
by Lm1, TARSKI:def 1;
then Lm2:
niltonil . (0. V) = 0
by FUNCOP_1:13;
Lm3:
for u being VECTOR of ((0). V)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
Lm4:
for u, v being VECTOR of ((0). V) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = NORMSTR(# the carrier of ((0). V),(0. ((0). V)),the addF of ((0). V),the Mult of ((0). V),niltonil #) as non empty NORMSTR ;
:: deftheorem Def2 defines RealNormSpace-like NORMSP_1:def 2 :
theorem :: NORMSP_1:1
canceled;
theorem :: NORMSP_1:2
canceled;
theorem :: NORMSP_1:3
canceled;
theorem :: NORMSP_1:4
canceled;
theorem :: NORMSP_1:5
theorem Th6: :: NORMSP_1:6
theorem Th7: :: NORMSP_1:7
theorem Th8: :: NORMSP_1:8
theorem :: NORMSP_1:9
theorem Th10: :: NORMSP_1:10
theorem Th11: :: NORMSP_1:11
theorem Th12: :: NORMSP_1:12
theorem Th13: :: NORMSP_1:13
theorem Th14: :: NORMSP_1:14
theorem :: NORMSP_1:15
theorem :: NORMSP_1:16
canceled;
theorem :: NORMSP_1:17
theorem :: NORMSP_1:18
canceled;
theorem :: NORMSP_1:19
theorem :: NORMSP_1:20
theorem :: NORMSP_1:21
theorem :: NORMSP_1:22
theorem :: NORMSP_1:23
theorem :: NORMSP_1:24
theorem :: NORMSP_1:25
canceled;
theorem :: NORMSP_1:26
canceled;
theorem :: NORMSP_1:27
canceled;
Lm6:
for RNS being non empty 1-sorted
for S being sequence of RNS
for n being Element of NAT holds S . n is Element of RNS
;
:: deftheorem NORMSP_1:def 3 :
canceled;
:: deftheorem NORMSP_1:def 4 :
canceled;
:: deftheorem Def5 defines + NORMSP_1:def 5 :
:: deftheorem Def6 defines - NORMSP_1:def 6 :
:: deftheorem Def7 defines - NORMSP_1:def 7 :
:: deftheorem Def8 defines * NORMSP_1:def 8 :
:: deftheorem Def9 defines convergent NORMSP_1:def 9 :
theorem :: NORMSP_1:28
canceled;
theorem :: NORMSP_1:29
canceled;
theorem :: NORMSP_1:30
canceled;
theorem :: NORMSP_1:31
canceled;
theorem :: NORMSP_1:32
canceled;
theorem :: NORMSP_1:33
canceled;
theorem Th34: :: NORMSP_1:34
theorem Th35: :: NORMSP_1:35
theorem Th36: :: NORMSP_1:36
theorem Th37: :: NORMSP_1:37
:: deftheorem Def10 defines ||. NORMSP_1:def 10 :
theorem :: NORMSP_1:38
canceled;
theorem Th39: :: NORMSP_1:39
:: deftheorem Def11 defines lim NORMSP_1:def 11 :
theorem :: NORMSP_1:40
canceled;
theorem :: NORMSP_1:41
theorem :: NORMSP_1:42
theorem :: NORMSP_1:43
theorem :: NORMSP_1:44
theorem :: NORMSP_1:45