:: Compactness of Neural Networks
:: by Keiichi Miyajima and Hiroshi Yamazaki
::
:: Received April 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

theorem :: NEURONS1:1

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
the carrier of RNS1 = the carrier of RNS2 ;

theorem :: NEURONS1:2

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
0. RNS1 = 0. RNS2 ;

theorem :: NEURONS1:3

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for p, q being Element of RNS1
for f, g being Element of RNS2 st p = f & q = g holds
p + q = f + g ;

theorem :: NEURONS1:4

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for r being Real
for q being Element of RNS1
for g being Element of RNS2 st q = g holds
r * q = r * g ;

theorem Th5: :: NEURONS1:5

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for q being Element of RNS1
for g being Element of RNS2 st q = g holds
- q = - g

proof end;

theorem :: NEURONS1:6

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for p, q being Element of RNS1
for f, g being Element of RNS2 st p = f & q = g holds
p - q = f - g by Th5;

theorem Th7: :: NEURONS1:7

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for X being set
for n being Nat holds
( X is Linear_Combination of RNS2 iff X is Linear_Combination of RNS1 )

proof end;

theorem :: NEURONS1:8

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Lv being Linear_Combination of RNS1
for Lr being Linear_Combination of RNS2 st Lr = Lv holds
Carrier Lr = Carrier Lv ;

theorem :: NEURONS1:9

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for F being set holds
( F is Subset of RNS1 iff F is Subset of RNS2 ) ;

theorem :: NEURONS1:10

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for F being set holds
( F is FinSequence of RNS1 iff F is FinSequence of RNS2 ) ;

theorem :: NEURONS1:11

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for F being set holds
( F is Function of RNS1,REAL iff F is Function of RNS2,REAL ) ;

theorem Th12: :: NEURONS1:12

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for FFr being FinSequence of RNS1
for fr being Function of RNS1,REAL
for Fv being FinSequence of RNS2
for fv being Function of RNS2,REAL st fr = fv & FFr = Fv holds
fr (#) FFr = fv (#) Fv

proof end;

theorem Th13: :: NEURONS1:13

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Ft being FinSequence of RNS1
for FFr being FinSequence of RNS2 st Ft = FFr holds
Sum Ft = Sum FFr

proof end;

theorem Th14: :: NEURONS1:14

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Lr being Linear_Combination of RNS2
for Lt being Linear_Combination of RNS1 st Lr = Lt holds
Sum Lr = Sum Lt

proof end;

theorem :: NEURONS1:15

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Ar being Subset of RNS2
for At being Subset of RNS1 st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )

proof end;

theorem Th16: :: NEURONS1:16

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Ar being Subset of RNS2
for At being Subset of RNS1 st Ar = At holds
[#] (Lin Ar) = [#] (Lin At)

proof end;

theorem Th17: :: NEURONS1:17

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for Ar being Subset of RNS2
for At being Subset of RNS1 st Ar = At holds
( Ar is linearly-independent iff At is linearly-independent )

proof end;

theorem :: NEURONS1:18

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for X being object holds
( X is Subspace of RNS2 iff X is Subspace of RNS1 )

proof end;

theorem :: NEURONS1:19

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for L being Linear_Combination of RNS2
for S being Linear_Combination of RNS1 st L = S holds
Sum L = Sum S

proof end;

theorem Th20: :: NEURONS1:20

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for X being set holds
( X is Basis of RNS1 iff X is Basis of RNS2 )

proof end;

theorem Th21: :: NEURONS1:21

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) & RNS1 is finite-dimensional holds
( RNS2 is finite-dimensional & dim RNS2 = dim RNS1 )

proof end;

theorem Th22: :: NEURONS1:22

for RNS being RealNormSpace holds NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) is strict RealNormSpace

proof end;

theorem Th23: :: NEURONS1:23

for RNS being RealNormSpace ex T being NormedLinearTopSpace st NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #)

proof end;

theorem :: NEURONS1:24

for RNS being RealNormSpace st RNS is finite-dimensional holds
ex T being NormedLinearTopSpace st
( NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & T is finite-dimensional )

