:: by Karol P\kak

::

:: Received February 11, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

registration

coherence

for b_{1} being FinSequence st b_{1} is empty holds

b_{1} is nonnegative-yielding

end;
for b

b

proof end;

definition

let n be non zero Nat;

let X be set ;

let F be Element of n -tuples_on (Funcs (X, the carrier of R^1));

:: original: <:

redefine func <:F:> -> Function of X,(TOP-REAL n);

coherence

<:F:> is Function of X,(TOP-REAL n)

end;
let X be set ;

let F be Element of n -tuples_on (Funcs (X, the carrier of R^1));

:: original: <:

redefine func <:F:> -> Function of X,(TOP-REAL n);

coherence

<:F:> is Function of X,(TOP-REAL n)

proof end;

theorem Th20: :: TIETZE_2:1

for X, Y being set

for F being Function-yielding Function

for x, y being object st ( F is Funcs (X,Y) -valued or y in dom <:F:> ) holds

(F . x) . y = (<:F:> . y) . x

for F being Function-yielding Function

for x, y being object st ( F is Funcs (X,Y) -valued or y in dom <:F:> ) holds

(F . x) . y = (<:F:> . y) . x

proof end;

definition

let n be Nat;

let p be Point of (TOP-REAL n);

let r be Real;

ex b_{1} being open Subset of (TOP-REAL n) ex e being Point of (Euclid n) st

( p = e & b_{1} = OpenHypercube (e,r) )

for b_{1}, b_{2} being open Subset of (TOP-REAL n) st ex e being Point of (Euclid n) st

( p = e & b_{1} = OpenHypercube (e,r) ) & ex e being Point of (Euclid n) st

( p = e & b_{2} = OpenHypercube (e,r) ) holds

b_{1} = b_{2}
;

end;
let p be Point of (TOP-REAL n);

let r be Real;

func OpenHypercube (p,r) -> open Subset of (TOP-REAL n) means :Def1: :: TIETZE_2:def 1

ex e being Point of (Euclid n) st

( p = e & it = OpenHypercube (e,r) );

existence ex e being Point of (Euclid n) st

( p = e & it = OpenHypercube (e,r) );

ex b

