:: JORDAN2B semantic presentation

Lm1: for n, i being Nat
for p being Element of (TOP-REAL n) ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )

proof end;

Lm2: for n, i being Nat
for p being Element of (TOP-REAL n) ex q being Real st
for g being FinSequence of REAL st g = p holds
q = g /. i

proof end;

definition

let n, i be Nat;
let p be Element of (TOP-REAL n);
func Proj p,i -> Real means :Def1: :: JORDAN2B:def 1
for g being FinSequence of REAL st g = p holds
it = g /. i;
existence by Lm2;
uniqueness

proof end;

end;

:: deftheorem Def1 defines Proj JORDAN2B:def 1 :

theorem :: JORDAN2B:1

for n, i being Nat ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = Proj p,i

proof end;

theorem Th2: :: JORDAN2B:2

for n, i being Nat st i in Seg n holds
(0* n) . i = 0

proof end;

theorem :: JORDAN2B:3

for n, i being Nat st i in Seg n holds
Proj (0.REAL n),i = 0

proof end;

theorem :: JORDAN2B:4

for n being Nat
for r being real number
for p being Point of (TOP-REAL n)
for i being Nat st i in Seg n holds
Proj (r * p),i = r * (Proj p,i)

proof end;

theorem :: JORDAN2B:5

for n being Nat
for p being Point of (TOP-REAL n)
for i being Nat st i in Seg n holds
Proj (- p),i = - (Proj p,i)

proof end;

theorem :: JORDAN2B:6

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for i being Nat st i in Seg n holds
Proj (p1 + p2),i = (Proj p1,i) + (Proj p2,i)

proof end;

theorem Th7: :: JORDAN2B:7

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for i being Nat st i in Seg n holds
Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i)

proof end;

theorem Th8: :: JORDAN2B:8

for n being Nat holds len (0* n) = n by FINSEQ_2:109;

theorem Th9: :: JORDAN2B:9

for i, n being Nat st i <= n holds
(0* n) | i = 0* i

proof end;

theorem Th10: :: JORDAN2B:10

for n, i being Nat holds (0* n) /^ i = 0* (n -' i)

proof end;

theorem Th11: :: JORDAN2B:11

for i being Nat holds Sum (0* i) = 0

proof end;

theorem Th12: :: JORDAN2B:12

for w being FinSequence
for r being set
for i being Nat holds len (w +* i,r) = len w

proof end;

theorem Th13: :: JORDAN2B:13

for i being Nat
for D being non empty set
for w being FinSequence of D
for r being Element of D st i in dom w holds
w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)

proof end;

theorem Th14: :: JORDAN2B:14

for i, n being Nat
for r being Real st i in Seg n holds
Sum ((0* n) +* i,r) = r

proof end;

theorem Th15: :: JORDAN2B:15

for n being Nat
for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Nat st i in Seg n & q = p holds
( Proj p,i <= |.q.| & (Proj p,i) ^2 <= |.q.| ^2 )

proof end;

theorem Th16: :: JORDAN2B:16

for n being Nat
for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Nat st P = { p where p is Point of (TOP-REAL n) : s1 > Proj p,i } & i in Seg n holds
P is open

proof end;

theorem Th17: :: JORDAN2B:17

for n being Nat
for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Nat st P = { p where p is Point of (TOP-REAL n) : s1 < Proj p,i } & i in Seg n holds
P is open

proof end;

theorem Th18: :: JORDAN2B:18

for n being Nat
for P being Subset of (TOP-REAL n)
for a, b being real number
for i being Nat st P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n holds
P is open

proof end;

theorem Th19: :: JORDAN2B:19

for n being Nat
for a, b being real number
for f being Function of (TOP-REAL n),R^1
for i being Nat st ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }

proof end;

theorem Th20: :: JORDAN2B:20

for X being non empty TopSpace
for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of the carrier of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball u,r holds
f " P is open ) holds
f is continuous

proof end;

theorem Th21: :: JORDAN2B:21

for u being Point of RealSpace
for r, u1 being real number st u1 = u & r > 0 holds
Ball u,r = { s where s is Real : ( u1 - r < s & s < u1 + r ) }

proof end;

theorem Th22: :: JORDAN2B:22

for n being Nat
for f being Function of (TOP-REAL n),R^1
for i being Nat st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f is continuous

proof end;

theorem :: JORDAN2B:23

for s being Real holds abs <*s*> = <*(abs s)*>

proof end;

theorem Th24: :: JORDAN2B:24

for p being Element of (TOP-REAL 1) ex r being Real st p = <*r*>

proof end;

theorem Th25: :: JORDAN2B:25

for w being Element of (Euclid 1) ex r being Real st w = <*r*> by FINSEQ_2:117;

definition

let r be real number ;
func |[r]| -> Point of (TOP-REAL 1) equals :: JORDAN2B:def 2
<*r*>;
coherence

proof end;

end;

:: deftheorem defines |[ JORDAN2B:def 2 :

theorem :: JORDAN2B:26

for r being real number
for s being Real holds s * |[r]| = |[(s * r)]|

proof end;

theorem :: JORDAN2B:27

for r1, r2 being real number holds |[(r1 + r2)]| = |[r1]| + |[r2]|

proof end;

theorem :: JORDAN2B:28

|[0]| = 0.REAL 1 by FINSEQ_2:73;

theorem :: JORDAN2B:29

for r1, r2 being real number st |[r1]| = |[r2]| holds
r1 = r2

proof end;

theorem Th30: :: JORDAN2B:30

for P being Subset of R^1
for b being real number st P = { s where s is Real : s < b } holds
P is open

proof end;

theorem Th31: :: JORDAN2B:31

for P being Subset of R^1
for a being real number st P = { s where s is Real : a < s } holds
P is open

proof end;

theorem Th32: :: JORDAN2B:32

for P being Subset of R^1
for a, b being real number st P = { s where s is Real : ( a < s & s < b ) } holds
P is open

proof end;

theorem Th33: :: JORDAN2B:33

for u being Point of (Euclid 1)
for r, u1 being real number st <*u1*> = u & r > 0 holds
Ball u,r = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }

proof end;

theorem :: JORDAN2B:34

for f being Function of (TOP-REAL 1),R^1 st ( for p being Element of (TOP-REAL 1) holds f . p = Proj p,1 ) holds
f is_homeomorphism

proof end;

theorem Th35: :: JORDAN2B:35

for p being Element of (TOP-REAL 2) holds
( Proj p,1 = p `1 & Proj p,2 = p `2 )

proof end;

theorem :: JORDAN2B:36

for p being Element of (TOP-REAL 2) holds
( Proj p,1 = proj1 . p & Proj p,2 = proj2 . p )

proof end;