:: by Roman Matuszewski and Yatsuka Nakamura

::

:: Received November 3, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

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;

registration

let n be Nat;

coherence

for b_{1} being Element of (TOP-REAL n) holds b_{1} is REAL -valued

end;
coherence

for b

proof end;

theorem :: JORDAN2B:1

for i being Element of NAT

for n being Nat ex f being Function of (TOP-REAL n),R^1 st

for p being Element of (TOP-REAL n) holds f . p = p /. i

for n being Nat ex f being Function of (TOP-REAL n),R^1 st

for p being Element of (TOP-REAL n) holds f . p = p /. i

proof end;

theorem :: JORDAN2B:3

for n being Element of NAT

for r being Real

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(r * p) /. i = r * (p /. i)

for r being Real

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(r * p) /. i = r * (p /. i)

proof end;

theorem :: JORDAN2B:4

for n being Element of NAT

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(- p) /. i = - (p /. i)

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(- p) /. i = - (p /. i)

proof end;

theorem :: JORDAN2B:5

for n being Element of NAT

for p1, p2 being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(p1 + p2) /. i = (p1 /. i) + (p2 /. i)

for p1, p2 being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(p1 + p2) /. i = (p1 /. i) + (p2 /. i)

proof end;

theorem Th6: :: JORDAN2B:6

for n being Element of NAT

for p1, p2 being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(p1 - p2) /. i = (p1 /. i) - (p2 /. i)

for p1, p2 being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n holds

(p1 - p2) /. i = (p1 /. i) - (p2 /. i)

proof end;

theorem Th11: :: JORDAN2B:11

for n being Element of NAT

for q being Element of REAL n

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n & q = p holds

( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )

for q being Element of REAL n

for p being Point of (TOP-REAL n)

for i being Element of NAT st i in Seg n & q = p holds

( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )

proof end;

theorem Th12: :: JORDAN2B:12

for n being Element of NAT

for s1 being Real

for P being Subset of (TOP-REAL n)

for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 > p /. i } & i in Seg n holds

P is open

for s1 being Real

for P being Subset of (TOP-REAL n)

for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 > p /. i } & i in Seg n holds

P is open

proof end;

theorem Th13: :: JORDAN2B:13

for n being Element of NAT

for s1 being Real

for P being Subset of (TOP-REAL n)

for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds

P is open

for s1 being Real

for P being Subset of (TOP-REAL n)

for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds

P is open

proof end;

theorem Th14: :: JORDAN2B:14

for n being Element of NAT

for P being Subset of (TOP-REAL n)

for a, b being Real

for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } & i in Seg n holds

P is open

for P being Subset of (TOP-REAL n)

for a, b being Real

for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } & i in Seg n holds

P is open

proof end;

theorem Th15: :: JORDAN2B:15

for n being Element of NAT

for a, b being Real

for f being Function of (TOP-REAL n),R^1

for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds

f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }

for a, b being Real

for f being Function of (TOP-REAL n),R^1

for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds

f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }

proof end;

theorem Th16: :: JORDAN2B:16

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

for u being Element 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

for M being non empty MetrSpace

for f being Function of X,(TopSpaceMetr M) st ( for r being Real

for u being Element 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 Th17: :: JORDAN2B:17

for u being Point of RealSpace

for r, u1 being Real st u1 = u holds

Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }

for r, u1 being Real st u1 = u holds

Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }

proof end;

theorem Th18: :: JORDAN2B:18

for n being Element of NAT

for f being Function of (TOP-REAL n),R^1

for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds

f is continuous

for f being Function of (TOP-REAL n),R^1

for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds

f is continuous

proof end;

definition

let r be Real;

:: original: |[

redefine func |[r]| -> Point of (TOP-REAL 1);

coherence

|[r]| is Point of (TOP-REAL 1)

end;
:: original: |[

redefine func |[r]| -> Point of (TOP-REAL 1);

coherence

|[r]| is Point of (TOP-REAL 1)

proof end;

theorem Th26: :: JORDAN2B:26

for P being Subset of R^1

for a, b being Real st P = { s where s is Real : ( a < s & s < b ) } holds

P is open

for a, b being Real st P = { s where s is Real : ( a < s & s < b ) } holds

P is open

proof end;

theorem Th27: :: JORDAN2B:27

for u being Point of (Euclid 1)

for r, u1 being Real st <*u1*> = u holds

Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }

for r, u1 being Real st <*u1*> = u holds

Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }

proof end;

theorem :: JORDAN2B:28

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

f is being_homeomorphism

f is being_homeomorphism

proof end;