( p = e & b

proof end;

uniqueness for b

( p = e & b

( p = e & b

b

:: deftheorem Def1 defines OpenHypercube TIETZE_2:def 1 :

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real

for b_{4} being open Subset of (TOP-REAL n) holds

( b_{4} = OpenHypercube (p,r) iff ex e being Point of (Euclid n) st

( p = e & b_{4} = OpenHypercube (e,r) ) );

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real

for b

( b

( p = e & b

theorem Th1: :: TIETZE_2:2

for n, i being Nat

for p, q being Point of (TOP-REAL n)

for r, s being Real st q in OpenHypercube (p,r) & s in ].((p . i) - r),((p . i) + r).[ holds

q +* (i,s) in OpenHypercube (p,r)

for p, q being Point of (TOP-REAL n)

for r, s being Real st q in OpenHypercube (p,r) & s in ].((p . i) - r),((p . i) + r).[ holds

q +* (i,s) in OpenHypercube (p,r)

proof end;

theorem Th2: :: TIETZE_2:3

for n, i being Nat

for p being Point of (TOP-REAL n)

for r being Real st i in Seg n holds

(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[

for p being Point of (TOP-REAL n)

for r being Real st i in Seg n holds

(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((p . i) - r),((p . i) + r).[

proof end;

theorem Th3: :: TIETZE_2:4

for n being Nat

for p, q being Point of (TOP-REAL n)

for r being Real holds

( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds

q . i in ].((p . i) - r),((p . i) + r).[ )

for p, q being Point of (TOP-REAL n)

for r being Real holds

( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds

q . i in ].((p . i) - r),((p . i) + r).[ )

proof end;

definition

let n be Nat;

let p be Point of (TOP-REAL n);

let R be real-valued FinSequence;

ex b_{1} being Subset of (TOP-REAL n) st

for q being Point of (TOP-REAL n) holds

( q in b_{1} iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )

for b_{1}, b_{2} being Subset of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds

( q in b_{1} iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) & ( for q being Point of (TOP-REAL n) holds

( q in b_{2} iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) holds

b_{1} = b_{2}

end;
let p be Point of (TOP-REAL n);

let R be real-valued FinSequence;

func ClosedHypercube (p,R) -> Subset of (TOP-REAL n) means :Def2: :: TIETZE_2:def 2

for q being Point of (TOP-REAL n) holds

( q in it iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] );

existence for q being Point of (TOP-REAL n) holds

( q in it iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] );

ex b

for q being Point of (TOP-REAL n) holds

( q in b

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )

proof end;

uniqueness for b

( q in b

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) & ( for q being Point of (TOP-REAL n) holds

( q in b

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) holds

b

proof end;

:: deftheorem Def2 defines ClosedHypercube TIETZE_2:def 2 :

for n being Nat

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence

for b_{4} being Subset of (TOP-REAL n) holds

( b_{4} = ClosedHypercube (p,R) iff for q being Point of (TOP-REAL n) holds

( q in b_{4} iff for i being Nat st i in Seg n holds

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) );

for n being Nat

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence

for b

( b

( q in b

q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) );

theorem Th4: :: TIETZE_2:5

for n being Nat

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st ex i being Nat st

( i in (Seg n) /\ (dom R) & R . i < 0 ) holds

ClosedHypercube (p,R) is empty

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st ex i being Nat st

( i in (Seg n) /\ (dom R) & R . i < 0 ) holds

ClosedHypercube (p,R) is empty

proof end;

theorem Th5: :: TIETZE_2:6

for n being Nat

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st ( for i being Nat st i in (Seg n) /\ (dom R) holds

R . i >= 0 ) holds

p in ClosedHypercube (p,R)

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st ( for i being Nat st i in (Seg n) /\ (dom R) holds

R . i >= 0 ) holds

p in ClosedHypercube (p,R)

proof end;

registration

let n be Nat;

let p be Point of (TOP-REAL n);

let R be real-valued nonnegative-yielding FinSequence;

coherence

not ClosedHypercube (p,R) is empty

end;
let p be Point of (TOP-REAL n);

let R be real-valued nonnegative-yielding FinSequence;

coherence

not ClosedHypercube (p,R) is empty

proof end;

registration

let n be Nat;

let p be Point of (TOP-REAL n);

let R be real-valued FinSequence;

coherence

( ClosedHypercube (p,R) is convex & ClosedHypercube (p,R) is compact )

end;
let p be Point of (TOP-REAL n);

let R be real-valued FinSequence;

coherence

( ClosedHypercube (p,R) is convex & ClosedHypercube (p,R) is compact )

proof end;

theorem Th6: :: TIETZE_2:7

for n, i being Nat

for p, q being Point of (TOP-REAL n)

for r being Real

for R being real-valued FinSequence st i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] holds

q +* (i,r) in ClosedHypercube (p,R)

for p, q being Point of (TOP-REAL n)

for r being Real

for R being real-valued FinSequence st i in Seg n & q in ClosedHypercube (p,R) & r in [.((p . i) - (R . i)),((p . i) + (R . i)).] holds

q +* (i,r) in ClosedHypercube (p,R)

proof end;

theorem Th7: :: TIETZE_2:8

for n, i being Nat

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st i in Seg n & not ClosedHypercube (p,R) is empty holds

(PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]

for p being Point of (TOP-REAL n)

for R being real-valued FinSequence st i in Seg n & not ClosedHypercube (p,R) is empty holds

(PROJ (n,i)) .: (ClosedHypercube (p,R)) = [.((p . i) - (R . i)),((p . i) + (R . i)).]

proof end;

theorem Th8: :: TIETZE_2:9

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real

for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds

OpenHypercube (p,r) c= ClosedHypercube (p,R)

for p being Point of (TOP-REAL n)

for r being Real

for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds

OpenHypercube (p,r) c= ClosedHypercube (p,R)

proof end;

theorem Th9: :: TIETZE_2:10

for n being Nat

for p, q being Point of (TOP-REAL n)

for R being real-valued FinSequence holds

( q in Fr (ClosedHypercube (p,R)) iff ( q in ClosedHypercube (p,R) & ex i being Nat st

( i in Seg n & ( q . i = (p . i) - (R . i) or q . i = (p . i) + (R . i) ) ) ) )

for p, q being Point of (TOP-REAL n)

for R being real-valued FinSequence holds

( q in Fr (ClosedHypercube (p,R)) iff ( q in ClosedHypercube (p,R) & ex i being Nat st

( i in Seg n & ( q . i = (p . i) - (R . i) or q . i = (p . i) + (R . i) ) ) ) )

proof end;

theorem :: TIETZE_2:11

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r >= 0 holds

p in ClosedHypercube (p,(n |-> r))

for p being Point of (TOP-REAL n)

for r being Real st r >= 0 holds

p in ClosedHypercube (p,(n |-> r))

proof end;

theorem Th11: :: TIETZE_2:12

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r)

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r)

proof end;

theorem Th12: :: TIETZE_2:13

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real holds OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))

for p being Point of (TOP-REAL n)

for r being Real holds OpenHypercube (p,r) c= ClosedHypercube (p,(n |-> r))

proof end;

theorem :: TIETZE_2:14

for n being Nat

for p being Point of (TOP-REAL n)

for r, s being Real st r < s holds

ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)

for p being Point of (TOP-REAL n)

for r, s being Real st r < s holds

ClosedHypercube (p,(n |-> r)) c= OpenHypercube (p,s)

proof end;

registration

let n be Nat;

let p be Point of (TOP-REAL n);

let r be positive Real;

coherence

not ClosedHypercube (p,(n |-> r)) is boundary

end;
let p be Point of (TOP-REAL n);

let r be positive Real;

coherence

not ClosedHypercube (p,(n |-> r)) is boundary

proof end;

theorem Th14: :: TIETZE_2:15

for T1, T2, S1, S2 being non empty TopSpace

for f being Function of T1,T2

for g being Function of S1,S2 st f is being_homeomorphism & g is being_homeomorphism holds

[:f,g:] is being_homeomorphism

for f being Function of T1,T2

for g being Function of S1,S2 st f is being_homeomorphism & g is being_homeomorphism holds

[:f,g:] is being_homeomorphism

proof end;

theorem Th15: :: TIETZE_2:16

for n, m being Nat

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

ex h being Function of [:((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))),((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))):],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st

( h is being_homeomorphism & h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1) )

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

