:: Tietze Extension Theorem for $n$-dimensional Spaces
:: by Karol P\kak
::
:: Copyright (c) 2014-2018 Association of Mizar Users

registration
coherence
for b1 being FinSequence st b1 is empty holds
b1 is nonnegative-yielding
proof end;
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,();
coherence
<:F:> is Function of X,()
proof end;
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
proof end;

definition
let n be Nat;
let p be Point of ();
let r be Real;
func OpenHypercube (p,r) -> open Subset of () means :Def1: :: TIETZE_2:def 1
ex e being Point of () st
( p = e & it = OpenHypercube (e,r) );
existence
ex b1 being open Subset of () ex e being Point of () st
( p = e & b1 = OpenHypercube (e,r) )
proof end;
uniqueness
for b1, b2 being open Subset of () st ex e being Point of () st
( p = e & b1 = OpenHypercube (e,r) ) & ex e being Point of () st
( p = e & b2 = OpenHypercube (e,r) ) holds
b1 = b2
;
end;

:: deftheorem Def1 defines OpenHypercube TIETZE_2:def 1 :
for n being Nat
for p being Point of ()
for r being Real
for b4 being open Subset of () holds
( b4 = OpenHypercube (p,r) iff ex e being Point of () st
( p = e & b4 = OpenHypercube (e,r) ) );

theorem Th1: :: TIETZE_2:2
for n, i being Nat
for p, q being Point of ()
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 ()
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 ()
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 ();
let R be real-valued FinSequence;
func ClosedHypercube (p,R) -> Subset of () means :Def2: :: TIETZE_2:def 2
for q being Point of () 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
ex b1 being Subset of () st
for q being Point of () holds
( q in b1 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for q being Point of () holds
( q in b1 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 () holds
( q in b2 iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ClosedHypercube TIETZE_2:def 2 :
for n being Nat
for p being Point of ()
for R being real-valued FinSequence
for b4 being Subset of () holds
( b4 = ClosedHypercube (p,R) iff for q being Point of () holds
( q in b4 iff for i being Nat st i in Seg n holds
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 ()
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 ()
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 ();
let R be real-valued nonnegative-yielding FinSequence;
cluster ClosedHypercube (p,R) -> non empty ;
coherence
not ClosedHypercube (p,R) is empty
proof end;
end;

registration
let n be Nat;
let p be Point of ();
let R be real-valued FinSequence;
coherence
( ClosedHypercube (p,R) is convex & ClosedHypercube (p,R) is compact )
proof end;
end;

theorem Th6: :: TIETZE_2:7
for n, i being Nat
for p, q being Point of ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ()
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 ();
let r be positive Real;
cluster ClosedHypercube (p,(n |-> r)) -> non boundary ;
coherence
not ClosedHypercube (p,(n |-> r)) is boundary
proof end;
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
proof end;

theorem Th15: :: TIETZE_2:16
for n, m being Nat
for pn being Point of ()
for pm being Point of ()
for r, s being Real st r > 0 & s > 0 holds
ex h being Function of [:(() | (ClosedHypercube (pn,(n |-> r)))),(() | (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 ()
for pm being Point of ()
for r, s being Real st r > 0 & s > 0 holds
for f being Function of T1,(() | (ClosedHypercube (pn,(n |-> r))))
for g being Function of T2,(() | (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;
cluster functional convex non boundary compact V256() V257() V258() for Subset of ();
existence
ex b1 being Subset of () st
( not b1 is boundary & b1 is convex & b1 is compact )
proof end;
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 ()
for B being convex non boundary compact Subset of ()
for C being convex non boundary compact Subset of (TOP-REAL (n + m))
for f being Function of T1,(() | A)
for g being Function of T2,(() | 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 ()
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 ()
for pm being Point of ()
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 ()
for pm being Point of () st r > 0 & s > 0 & T1,() | (Ball (pn,r)) are_homeomorphic & T2,() | (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 () st V is open holds
for e being Point of () 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
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),(() | (ClosedHypercube ((0. ()),(n |-> 1)))) st f is continuous holds
ex g being Function of T,(() | (ClosedHypercube ((0. ()),(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 () st X is compact & not X is boundary & X is convex holds
for f being Function of (T | A),(() | X) st f is continuous holds
ex g being Function of T,(() | X) st
( g is continuous & g | A = f )
proof end;

:: Tietze Extension Theorem for n-dimensional spaces
:: The First Implication
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 () 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;

:: The Second Implication
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 () 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;