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

registration

cluster Relation-like empty Function-like FinSequence-like -> nonnegative-yielding for set ;

coherence
for b₁ being FinSequence st b₁ is empty holds
b₁ 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,(TOP-REAL n);
coherence
<:F:> is Function of X,(TOP-REAL n)

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 (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 b₁ being open Subset of (TOP-REAL n) ex e being Point of (Euclid n) st
( p = e & b₁ = OpenHypercube (e,r) )

proof end;

uniqueness
for b₁, b₂ being open Subset of (TOP-REAL n) st ex e being Point of (Euclid n) st
( p = e & b₁ = OpenHypercube (e,r) ) & ex e being Point of (Euclid n) st
( p = e & b₂ = OpenHypercube (e,r) ) holds
b₁ = b₂ ;

end;

:: 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₄ being open Subset of (TOP-REAL n) holds
( b₄ = OpenHypercube (p,r) iff ex e being Point of (Euclid n) st
( p = e & b₄ = OpenHypercube (e,r) ) );

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)

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).[

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).[ )

proof end;

definition

let n be Nat;
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
ex b₁ being Subset of (TOP-REAL n) st
for q being Point of (TOP-REAL n) holds
( q in b₁ 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 b₁, b₂ being Subset of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds
( q in b₁ 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₂ iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) holds
b₁ = b₂

proof end;

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₄ being Subset of (TOP-REAL n) holds
( b₄ = ClosedHypercube (p,R) iff for q being Point of (TOP-REAL n) holds
( q in b₄ 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 (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)

proof end;

registration

let n be Nat;
let p be Point of (TOP-REAL n);
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 (TOP-REAL n);
let R be real-valued FinSequence;

cluster ClosedHypercube (p,R) -> convex compact ;

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 (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)).]

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)

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) ) ) ) )

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))

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)

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))

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)

proof end;

registration

let n be Nat;
let p be Point of (TOP-REAL n);
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 (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) ) ) )

proof end;

registration

let n be Nat;

cluster functional convex non boundary compact V256() V257() V258() for Element of bool the carrier of (TOP-REAL n);

existence
ex b₁ being Subset of (TOP-REAL n) st
( not b₁ is boundary & b₁ is convex & b₁ 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 (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) )

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

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

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 )

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 )

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 (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;

:: 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 (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;