proof end;

theorem Th25: :: NEURONS1:25

for T being NormedLinearTopSpace
for RNS being RealNormSpace st T is finite-dimensional & RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
( RNS is finite-dimensional & dim RNS = dim T )

proof end;

theorem Th26: :: NEURONS1:26

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded iff ( G is equibounded & G is equicontinuous ) )

proof end;

theorem Th27: :: NEURONS1:27

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )

proof end;

theorem Th28: :: NEURONS1:28

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) )

proof end;

theorem Th29: :: NEURONS1:29

for RNS being RealNormSpace
for T being NormedLinearTopSpace
for X being non empty Subset of RNS
for S being non empty strict compact TopSpace
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st S is SubSpace of TopSpaceNorm RNS & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & ex K, D being Real st
( 0 < K & 0 < D & ( for F being Function of X,T st F in G holds
( ( for x, y being Point of RNS st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of RNS st x in X holds
||.(F /. x).|| <= K ) ) ) ) holds
Cl G is compact

proof end;

Lm1: ex N being FinSequence ex k being FinSequence of NAT st
( (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) )

proof end;

definition

let n be Nat;
let k be FinSequence of NAT ;
let N be FinSequence;

pred N is_Multilayer_perceptron_with k,n means :: NEURONS1:def 1
( len N = n & (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) );

end;

:: deftheorem defines is_Multilayer_perceptron_with NEURONS1:def 1 :
for n being Nat
for k being FinSequence of NAT
for N being FinSequence holds
( N is_Multilayer_perceptron_with k,n iff ( len N = n & (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) ) );

definition

let N be FinSequence;

attr N is Multilayer_perceptron_like means :Def2: :: NEURONS1:def 2
ex k being FinSequence of NAT st
( (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) );

end;

:: deftheorem Def2 defines Multilayer_perceptron_like NEURONS1:def 2 :
for N being FinSequence holds
( N is Multilayer_perceptron_like iff ex k being FinSequence of NAT st
( (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) ) );

registration

cluster Relation-like -defined Function-like finite FinSequence-like FinSubsequence-like Multilayer_perceptron_like for set ;

existence
ex b₁ being FinSequence st b₁ is Multilayer_perceptron_like

proof end;

end;

definition

mode Multilayer_perceptron is Multilayer_perceptron_like FinSequence;

end;

theorem :: NEURONS1:30

for N being Multilayer_perceptron ex k being FinSequence of NAT st
( (len N) + 1 = len k & ( for i being Nat st 1 <= i & i < len k holds
N . i is Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) ) ) by Def2;

definition

let n be Nat;
let k be FinSequence of NAT ;
let N be FinSequence;
assume A1: N is_Multilayer_perceptron_with k,n ;
assume A2: len N <> 0 ;

func OutPutFunc (N,k,n) -> Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) means :Def3: :: NEURONS1:def 3
ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & it = p . (len N) );

existence
ex b₁ being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & b₁ = p . (len N) )

proof end;

uniqueness
for b₁, b₂ being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) st ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & b₁ = p . (len N) ) & ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & b₂ = p . (len N) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines OutPutFunc NEURONS1:def 3 :
for n being Nat
for k being FinSequence of NAT
for N being FinSequence st N is_Multilayer_perceptron_with k,n & len N <> 0 holds
for b₄ being Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) holds
( b₄ = OutPutFunc (N,k,n) iff ex p being FinSequence st
( len p = len N & p . 1 = N . 1 & ( for i being Nat st 1 <= i & i < len N holds
ex NN being Function of (REAL-NS (k . (i + 1))),(REAL-NS (k . (i + 2))) ex pp being Function of (REAL-NS (k . 1)),(REAL-NS (k . (i + 1))) st
( NN = N . (i + 1) & pp = p . i & p . (i + 1) = NN * pp ) ) & b₄ = p . (len N) ) );

theorem Th31: :: NEURONS1:31

