defpred S1[ object , object ] means for SX being SimplicialComplexStr of X st the topology of SX = $1 & [#] SX = [#] KX holds
the topology of (subdivision (P,SX)) = $2;
set BBK = bool (bool ([#] KX));
A1:
for x being object st x in bool (bool ([#] KX)) holds
ex y being object st
( y in bool (bool ([#] KX)) & S1[x,y] )
proof
let x be
object ;
( x in bool (bool ([#] KX)) implies ex y being object st
( y in bool (bool ([#] KX)) & S1[x,y] ) )
assume A2:
x in bool (bool ([#] KX))
;
ex y being object st
( y in bool (bool ([#] KX)) & S1[x,y] )
per cases
( ex SX being SimplicialComplexStr of X st
( the topology of SX = x & [#] SX = [#] KX ) or for SX being SimplicialComplexStr of X holds
( the topology of SX <> x or [#] SX <> [#] KX ) )
;
suppose
ex
SX being
SimplicialComplexStr of
X st
( the
topology of
SX = x &
[#] SX = [#] KX )
;
ex y being object st
( y in bool (bool ([#] KX)) & S1[x,y] )then consider SX being
SimplicialComplexStr of
X such that A3:
the
topology of
SX = x
and A4:
[#] SX = [#] KX
;
take T = the
topology of
(subdivision (P,SX));
( T in bool (bool ([#] KX)) & S1[x,T] )
[#] (subdivision (P,SX)) = [#] SX
by Def20;
hence
T in bool (bool ([#] KX))
by A4;
S1[x,T]let SX1 be
SimplicialComplexStr of
X;
( the topology of SX1 = x & [#] SX1 = [#] KX implies the topology of (subdivision (P,SX1)) = T )assume A5:
( the
topology of
SX1 = x &
[#] SX1 = [#] KX )
;
the topology of (subdivision (P,SX1)) = T
TopStruct(# the
carrier of
SX, the
topology of
SX #)
= TopStruct(# the
carrier of
SX1, the
topology of
SX1 #)
by A3, A4, A5;
hence
the
topology of
(subdivision (P,SX1)) = T
by Th60;
verum end;
end;
consider f being Function of (bool (bool ([#] KX))),(bool (bool ([#] KX))) such that
A7:
for x being object st x in bool (bool ([#] KX)) holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
deffunc H1( set , set ) -> set = f . $2;
consider g being Function such that
A8:
( dom g = NAT & g . 0 = the topology of KX & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) )
from NAT_1:sch 11();
defpred S2[ Nat] means ( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . $1 & [#] SX = [#] KX & ( $1 > 0 implies SX is strict ) ) & ( for SX being SimplicialComplexStr of X st the topology of SX = g . $1 & [#] SX = [#] KX holds
g . ($1 + 1) = the topology of (subdivision (P,SX)) ) );
g . (0 + 1) = f . the topology of KX
by A8;
then A9:
g . 1 = the topology of (subdivision (P,KX))
by A7;
A10:
S2[ 0 ]
defpred S3[ object , object ] means for k being Nat st k = $1 holds
( ( k = 0 implies $2 = KX ) & ( k > 0 implies for SF being Subset-Family of KX st SF = g . k holds
$2 = TopStruct(# the carrier of KX,SF #) ) );
A11:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
set k1 =
k + 1;
given SX being
SimplicialComplexStr of
X such that A12:
the
topology of
SX = g . k
and A13:
[#] SX = [#] KX
and
(
k > 0 implies
SX is
strict )
;
( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . k & [#] SX = [#] KX & not g . (k + 1) = the topology of (subdivision (P,SX)) ) or S2[k + 1] )
assume
for
SX being
SimplicialComplexStr of
X st the
topology of
SX = g . k &
[#] SX = [#] KX holds
g . (k + 1) = the
topology of
(subdivision (P,SX))
;
S2[k + 1]
then A14:
g . (k + 1) = the
topology of
(subdivision (P,SX))
by A12, A13;
[#] (subdivision (P,SX)) = [#] KX
by A13, Def20;
hence
ex
SX being
SimplicialComplexStr of
X st
( the
topology of
SX = g . (k + 1) &
[#] SX = [#] KX & (
k + 1
> 0 implies
SX is
strict ) )
by A14;
for SX being SimplicialComplexStr of X st the topology of SX = g . (k + 1) & [#] SX = [#] KX holds
g . ((k + 1) + 1) = the topology of (subdivision (P,SX))
let S1 be
SimplicialComplexStr of
X;
( the topology of S1 = g . (k + 1) & [#] S1 = [#] KX implies g . ((k + 1) + 1) = the topology of (subdivision (P,S1)) )
assume A15:
( the
topology of
S1 = g . (k + 1) &
[#] S1 = [#] KX )
;
g . ((k + 1) + 1) = the topology of (subdivision (P,S1))
g . ((k + 1) + 1) = f . (g . (k + 1))
by A8;
hence
g . ((k + 1) + 1) = the
topology of
(subdivision (P,S1))
by A7, A15;
verum
end;
A16:
for k being Nat holds S2[k]
from NAT_1:sch 2(A10, A11);
A17:
for x being object st x in NAT holds
ex y being object st S3[x,y]
consider h being Function such that
A22:
( dom h = NAT & ( for x being object st x in NAT holds
S3[x,h . x] ) )
from CLASSES1:sch 1(A17);
A23:
h . 0 = KX
by A22;
A24:
for k being Nat
for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)
proof
let k be
Nat;
for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)let KK be
SimplicialComplexStr of
X;
( h . k = KK implies h . (k + 1) = subdivision (P,KK) )
assume A25:
h . k = KK
;
h . (k + 1) = subdivision (P,KK)
S2[
k + 1]
by A16;
then consider K1 being
SimplicialComplexStr of
X such that A26:
the
topology of
K1 = g . (k + 1)
and A27:
[#] K1 = [#] KX
;
reconsider TOP1 = the
topology of
K1 as
Subset-Family of
KX by A27;
A28:
k in NAT
by ORDINAL1:def 12;
S2[
k]
by A16;
then consider K2 being
SimplicialComplexStr of
X such that A29:
the
topology of
K2 = g . k
and A30:
[#] K2 = [#] KX
;
reconsider TOP2 = the
topology of
K2 as
Subset-Family of
KX by A30;
A31:
[#] (subdivision (P,KK)) = [#] KK
by Def20;
per cases
( k = 0 or k > 0 )
;
suppose A32:
k = 0
;
h . (k + 1) = subdivision (P,KK)then
TOP1 = the
topology of
(subdivision (P,KK))
by A8, A10, A23, A25, A26;
hence
h . (k + 1) = subdivision (
P,
KK)
by A22, A23, A25, A26, A31, A32;
verum end; suppose
k > 0
;
h . (k + 1) = subdivision (P,KK)then A33:
KK = TopStruct(# the
carrier of
KX,
TOP2 #)
by A22, A25, A28, A29;
then
[#] KK = [#] KX
;
then
g . (k + 1) = the
topology of
(subdivision (P,KK))
by A16, A29, A33;
hence
h . (k + 1) = subdivision (
P,
KK)
by A22, A31, A33;
verum end;
end;