let n be Nat; for k being FinSequence of NAT
for S being non empty strict compact TopSpace
for X being non empty Subset of (REAL-NS (k . 1))
for T being NormedLinearTopSpace st S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let k be FinSequence of NAT ; for S being non empty strict compact TopSpace
for X being non empty Subset of (REAL-NS (k . 1))
for T being NormedLinearTopSpace st S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let S be non empty strict compact TopSpace; for X being non empty Subset of (REAL-NS (k . 1))
for T being NormedLinearTopSpace st S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let X be non empty Subset of (REAL-NS (k . 1)); for T being NormedLinearTopSpace st S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let T be NormedLinearTopSpace; ( S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) implies for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact )
assume A1:
( S is SubSpace of TopSpaceNorm (REAL-NS (k . 1)) & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) )
; for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let G be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); for D, K being Real st 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is compact
let D, K be Real; ( 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } implies Cl G is compact )
assume A2:
( 0 < D & 0 < K & G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } )
; Cl G is compact
set K1 = K + 1;
set D1 = (D |^ n) + 1;
A3:
0 <= D |^ n
by A2, POWER:3;
for F being Function of X,T st F in G holds
( ( for x, y being Point of (REAL-NS (k . 1)) st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).|| ) & ( for x being Point of (REAL-NS (k . 1)) st x in X holds
||.(F /. x).|| <= K + 1 ) )
proof
let F be
Function of
X,
T;
( F in G implies ( ( for x, y being Point of (REAL-NS (k . 1)) st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).|| ) & ( for x being Point of (REAL-NS (k . 1)) st x in X holds
||.(F /. x).|| <= K + 1 ) ) )
assume
F in G
;
( ( for x, y being Point of (REAL-NS (k . 1)) st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).|| ) & ( for x being Point of (REAL-NS (k . 1)) st x in X holds
||.(F /. x).|| <= K + 1 ) )
then
F in { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) }
by A2;
then consider F0 being
Function of
(REAL-NS (k . 1)),
(REAL-NS (k . (n + 1))) such that A4:
(
F = F0 | X & ex
N being non
empty FinSequence st
(
N is_LayerFunc_Seq D,
K,
k,
n &
F0 = OutPutFunc (
N,
k,
n) ) )
;
consider N being non
empty FinSequence such that A5:
(
N is_LayerFunc_Seq D,
K,
k,
n &
F0 = OutPutFunc (
N,
k,
n) )
by A4;
A6:
F0 is_LayerFunc D |^ n,
K
by Th34, A5, A2;
A7:
dom F = X
by FUNCT_2:def 1;
thus
for
x,
y being
Point of
(REAL-NS (k . 1)) st
x in X &
y in X holds
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).||
for x being Point of (REAL-NS (k . 1)) st x in X holds
||.(F /. x).|| <= K + 1proof
let x,
y be
Point of
(REAL-NS (k . 1));
( x in X & y in X implies ||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).|| )
assume A8:
(
x in X &
y in X )
;
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).||
then A9:
F /. x =
F . x
by A7, PARTFUN1:def 6
.=
F0 . x
by A4, A8, FUNCT_1:49
;
A10:
F /. y =
F . y
by A7, A8, PARTFUN1:def 6
.=
F0 . y
by A4, A8, FUNCT_1:49
;
RLSStruct(# the
carrier of
(REAL-NS (k . (n + 1))), the
ZeroF of
(REAL-NS (k . (n + 1))), the
addF of
(REAL-NS (k . (n + 1))), the
Mult of
(REAL-NS (k . (n + 1))) #)
= RLSStruct(# the
carrier of
T, the
ZeroF of
T, the
addF of
T, the
Mult of
T #)
by A1;
then
||.((F0 . x) - (F0 . y)).|| = ||.((F /. x) - (F /. y)).||
by A1, A9, A10, Th5;
then A12:
||.((F /. x) - (F /. y)).|| <= (D |^ n) * ||.(x - y).||
by A6;
(D |^ n) + 0 < (D |^ n) + 1
by XREAL_1:8;
then
(D |^ n) * ||.(x - y).|| <= ((D |^ n) + 1) * ||.(x - y).||
by XREAL_1:64;
hence
||.((F /. x) - (F /. y)).|| <= ((D |^ n) + 1) * ||.(x - y).||
by A12, XXREAL_0:2;
verum
end;
let x be
Point of
(REAL-NS (k . 1));
( x in X implies ||.(F /. x).|| <= K + 1 )
assume A13:
x in X
;
||.(F /. x).|| <= K + 1
then F /. x =
F . x
by A7, PARTFUN1:def 6
.=
F0 . x
by A4, A13, FUNCT_1:49
;
then
||.(F0 . x).|| = ||.(F /. x).||
by A1;
then A15:
||.(F /. x).|| <= K
by A6;
K + 0 < K + 1
by XREAL_1:8;
hence
||.(F /. x).|| <= K + 1
by A15, XXREAL_0:2;
verum
end;
hence
Cl G is compact
by Th29, A1, A3, A2; verum