ex h being Function of [:((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))),((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))):],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st

( h is being_homeomorphism & h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1) )

proof end;

theorem Th16: :: TIETZE_2:17

for n, m being Nat

for T1, T2 being non empty TopSpace

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

for f being Function of T1,((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r))))

for g being Function of T2,((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))) st f is being_homeomorphism & g is being_homeomorphism holds

ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st

( h is being_homeomorphism & ( for t1 being Point of T1

for t2 being Point of T2 holds

( ( f . t1 in OpenHypercube (pn,r) & g . t2 in OpenHypercube (pm,s) ) iff h . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ) ) )

for T1, T2 being non empty TopSpace

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

for f being Function of T1,((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r))))

for g being Function of T2,((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))) st f is being_homeomorphism & g is being_homeomorphism holds

ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st

( h is being_homeomorphism & ( for t1 being Point of T1

for t2 being Point of T2 holds

( ( f . t1 in OpenHypercube (pn,r) & g . t2 in OpenHypercube (pm,s) ) iff h . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ) ) )

proof end;

registration

let n be Nat;

existence

ex b_{1} being Subset of (TOP-REAL n) st

( not b_{1} is boundary & b_{1} is convex & b_{1} is compact )

end;
existence

ex b

( not b

proof end;

theorem Th17: :: TIETZE_2:18

for n, m being Nat

for T1, T2 being non empty TopSpace

for A being convex non boundary compact Subset of (TOP-REAL n)

for B being convex non boundary compact Subset of (TOP-REAL m)

for C being convex non boundary compact Subset of (TOP-REAL (n + m))

for f being Function of T1,((TOP-REAL n) | A)

for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds

ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st

( h is being_homeomorphism & ( for t1 being Point of T1

for t2 being Point of T2 holds

( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )

for T1, T2 being non empty TopSpace

for A being convex non boundary compact Subset of (TOP-REAL n)

for B being convex non boundary compact Subset of (TOP-REAL m)

for C being convex non boundary compact Subset of (TOP-REAL (n + m))

for f being Function of T1,((TOP-REAL n) | A)

for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds

ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st

( h is being_homeomorphism & ( for t1 being Point of T1

for t2 being Point of T2 holds

( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )

proof end;

Lm1: for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

proof end;

theorem Th18: :: TIETZE_2:19

for n, m being Nat

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

ex h being Function of [:(Tdisk (pn,r)),(Tdisk (pm,s)):],(Tdisk ((0. (TOP-REAL (n + m))),1)) st

( h is being_homeomorphism & h .: [:(Ball (pn,r)),(Ball (pm,s)):] = Ball ((0. (TOP-REAL (n + m))),1) )

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m)

for r, s being Real st r > 0 & s > 0 holds

ex h being Function of [:(Tdisk (pn,r)),(Tdisk (pm,s)):],(Tdisk ((0. (TOP-REAL (n + m))),1)) st

( h is being_homeomorphism & h .: [:(Ball (pn,r)),(Ball (pm,s)):] = Ball ((0. (TOP-REAL (n + m))),1) )

proof end;

theorem :: TIETZE_2:20

for n, m being Nat

for r, s being Real

for T1, T2 being non empty TopSpace

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds

[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic

for r, s being Real

for T1, T2 being non empty TopSpace

for pn being Point of (TOP-REAL n)

for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds

[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic

proof end;

Lm2: for n being Nat

for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds

for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V )

proof end;

theorem Th21: :: TIETZE_2:21

for T being TopSpace

for n being non zero Nat

for F being Element of n -tuples_on (Funcs ( the carrier of T, the carrier of R^1)) st ( for i being Nat st i in dom F holds

for h being Function of T,R^1 st h = F . i holds

h is continuous ) holds

<:F:> is continuous

for n being non zero Nat

for F being Element of n -tuples_on (Funcs ( the carrier of T, the carrier of R^1)) st ( for i being Nat st i in dom F holds

for h being Function of T,R^1 st h = F . i holds

h is continuous ) holds

<:F:> is continuous

proof end;

theorem Th22: :: TIETZE_2:22

for n being Nat

for T being TopSpace

for A being closed Subset of T st T is normal holds

for f being Function of (T | A),((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) st f is continuous holds

ex g being Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) st

( g is continuous & g | A = f )

for T being TopSpace

for A being closed Subset of T st T is normal holds

for f being Function of (T | A),((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) st f is continuous holds

ex g being Function of T,((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) st

( g is continuous & g | A = f )

proof end;

theorem Th23: :: TIETZE_2:23

for n being Nat

for T being TopSpace

for A being closed Subset of T st T is normal holds

for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex holds

for f being Function of (T | A),((TOP-REAL n) | X) st f is continuous holds

ex g being Function of T,((TOP-REAL n) | X) st

( g is continuous & g | A = f )

for T being TopSpace

for A being closed Subset of T st T is normal holds

for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex holds

for f being Function of (T | A),((TOP-REAL n) | X) st f is continuous holds

ex g being Function of T,((TOP-REAL n) | X) st

( g is continuous & g | A = f )

proof end;

theorem :: TIETZE_2:24

for n being Nat

for T, S being TopSpace

for A being closed Subset of T

for B being Subset of S st T is normal holds

for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds

for f being Function of (T | A),(S | B) st f is continuous holds

ex g being Function of T,(S | B) st

( g is continuous & g | A = f )

for T, S being TopSpace

for A being closed Subset of T

for B being Subset of S st T is normal holds

for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds

for f being Function of (T | A),(S | B) st f is continuous holds

ex g being Function of T,(S | B) st

( g is continuous & g | A = f )

proof end;

theorem :: TIETZE_2:25

for T being non empty TopSpace

for n being Nat st n >= 1 & ( for S being TopSpace

for A being non empty closed Subset of T

for B being Subset of S st ex X being Subset of (TOP-REAL n) st

( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds

for f being Function of (T | A),(S | B) st f is continuous holds

ex g being Function of T,(S | B) st

( g is continuous & g | A = f ) ) holds

T is normal

for n being Nat st n >= 1 & ( for S being TopSpace

for A being non empty closed Subset of T

for B being Subset of S st ex X being Subset of (TOP-REAL n) st

( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds

for f being Function of (T | A),(S | B) st f is continuous holds

ex g being Function of T,(S | B) st

( g is continuous & g | A = f ) ) holds

T is normal

proof end;

:: The First Implication