for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st n <> 0 & N is_Multilayer_perceptron_with k,n + 1 holds
ex k1 being FinSequence of NAT ex N1 being non empty FinSequence ex NN being Function of (REAL-NS (k . (n + 1))),(REAL-NS (k . (n + 2))) st
( N1 = N | n & k1 = k | (n + 1) & NN = N . (n + 1) & N1 is_Multilayer_perceptron_with k1,n & OutPutFunc (N,k,(n + 1)) = NN * (OutPutFunc (N1,k1,n)) )

proof end;

definition

let n be Nat;
let k be FinSequence of NAT ;

func NEURONS (n,k) -> Subset of (Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1))))) equals :: NEURONS1:def 4
{ F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } ;

correctness
coherence
{ F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } is Subset of (Funcs ( the carrier of (REAL-NS (k . 1)), the carrier of (REAL-NS (k . (n + 1)))));

proof end;

end;

:: deftheorem defines NEURONS NEURONS1:def 4 :
for n being Nat
for k being FinSequence of NAT holds NEURONS (n,k) = { F where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being FinSequence st
( N is_Multilayer_perceptron_with k,n & F = OutPutFunc (N,k,n) ) } ;

theorem :: NEURONS1:32

for n being Nat
for k being FinSequence of NAT
for S being non empty strict compact TopSpace
for M being non empty SubSpace of MetricSpaceNorm (REAL-NS (k . 1))
for X being non empty Subset of (REAL-NS (k . 1))
for T being NormedLinearTopSpace st S = TopSpaceMetr M & the carrier of M = 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 Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F & G c= { (f | X) where f is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : f in NEURONS (n,k) } holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) ) by Th28;

theorem :: NEURONS1:33

for n being 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)) st G c= { (f | X) where f is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : f in NEURONS (n,k) } & ex K, D being Real st
( 0 < K & 0 < D & ( 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 * ||.(x - y).|| ) & ( for x being Point of (REAL-NS (k . 1)) st x in X holds
||.(F /. x).|| <= K ) ) ) ) holds
Cl G is compact by Th29;

definition

let X, Y be RealNormSpace;
let F be Function of X,Y;
let D, K be Real;

pred F is_LayerFunc D,K means :: NEURONS1:def 5
( ( for x, y being Point of X holds ||.((F . x) - (F . y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of X holds ||.(F . x).|| <= K ) );

end;

:: deftheorem defines is_LayerFunc NEURONS1:def 5 :
for X, Y being RealNormSpace
for F being Function of X,Y
for D, K being Real holds
( F is_LayerFunc D,K iff ( ( for x, y being Point of X holds ||.((F . x) - (F . y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of X holds ||.(F . x).|| <= K ) ) );

definition

let n be Nat;
let k be FinSequence of NAT ;
let D, K be Real;
let N be FinSequence;

pred N is_LayerFunc_Seq D,K,k,n means :: NEURONS1:def 6
( len N = n & N is_Multilayer_perceptron_with k,n & ( for i being Nat st 1 <= i & i < len k holds
ex Ni being Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) st
( N . i = Ni & Ni is_LayerFunc D,K ) ) );

end;

:: deftheorem defines is_LayerFunc_Seq NEURONS1:def 6 :
for n being Nat
for k being FinSequence of NAT
for D, K being Real
for N being FinSequence holds
( N is_LayerFunc_Seq D,K,k,n iff ( len N = n & N is_Multilayer_perceptron_with k,n & ( for i being Nat st 1 <= i & i < len k holds
ex Ni being Function of (REAL-NS (k . i)),(REAL-NS (k . (i + 1))) st
( N . i = Ni & Ni is_LayerFunc D,K ) ) ) );

theorem Th34: :: NEURONS1:34

for D, K being Real st 0 <= D & 0 <= K holds
for n being Nat
for k being FinSequence of NAT
for N being non empty FinSequence st N is_LayerFunc_Seq D,K,k,n holds
OutPutFunc (N,k,n) is_LayerFunc D |^ n,K

proof end;

theorem :: NEURONS1:35

for n being 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

proof end;